:: Riemann Integral of Functions from $\mathbbbR$ into Real {B}anach Space
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received June 18, 2013
:: 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 b₁ 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 = ||.v.|| ) ) 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 (delta T) = 0 holds
middle_sum (h,S) is convergent

proof end;

scheme :: INTEGR20:sch 1
ExRealSeq2X{ F₁() -> non empty set , F₂( set ) -> Element of F₁(), F₃( set ) -> Element of F₁() } :

ex s being sequence of F₁() st
for n being Nat holds
( s . (2 * n) = F₂(n) & s . ((2 * n) + 1) = F₃(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 (delta T) = 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;