:: Riemann-Stieltjes Integral
::  by Keiko Narita , Kazuhisa Nakasho and Yasunari Shidama
:: 
:: Received June 30, 2016
:: Copyright (c) 2016-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, INTEGRA1, SUBSET_1, FUNCT_1, FINSEQ_1, NAT_1, RELAT_1,
      MEASURE7, XBOOLE_0, XXREAL_2, XXREAL_0, SEQ_4, CARD_1, REAL_1, ARYTM_3,
      ARYTM_1, CARD_3, FINSEQ_2, INTEGRA2, SEQ_1, SEQ_2, ORDINAL2, COMPLEX1,
      XXREAL_1, FUNCT_3, PARTFUN1, VALUED_1, TARSKI, INTEGR15, MEASURE5,
      FUNCT_7, INTEGR22, VALUED_0, ZFMISC_1, ORDINAL4, FUNCOP_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, RELAT_1, FUNCT_1, ORDINAL1,
      RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, BINOP_1, NUMBERS, XCMPLX_0,
      XXREAL_0, XREAL_0, NAT_1, VALUED_0, COMPLEX1, XXREAL_2, FINSEQ_1,
      FINSEQ_2, VALUED_1, SEQ_1, SEQ_2, RVSUM_1, SEQ_4, RCOMP_1, MEASURE5,
      INTEGRA1, INTEGRA2, INTEGRA3;
 constructors REAL_1, FINSEQOP, MONOID_0, SEQ_4, NAT_D, SUPINF_2, INTEGRA2,
      RELSET_1, SEQ_2, INTEGRA3, COMSEQ_2;
 registrations NUMBERS, XREAL_0, SEQ_2, INTEGRA1, FUNCT_2, NAT_1, MEMBERED,
      ORDINAL1, VALUED_0, VALUED_1, RELSET_1, CARD_1, MEASURE5, FINSEQ_1,
      SEQM_3, INT_1, XXREAL_2;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Properties of Real Finite Sequences

definition
  let A be Subset of REAL;
  let rho be real-valued Function;
  func vol(A,rho) -> Real equals
:: INTEGR22:def 1
  0 if A is empty otherwise
    rho.(upper_bound A) - rho.(lower_bound A);
end;

theorem :: INTEGR22:1
for A being non empty closed_interval Subset of REAL,
    D being Division of A,
    rho be Function of A,REAL,
    B be non empty closed_interval Subset of REAL,
    v be FinSequence of REAL
      st B c= A & len D = len v &
         for i be Nat st i in dom v
           holds v.i = vol (B /\ divset(D,i),rho)
 holds Sum v = vol (B,rho);

theorem :: INTEGR22:2
  for n,m be Nat, a be Function of [:Seg n,Seg m:],REAL
  for p,q be FinSequence of REAL st
    ( dom p = Seg n
    & for i be Nat st i in dom p holds
        ex r be FinSequence of REAL st
          (dom r = Seg m & p.i = Sum r
         & for j be Nat st j in dom r holds r.j=a.(i,j) ) )
  & ( dom q = Seg m
    & for j be Nat st j in dom q holds
        ex s be FinSequence of REAL st
          (dom s = Seg n & q.j = Sum s
         & for i be Nat st i in dom s holds s.i=a.(i,j) ) )
  holds Sum p = Sum q;

begin :: The Definitions of Bounded Variation

definition
  let A be non empty closed_interval Subset of REAL;
  let rho be real-valued Function;
  let t be Division of A;
  mode var_volume of rho,t -> FinSequence of REAL means
:: INTEGR22:def 2
    len it = len t
    & for k be Nat st k in dom t holds it.k = |. vol (divset(t,k),rho) .|;
end;

theorem :: INTEGR22:3
for A be non empty closed_interval Subset of REAL,
    rho be Function of A,REAL,
    t be Division of A,
    F be var_volume of rho,t
 holds for k be Nat st k in dom F holds 0 <= F.k;

theorem :: INTEGR22:4
for A be non empty closed_interval Subset of REAL,
    rho be Function of A,REAL,
    t be Division of A,
    F be var_volume of rho,t
 holds 0 <= Sum(F);

definition
  let A be non empty closed_interval Subset of REAL;
  let rho be Function of A,REAL;
  attr rho is bounded_variation means
:: INTEGR22:def 3
  ex d be Real st
    0 < d
   &
    for t be Division of A, F be var_volume of rho,t
      holds Sum(F) <= d;
end;

