:: Riemann-Stieltjes Integral
:: by Keiko Narita , Kazuhisa Nakasho and Yasunari Shidama
::
:: Copyright (c) 2016-2021 Association of Mizar Users

definition
let A be Subset of REAL;
let rho be real-valued Function;
func vol (A,rho) -> Real equals :Defvol: :: INTEGR22:def 1
0 if A is empty
otherwise (rho . ()) - (rho . ());
correctness
coherence
( ( A is empty implies 0 is Real ) & ( not A is empty implies (rho . ()) - (rho . ()) is Real ) )
;
consistency
for b1 being Real holds verum
;
;
end;

:: deftheorem Defvol defines vol INTEGR22:def 1 :
for A being Subset of REAL
for rho being real-valued Function holds
( ( A is empty implies vol (A,rho) = 0 ) & ( not A is empty implies vol (A,rho) = (rho . ()) - (rho . ()) ) );

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

proof end;

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

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

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 :defvm: :: INTEGR22:def 2
( len it = len t & ( for k being Nat st k in dom t holds
it . k = |.(vol ((divset (t,k)),rho)).| ) );
correctness
existence
ex b1 being FinSequence of REAL st
( len b1 = len t & ( for k being Nat st k in dom t holds
b1 . k = |.(vol ((divset (t,k)),rho)).| ) )
;
proof end;
end;

:: deftheorem defvm defines var_volume INTEGR22:def 2 :
for A being non empty closed_interval Subset of REAL
for rho being real-valued Function
for t being Division of A
for b4 being FinSequence of REAL holds
( b4 is var_volume of rho,t iff ( len b4 = len t & ( for k being Nat st k in dom t holds
b4 . k = |.(vol ((divset (t,k)),rho)).| ) ) );

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

theorem LM2: :: INTEGR22:4
for A being non empty closed_interval Subset of REAL
for rho being Function of A,REAL
for t being Division of A
for F being var_volume of rho,t holds 0 <= Sum F
proof end;

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 being Real st
( 0 < d & ( for t being Division of A
for F being var_volume of rho,t holds Sum F <= d ) );
end;

:: deftheorem defines bounded_variation INTEGR22:def 3 :
for A being non empty closed_interval Subset of REAL
for rho being Function of A,REAL holds
( rho is bounded_variation iff ex d being Real st
( 0 < d & ( for t being Division of A
for F being var_volume of rho,t holds Sum F <= d ) ) );

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

:: deftheorem DeftotalVD defines total_vd INTEGR22:def 4 :
for A being non empty closed_interval Subset of REAL
for rho being Function of A,REAL st rho is bounded_variation holds
for b3 being Real holds
( b3 = total_vd rho iff ex VD being non empty Subset of REAL st
( VD is bounded_above & VD = { r where r is Real : ex t being Division of A ex F being var_volume of rho,t st r = Sum F } & b3 = upper_bound VD ) );

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

theorem :: INTEGR22:6
for A being non empty closed_interval Subset of REAL
for rho being Function of A,REAL st rho is bounded_variation holds
0 <= total_vd rho
proof 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 AS: ( rho is bounded_variation & dom u = A ) ;
let t be Division of A;
mode middle_volume of rho,u,t -> FinSequence of REAL means :Def1: :: INTEGR22:def 5
( len it = len t & ( for k being Nat st k in dom t holds
ex r being Real st
( r in rng (u | (divset (t,k))) & it . k = r * (vol ((divset (t,k)),rho)) ) ) );
correctness
existence
ex b1 being FinSequence of REAL st
( len b1 = len t & ( for k being Nat st k in dom t holds
ex r being Real st
( r in rng (u | (divset (t,k))) & b1 . k = r * (vol ((divset (t,k)),rho)) ) ) )
;
proof end;
end;

:: deftheorem Def1 defines middle_volume INTEGR22:def 5 :
for A being non empty closed_interval Subset of REAL
for rho being Function of A,REAL
for u being PartFunc of REAL,REAL st rho is bounded_variation & dom u = A holds
for t being Division of A
for b5 being FinSequence of REAL holds
( b5 is middle_volume of rho,u,t iff ( len b5 = len t & ( for k being Nat st k in dom t holds
ex r being Real st
( r in rng (u | (divset (t,k))) & b5 . k = r * (vol ((divset (t,k)),rho)) ) ) ) );

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;
let T be DivSequence of A;
::: assume rho is bounded_variation & dom u = A;
mode middle_volume_Sequence of rho,u,T -> sequence of () means :Def3: :: INTEGR22:def 6
for k being Element of NAT holds it . k is middle_volume of rho,u,T . k;
correctness
existence
ex b1 being sequence of () st
for k being Element of NAT holds b1 . k is middle_volume of rho,u,T . k
;
proof end;
end;

