:: Riemann Integral of Functions from $\mathbbbR$ into Real {B}anach Space
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Copyright (c) 2013-2021 Association of Mizar Users

definition
let X be RealNormSpace;
let f be PartFunc of REAL, the carrier of X;
attr f is uniformly_continuous means :: INTEGR20:def 1
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom f & x2 in dom f & |.(x1 - x2).| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) );
end;

:: deftheorem defines uniformly_continuous INTEGR20:def 1 :
for X being RealNormSpace
for f being PartFunc of REAL, the carrier of X holds
( f is uniformly_continuous iff for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom f & x2 in dom f & |.(x1 - x2).| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) ) );

theorem Th1: :: INTEGR20:1
for X being set
for Y being RealNormSpace
for f being PartFunc of REAL, the carrier of Y holds
( f | X is uniformly_continuous iff for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & |.(x1 - x2).| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) ) )
proof end;

theorem :: INTEGR20:2
for X, X1 being set
for Y being RealNormSpace
for f being PartFunc of REAL, the carrier of Y st f | X is uniformly_continuous & X1 c= X holds
f | X1 is uniformly_continuous
proof end;

theorem Th3: :: INTEGR20:3
for X being RealNormSpace
for f being PartFunc of REAL, the carrier of X
for Z being Subset of REAL st Z c= dom f & Z is compact & f | Z is continuous holds
f | Z is uniformly_continuous
proof end;

theorem Th4: :: INTEGR20:4
for X being RealNormSpace
for n, m being Nat
for a being Function of [:(Seg n),(Seg m):],X
for p, q being FinSequence of X st dom p = Seg n & ( for i being Nat st i in dom p holds
ex r being FinSequence of X 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 X 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 Subset of REAL;
func xvol A -> Real equals :Def2: :: INTEGR20:def 2
0 if A is empty
otherwise vol A;
correctness
coherence
( ( A is empty implies 0 is Real ) & ( not A is empty implies vol A is Real ) )
;
consistency
for b1 being Real holds verum
;
;
end;

:: deftheorem Def2 defines xvol INTEGR20:def 2 :
for A being Subset of REAL holds
( ( A is empty implies xvol A = 0 ) & ( not A is empty implies xvol A = vol A ) );

Lm1: for X, Y, Z being non empty set
for f being PartFunc of X,Y st Z c= dom f holds
f | Z is Function of Z,Y

proof end;

theorem Th5: :: INTEGR20:5
for A being real-bounded Subset of REAL holds 0 <= xvol A
proof end;

theorem Th6: :: INTEGR20:6
for A being non empty closed_interval Subset of REAL
for D being Division of A
for q being FinSequence of REAL st dom q = Seg (len D) & ( for i being Nat st i in Seg (len D) holds
q . i = vol (divset (D,i)) ) holds
Sum q = vol A
proof end;

theorem Th7: :: INTEGR20:7
for Y being RealNormSpace
for E being Point of Y
for q being FinSequence of REAL
for S being FinSequence of Y st len S = len q & ( for i being Nat st i in dom S holds
ex r being Real st
( r = q . i & S . i = r * E ) ) holds
Sum S = (Sum q) * E
proof end;

theorem Th8: :: INTEGR20:8
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 B c= A & len D = len v & ( for i being Nat st i in dom v holds
v . i = xvol (B /\ (divset (D,i))) ) holds
Sum v = vol B
proof end;

Lm2: for Y being RealNormSpace
for xseq, yseq being FinSequence of Y st len xseq = (len yseq) + 1 & xseq | (len yseq) = yseq holds
ex v being Point of Y st
( v = xseq /. (len xseq) & Sum xseq = (Sum yseq) + v )

proof end;

theorem Th9: :: INTEGR20:9
for Y being RealNormSpace
for xseq being FinSequence of Y
for yseq being FinSequence of REAL st len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
ex v being Point of Y st
( v = xseq /. i & yseq . i = ) ) holds
||.(Sum xseq).|| <= Sum yseq
proof end;