definition
  let A be non empty closed_interval Subset of REAL;
  let rho be Function of A,REAL;
  assume
 rho is bounded_variation;
  func total_vd(rho) -> Real means
:: INTEGR22:def 4
  ex VD be non empty Subset of REAL st
    VD is bounded_above
   &
    VD = { r where r is Real:
           ex t be Division of A, F be var_volume of rho,t st
             r = Sum(F) }
   & it = upper_bound VD;
end;

theorem :: INTEGR22:5
 for A be non empty closed_interval Subset of REAL,
     rho be Function of A,REAL,
     T be Division of A
   st rho is bounded_variation holds
   for F be var_volume of rho,T
     holds Sum(F) <= total_vd(rho);

theorem :: INTEGR22:6
  for A be non empty closed_interval Subset of REAL,
      rho be Function of A,REAL
   st rho is bounded_variation holds
   0 <= total_vd(rho);

begin :: The definitions of Riemann-Stieltjes Integral

definition
  let A be non empty closed_interval Subset of REAL;
  let rho be Function of A,REAL;
  let u be PartFunc of REAL,REAL;
  assume
 rho is bounded_variation & dom u = A;
  let t be Division of A;
  mode middle_volume of rho,u,t -> FinSequence of REAL means
:: INTEGR22:def 5
  len it = len t
  & for k be Nat st k in dom t holds ex r be Real st
  r in rng (u|divset(t,k))
  & it.k = r*(vol (divset(t,k),rho));
end;

definition
  let A be non empty closed_interval Subset of REAL;
  let rho be Function of A,REAL;
  let u be PartFunc of REAL,REAL;
:::  assume rho is bounded_variation & dom u = A;
  let T be DivSequence of A;
  mode middle_volume_Sequence of rho,u,T -> sequence of (REAL)* means
:: INTEGR22:def 6
    for k be Element of NAT holds it.k is middle_volume of rho,u,T.k;
end;

definition
  let A be non empty closed_interval Subset of REAL;
  let rho be Function of A,REAL;
  let u be PartFunc of REAL,REAL;
:::  assume rho is bounded_variation & dom u = A;
  let T be DivSequence of A;
  let S be middle_volume_Sequence of rho,u,T;
  let k be Nat;
  redefine func S.k -> middle_volume of rho,u,T.k;
end;

reserve A for non empty closed_interval Subset of REAL;
reserve rho for Function of A,REAL;
reserve u for PartFunc of REAL,REAL;
reserve T for DivSequence of A;
reserve S for middle_volume_Sequence of rho,u,T;
reserve k for Nat;

definition
  let A be non empty closed_interval Subset of REAL;
  let rho be Function of A,REAL;
  let u be PartFunc of REAL,REAL;
:::  assume rho is bounded_variation & dom u = A;
  let T be DivSequence of A;
  let S be middle_volume_Sequence of rho,u,T;
  func middle_sum(S) -> Real_Sequence means
:: INTEGR22:def 7
  for i be Nat holds it.i = Sum(S.i);
end;

definition
  let A be non empty closed_interval Subset of REAL;
  let rho be Function of A,REAL;
  let u be PartFunc of REAL,REAL;
:::  assume rho is bounded_variation & dom u = A;
  pred u is_RiemannStieltjes_integrable_with rho means
:: INTEGR22:def 8
  ex I be Real st for T being DivSequence of A,
     S be middle_volume_Sequence of rho,u,T st
     delta(T) is convergent & lim delta(T) = 0 holds
     middle_sum(S) is convergent & lim (middle_sum(S)) = I;
end;

definition
  let A be non empty closed_interval Subset of REAL;
  let rho be Function of A,REAL;
  let u be PartFunc of REAL,REAL;
  assume rho is bounded_variation & dom u = A &
            u is_RiemannStieltjes_integrable_with rho;
  func integral(u,rho) -> Real means
:: INTEGR22:def 9
  for T being DivSequence of A,
      S be middle_volume_Sequence of rho,u,T st
        delta(T) is convergent & lim delta(T) = 0 holds
        middle_sum(S) is convergent & lim (middle_sum(S)) = it;
end;

begin :: Linearity of Riemann-Stieltjes Integral

