INTEGR22: Riemann-Stieltjes Integral

:: Riemann-Stieltjes Integral
:: by Keiko Narita , Kazuhisa Nakasho and Yasunari Shidama
::
:: Received June 30, 2016
:: 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 . (upper_bound A)) - (rho . (lower_bound A));

end;

:: deftheorem Defvol defines vol INTEGR22:def 1 :

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)).| ) );

proof end;

end;

:: deftheorem defvm defines var_volume INTEGR22:def 2 :

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 :

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 );

proof end;

end;

:: deftheorem DeftotalVD defines total_vd INTEGR22:def 4 :

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)) ) ) );

proof end;

end;

:: deftheorem Def1 defines middle_volume INTEGR22:def 5 :

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 (REAL *) means :Def3: :: INTEGR22:def 6
for k being Element of NAT holds it . k is middle_volume of rho,u,T . k;

proof end;

end;

:: deftheorem Def3 defines middle_volume_Sequence INTEGR22:def 6 :

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

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);

proof end;

proof end;

end;

:: deftheorem Def4 defines middle_sum INTEGR22:def 7 :

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 (delta T) = 0 holds
( middle_sum S is convergent & lim (middle_sum S) = I );

end;

:: deftheorem defines is_RiemannStieltjes_integrable_with INTEGR22:def 8 :

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 (delta T) = 0 holds
( middle_sum S is convergent & lim (middle_sum S) = it );

existence by A1;
uniqueness

proof end;

end;

:: deftheorem Def6 defines integral INTEGR22:def 9 :

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;