:: by Keiko Narita , Noboru Endou and Yasunari Shidama

::

:: Received June 18, 2013

:: Copyright (c) 2013-2021 Association of Mizar Users

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

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

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

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

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

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;

correctness

coherence

( ( A is empty implies 0 is Real ) & ( not A is empty implies vol A is Real ) );

consistency

for b_{1} being Real holds verum;

;

end;
correctness

coherence

( ( A is empty implies 0 is Real ) & ( not A is empty implies vol A is Real ) );

consistency

for b

;

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

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

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

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

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

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

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

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

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

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;

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 )

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 )

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 )

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 )

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']

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;