theorem :: INTEGR22:7
  for A be non empty closed_interval Subset of REAL,
      r be Real,
      rho be Function of A,REAL,
      u,w be PartFunc of REAL,REAL st
      rho is bounded_variation & dom u = A & dom w = A &
      w = r(#)u & u is_RiemannStieltjes_integrable_with rho holds
        w is_RiemannStieltjes_integrable_with rho &
        integral(w,rho) = r * integral(u,rho);

theorem :: INTEGR22:8
  for A be non empty closed_interval Subset of REAL,
      rho be Function of A,REAL,
      u,w be PartFunc of REAL,REAL st
      rho is bounded_variation & dom u = A & dom w = A &
      w = -u & u is_RiemannStieltjes_integrable_with rho holds
        w is_RiemannStieltjes_integrable_with rho &
        integral(w,rho) = -integral(u,rho);

theorem :: INTEGR22:9
  for A be non empty closed_interval Subset of REAL,
      rho be Function of A,REAL,
      u,v,w be PartFunc of REAL,REAL st
      rho is bounded_variation & dom u = A & dom v = A & dom w = A &
      w = u + v & u is_RiemannStieltjes_integrable_with rho &
      v is_RiemannStieltjes_integrable_with rho holds
        w is_RiemannStieltjes_integrable_with rho &
        integral(w,rho) = integral(u,rho) + integral(v,rho);

theorem :: INTEGR22:10
  for A be non empty closed_interval Subset of REAL,
      rho be Function of A,REAL,
      u,v,w be PartFunc of REAL,REAL st
      rho is bounded_variation & dom u = A & dom v = A & dom w = A &
      w = u - v & u is_RiemannStieltjes_integrable_with rho &
      v is_RiemannStieltjes_integrable_with rho holds
        w is_RiemannStieltjes_integrable_with rho &
        integral(w,rho) = integral(u,rho) - integral(v,rho);

theorem :: INTEGR22:11
  for A,B be non empty closed_interval Subset of REAL,
      r be Real, rho,rho1 be Function of A,REAL
    st B c= A & rho = r(#)rho1
   holds vol(B,rho) = r * vol(B,rho1);

theorem :: INTEGR22:12
  for A be non empty closed_interval Subset of REAL,
      r be Real, rho,rho1 be Function of A,REAL,
      u be PartFunc of REAL,REAL st
      rho is bounded_variation & rho1 is bounded_variation & dom u = A &
      rho = r(#)rho1 & u is_RiemannStieltjes_integrable_with rho1 holds
        u is_RiemannStieltjes_integrable_with rho &
        integral(u,rho) = r * integral(u,rho1);

theorem :: INTEGR22:13
  for A be non empty closed_interval Subset of REAL,
      rho,rho1 be Function of A,REAL,
      u be PartFunc of REAL,REAL st
      rho is bounded_variation & rho1 is bounded_variation & dom u = A &
      rho = -rho1 & u is_RiemannStieltjes_integrable_with rho1 holds
        u is_RiemannStieltjes_integrable_with rho &
        integral(u,rho) = -integral(u,rho1);

theorem :: INTEGR22:14
  for A,B be non empty closed_interval Subset of REAL,
      rho,rho1,rho2 be Function of A,REAL
    st B c= A & rho = rho1 + rho2
   holds vol(B,rho) = vol(B,rho1) + vol(B,rho2);

theorem :: INTEGR22:15
  for A be non empty closed_interval Subset of REAL,
      rho,rho1,rho2 be Function of A,REAL,
      u be PartFunc of REAL,REAL st
      rho is bounded_variation & rho1 is bounded_variation &
      rho2 is bounded_variation & dom u = A &
      rho = rho1 + rho2 & u is_RiemannStieltjes_integrable_with rho1 &
      u is_RiemannStieltjes_integrable_with rho2
      holds
        u is_RiemannStieltjes_integrable_with rho &
        integral(u,rho) = integral(u,rho1) + integral(u,rho2);

theorem :: INTEGR22:16
  for A,B be non empty closed_interval Subset of REAL,
      rho,rho1,rho2 be Function of A,REAL
    st B c= A & rho = rho1 - rho2
   holds vol(B,rho) = vol(B,rho1) - vol(B,rho2);

theorem :: INTEGR22:17
  for A be non empty closed_interval Subset of REAL,
      rho,rho1,rho2 be Function of A,REAL,
      u be PartFunc of REAL,REAL st
      rho is bounded_variation & rho1 is bounded_variation &
      rho2 is bounded_variation & dom u = A &
      rho = rho1 - rho2 & u is_RiemannStieltjes_integrable_with rho1 &
      u is_RiemannStieltjes_integrable_with rho2
    holds
        u is_RiemannStieltjes_integrable_with rho &
        integral(u,rho) = integral(u,rho1) - integral(u,rho2);