theorem Th10: :: INTEGR20:10
for Y being RealNormSpace
for p being FinSequence of Y
for q being FinSequence of REAL st len p = len q & ( for j being Nat st j in dom p holds
||.(p /. j).|| <= q . j ) holds
||.(Sum p).|| <= Sum q
proof end;

theorem Th11: :: INTEGR20:11
for j being Element of NAT
for A being non empty closed_interval Subset of REAL
for D1 being Division of A st j in dom D1 holds
vol (divset (D1,j)) <= delta D1
proof end;

theorem Th12: :: INTEGR20:12
for A being non empty closed_interval Subset of REAL
for D being Division of A
for r being Real st delta D < r holds
for i being Nat
for s, t being Real st i in dom D & s in divset (D,i) & t in divset (D,i) holds
|.(s - t).| < r
proof end;

theorem Th13: :: INTEGR20:13
for X being RealBanachSpace
for A being non empty closed_interval Subset of REAL
for h being Function of A, the carrier of X st ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom h & x2 in dom h & |.(x1 - x2).| < s holds
||.((h /. x1) - (h /. x2)).|| < r ) ) ) holds
for T being DivSequence of A
for S being middle_volume_Sequence of h,T st delta T is convergent & lim () = 0 holds
middle_sum (h,S) is convergent
proof end;

scheme :: INTEGR20:sch 1
ExRealSeq2X{ F1() -> non empty set , F2( set ) -> Element of F1(), F3( set ) -> Element of F1() } :
ex s being sequence of F1() st
for n being Nat holds
( s . (2 * n) = F2(n) & s . ((2 * n) + 1) = F3(n) )
proof end;

theorem Th14: :: INTEGR20:14
for n being Nat ex k being Nat st
( n = 2 * k or n = (2 * k) + 1 )
proof end;

theorem Th15: :: INTEGR20:15
for A being non empty closed_interval Subset of REAL
for T0, T being DivSequence of A ex T1 being DivSequence of A st
for i being Nat holds
( T1 . (2 * i) = T0 . i & T1 . ((2 * i) + 1) = T . i )
proof end;

theorem Th16: :: INTEGR20:16
for A being non empty closed_interval Subset of REAL
for T0, T, T1 being DivSequence of A st delta T0 is convergent & lim (delta T0) = 0 & delta T is convergent & lim () = 0 & ( for i being Nat holds
( T1 . (2 * i) = T0 . i & T1 . ((2 * i) + 1) = T . i ) ) holds
( delta T1 is convergent & lim (delta T1) = 0 )
proof end;

theorem Th17: :: INTEGR20:17
for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for h being Function of A, the carrier of X
for T0, T, T1 being DivSequence of A
for S0 being middle_volume_Sequence of h,T0
for S being middle_volume_Sequence of h,T st ( for i being Nat holds
( T1 . (2 * i) = T0 . i & T1 . ((2 * i) + 1) = T . i ) ) holds
ex S1 being middle_volume_Sequence of h,T1 st
for i being Nat holds
( S1 . (2 * i) = S0 . i & S1 . ((2 * i) + 1) = S . i )
proof end;

theorem Th18: :: INTEGR20:18
for X being RealNormSpace
for Sq0, Sq, Sq1 being sequence of X st Sq1 is convergent & ( for i being Nat holds
( Sq1 . (2 * i) = Sq0 . i & Sq1 . ((2 * i) + 1) = Sq . i ) ) holds
( Sq0 is convergent & lim Sq0 = lim Sq1 & Sq is convergent & lim Sq = lim Sq1 )
proof end;

theorem :: INTEGR20:19
for a, b being Real
for X being RealBanachSpace
for f being continuous PartFunc of REAL, the carrier of X st a <= b & ['a,b'] c= dom f holds
f is_integrable_on ['a,b']
proof end;