:: deftheorem Def3 defines middle_volume_Sequence INTEGR22:def 6 :
for A being non empty closed_interval Subset of REAL
for rho being Function of A,REAL
for u being PartFunc of REAL,REAL
for T being DivSequence of A
for b5 being sequence of () holds
( b5 is middle_volume_Sequence of rho,u,T iff for k being Element of NAT holds b5 . k is middle_volume of rho,u,T . k );

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;
let T be DivSequence of A;
let S be middle_volume_Sequence of rho,u,T;
let k be Nat;
:: original: .
redefine func S . k -> middle_volume of rho,u,T . k;
coherence
S . k is middle_volume of rho,u,T . k
proof end;
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;
let T be DivSequence of A;
let S be middle_volume_Sequence of rho,u,T;
func middle_sum S -> Real_Sequence means :Def4: :: INTEGR22:def 7
for i being Nat holds it . i = Sum (S . i);
existence
ex b1 being Real_Sequence st
for i being Nat holds b1 . i = Sum (S . i)
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for i being Nat holds b1 . i = Sum (S . i) ) & ( for i being Nat holds b2 . i = Sum (S . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines middle_sum INTEGR22:def 7 :
for A being non empty closed_interval Subset of REAL
for rho being Function of A,REAL
for u being PartFunc of REAL,REAL
for T being DivSequence of A
for S being middle_volume_Sequence of rho,u,T
for b6 being Real_Sequence holds
( b6 = middle_sum S iff for i being Nat holds b6 . i = Sum (S . i) );

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 being Real st
for T being DivSequence of A
for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim () = 0 holds
( middle_sum S is convergent & lim () = I );
end;

:: deftheorem defines is_RiemannStieltjes_integrable_with INTEGR22:def 8 :
for A being non empty closed_interval Subset of REAL
for rho being Function of A,REAL
for u being PartFunc of REAL,REAL holds
( u is_RiemannStieltjes_integrable_with rho iff ex I being Real st
for T being DivSequence of A
for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim () = 0 holds
( middle_sum S is convergent & lim () = I ) );

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 A1: ( rho is bounded_variation & dom u = A & u is_RiemannStieltjes_integrable_with rho ) ;
func integral (u,rho) -> Real means :Def6: :: INTEGR22:def 9
for T being DivSequence of A
for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim () = 0 holds
( middle_sum S is convergent & lim () = it );
existence
ex b1 being Real st
for T being DivSequence of A
for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim () = 0 holds
( middle_sum S is convergent & lim () = b1 )
by A1;
uniqueness
for b1, b2 being Real st ( for T being DivSequence of A
for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim () = 0 holds
( middle_sum S is convergent & lim () = b1 ) ) & ( for T being DivSequence of A
for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim () = 0 holds
( middle_sum S is convergent & lim () = b2 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines integral INTEGR22:def 9 :
for A being non empty closed_interval Subset of REAL
for rho being Function of A,REAL
for u being PartFunc of REAL,REAL st rho is bounded_variation & dom u = A & u is_RiemannStieltjes_integrable_with rho holds
for b4 being Real holds
( b4 = integral (u,rho) iff for T being DivSequence of A
for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim () = 0 holds
( middle_sum S is convergent & lim () = b4 ) );

theorem Th4: :: INTEGR22:7
for A being non empty closed_interval Subset of REAL
for r being Real
for rho being Function of A,REAL
for u, w being 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)) )
proof end;

reconsider jj = 1 as Real ;

theorem Th5: :: INTEGR22:8
for A being non empty closed_interval Subset of REAL
for rho being Function of A,REAL
for u, w being 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)) )
proof end;

theorem Th6: :: INTEGR22:9
for A being non empty closed_interval Subset of REAL
for rho being Function of A,REAL
for u, v, w being 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)) )
proof end;

theorem :: INTEGR22:10
for A being non empty closed_interval Subset of REAL
for rho being Function of A,REAL
for u, v, w being 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)) )
proof end;

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

theorem Th4A: :: INTEGR22:12
for A being non empty closed_interval Subset of REAL
for r being Real
for rho, rho1 being Function of A,REAL
for u being 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)) )
proof end;

theorem :: INTEGR22:13
for A being non empty closed_interval Subset of REAL
for rho, rho1 being Function of A,REAL
for u being 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)) )
proof end;

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

theorem :: INTEGR22:15
for A being non empty closed_interval Subset of REAL
for rho, rho1, rho2 being Function of A,REAL
for u being 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)) )
proof end;

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

theorem :: INTEGR22:17
for A being non empty closed_interval Subset of REAL
for rho, rho1, rho2 being Function of A,REAL
for u being 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)) )
proof end;