:: Relationship between the {R}iemann and {L}ebesgue Integrals
:: by Noboru Endou
::
:: Received September 30, 2021
:: Copyright (c) 2021 Association of Mizar Users


Lm1: for a1, b1 being Real
for a2, b2 being R_eal st a1 = a2 & b1 = b2 holds
a1 - b1 = a2 - b2
proof end;

theorem Th1: :: MESFUN14:1
for X being non empty set
for f being PartFunc of X,ExtREAL holds
( rng (max+ f) c= (rng f) \/ {0} & rng (max- f) c= (rng (- f)) \/ {0} )
proof end;

theorem Th2: :: MESFUN14:2
for X being non empty set
for f being PartFunc of X,ExtREAL st f is V55() holds
( - f is V55() & max+ f is V55() & max- f is V55() )
proof end;

theorem Th3: :: MESFUN14:3
for X being non empty set
for f being PartFunc of X,ExtREAL st f is V171() & f is V172() holds
f is PartFunc of X,REAL
proof end;

theorem Th4: :: MESFUN14:4
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds
( max+ f is_simple_func_in S & max- f is_simple_func_in S )
proof end;

theorem Th5: :: MESFUN14:5
for a, b being Real st a <= b holds
( B-Meas . [.a,b.] = b - a & B-Meas . [.a,b.[ = b - a & B-Meas . ].a,b.] = b - a & B-Meas . ].a,b.[ = b - a & L-Meas . [.a,b.] = b - a & L-Meas . [.a,b.[ = b - a & L-Meas . ].a,b.] = b - a & L-Meas . ].a,b.[ = b - a )
proof end;

theorem :: MESFUN14:6
for a, b being Real st a > b holds
( B-Meas . [.a,b.] = 0 & B-Meas . [.a,b.[ = 0 & B-Meas . ].a,b.] = 0 & B-Meas . ].a,b.[ = 0 & L-Meas . [.a,b.] = 0 & L-Meas . [.a,b.[ = 0 & L-Meas . ].a,b.] = 0 & L-Meas . ].a,b.[ = 0 )
proof end;

theorem :: MESFUN14:7
for A1 being Element of Borel_Sets
for A2 being Element of L-Field
for f being PartFunc of REAL,ExtREAL st A1 = A2 & f is A1 -measurable holds
f is A2 -measurable
proof end;

theorem Th8: :: MESFUN14:8
for a, b being Real
for A being non empty closed_interval Subset of REAL st a < b & A = [.a,b.] holds
for n being Nat st n > 0 holds
ex D being Division of A st D divide_into_equal n
proof end;

Lm2: for r being Real
for F being FinSequence of REAL st ( for n being Nat st n in dom F holds
F . n = r ) holds
Sum F = r * (len F)
proof end;

definition
let F be FinSequence of Borel_Sets ;
let n be Nat;
:: original: .
redefine func F . n -> ext-real-membered set ;
correctness
coherence
F . n is ext-real-membered set ;
proof end;
end;

theorem Th9: :: MESFUN14:9
for a, b being Real
for A being non empty closed_interval Subset of REAL
for D being Division of A st A = [.a,b.] holds
ex F being Finite_Sep_Sequence of Borel_Sets st
( dom D = dom F & union (rng F) = A & ( for k being Nat st k in dom F holds
( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) )
proof end;

theorem Th10: :: MESFUN14:10
for a, b being Real
for A being non empty closed_interval Subset of REAL
for D being Division of A
for f being PartFunc of A,REAL st A = [.a,b.] holds
ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st
( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds
( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & dom g = A & ( for x being Real st x in dom g holds
ex k being Nat st
( 1 <= k & k <= len F & x in F . k & g . x = lower_bound (rng (f | (divset (D,k)))) ) ) )
proof end;

theorem Th11: :: MESFUN14:11
for a, b being Real
for A being non empty closed_interval Subset of REAL
for D being Division of A
for f being PartFunc of A,REAL st A = [.a,b.] holds
ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st
( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds
( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & dom g = A & ( for x being Real st x in dom g holds
ex k being Nat st
( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) )
proof end;

theorem Th12: :: MESFUN14:12
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for F being Finite_Sep_Sequence of S
for a being FinSequence of ExtREAL
for n being Nat st f is_simple_func_in S & F,a are_Re-presentation_of f & n in dom F & not F . n = {} holds
a . n is Real
proof end;

Lm3: for A being non empty closed_interval Subset of REAL
for n being Nat st n > 0 & vol A > 0 holds
ex D being Division of A st D divide_into_equal n
proof end;

definition
let A be non empty closed_interval Subset of REAL;
let n be Nat;
assume A1: ( n > 0 & vol A > 0 ) ;
func EqDiv (A,n) -> Division of A means :Def1: :: MESFUN14:def 1
it divide_into_equal n;
existence
ex b1 being Division of A st b1 divide_into_equal n by A1, Lm3;
uniqueness
for b1, b2 being Division of A st b1 divide_into_equal n & b2 divide_into_equal n holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines EqDiv MESFUN14:def 1 :
for A being non empty closed_interval Subset of REAL
for n being Nat st n > 0 & vol A > 0 holds
for b3 being Division of A holds
( b3 = EqDiv (A,n) iff b3 divide_into_equal n );

theorem :: MESFUN14:13
for A being non empty closed_interval Subset of REAL
for n being Nat st vol A > 0 & len (EqDiv (A,(2 |^ n))) = 1 holds
n = 0
proof end;

theorem :: MESFUN14:14
for a, b being Real
for A being non empty closed_interval Subset of REAL st a < b & A = [.a,b.] holds
ex D being DivSequence of A st
for n being Nat holds D . n divide_into_equal 2 |^ n
proof end;

theorem Th15: :: MESFUN14:15
for A being non empty closed_interval Subset of REAL
for D being Division of A
for n, k being Nat st D divide_into_equal n & k in dom D holds
vol (divset (D,k)) = (vol A) / n
proof end;

theorem Th16: :: MESFUN14:16
for x being Complex
for r being natural Number st x <> 0 holds
(x |^ r) " = (x ") |^ r
proof end;

theorem Th17: :: MESFUN14:17
for A being non empty closed_interval Subset of REAL
for T being sequence of (divs A) st vol A > 0 & ( for n being Nat holds T . n = EqDiv (A,(2 |^ n)) ) holds
( delta T is 0 -convergent & delta T is non-zero )
proof end;

Lm4: for A being non empty closed_interval Subset of REAL
for n being Nat st vol A > 0 & len (EqDiv (A,(2 |^ n))) = 1 holds
divset ((EqDiv (A,(2 |^ n))),1) = A
proof end;

Lm5: for l being Real
for m, n being Nat st l > 1 & n <= m holds
( (l |^ n) * (l |^ (m -' n)) = l |^ m & (l |^ n) * ((l |^ (m -' n)) -' 1) < l |^ m )
proof end;

theorem Th18: :: MESFUN14:18
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f being PartFunc of X,ExtREAL
for F being Finite_Sep_Sequence of S
for a, x being FinSequence of ExtREAL st f is_simple_func_in S & E = dom f & M . E < +infty & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds
x . i = (a . i) * ((M * F) . i) ) holds
Integral (M,f) = Sum x
proof end;

theorem Th19: :: MESFUN14:19
for A being non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL
for D being Division of A st f is bounded & A c= dom f holds
ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st
( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds
( ( len D = 1 implies F . k = [.(inf A),(sup A).] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.(inf A),(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & ( for x being Real st x in dom g holds
ex k being Nat st
( 1 <= k & k <= len F & x in F . k & g . x = lower_bound (rng (f | (divset (D,k)))) ) ) & dom g = A & Integral (B-Meas,g) = lower_sum (f,D) & ( for x being Real st x in A holds
( lower_bound (rng f) <= g . x & g . x <= f . x ) ) )
proof end;

theorem Th20: :: MESFUN14:20
for A being non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL
for D being Division of A st f is bounded & A c= dom f holds
ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st
( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds
( ( len D = 1 implies F . k = [.(inf A),(sup A).] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.(inf A),(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & ( for x being Real st x in dom g holds
ex k being Nat st
( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) & dom g = A & Integral (B-Meas,g) = upper_sum (f,D) & ( for x being Real st x in A holds
( upper_bound (rng f) >= g . x & g . x >= f . x ) ) )
proof end;

theorem Th21: :: MESFUN14:21
for A being non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL st f is bounded & A c= dom f & vol A > 0 holds
ex F being with_the_same_dom Functional_Sequence of REAL,ExtREAL ex I being ExtREAL_sequence st
( A = dom (F . 0) & ( for n being Nat holds
( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = lower_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds
( lower_bound (rng f) <= (F . n) . x & (F . n) . x <= f . x ) ) ) ) & ( for n, m being Nat st n <= m holds
for x being Element of REAL st x in A holds
(F . n) . x <= (F . m) . x ) & ( for x being Element of REAL st x in A holds
( F # x is convergent & lim (F # x) = sup (F # x) & sup (F # x) <= f . x ) ) & lim F is_integrable_on B-Meas & ( for n being Nat holds I . n = Integral (B-Meas,(F . n)) ) & I is convergent & lim I = Integral (B-Meas,(lim F)) )
proof end;

theorem Th22: :: MESFUN14:22
for A being non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL st f is bounded & A c= dom f & vol A > 0 holds
ex F being with_the_same_dom Functional_Sequence of REAL,ExtREAL ex I being ExtREAL_sequence st
( A = dom (F . 0) & ( for n being Nat holds
( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = upper_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds
( upper_bound (rng f) >= (F . n) . x & (F . n) . x >= f . x ) ) ) ) & ( for n, m being Nat st n <= m holds
for x being Element of REAL st x in A holds
(F . n) . x >= (F . m) . x ) & ( for x being Element of REAL st x in A holds
( F # x is convergent & lim (F # x) = inf (F # x) & inf (F # x) >= f . x ) ) & lim F is_integrable_on B-Meas & ( for n being Nat holds I . n = Integral (B-Meas,(F . n)) ) & I is convergent & lim I = Integral (B-Meas,(lim F)) )
proof end;

theorem Th23: :: MESFUN14:23
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for E being Element of S
for n being Nat st E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 holds
M . (E /\ (great_eq_dom (f,(1 / (n + 1))))) = 0
proof end;

theorem Th24: :: MESFUN14:24
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for E being Element of S st E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 holds
M . (E /\ (great_dom (f,0))) = 0
proof end;

theorem Th25: :: MESFUN14:25
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for E being Element of S st E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 holds
f a.e.= (X --> 0) | E,M
proof end;

theorem Th26: :: MESFUN14:26
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for E1 being Element of S st M is complete & f is E1 -measurable & f a.e.= g,M & E1 = dom f holds
g is E1 -measurable
proof end;

theorem Th27: :: MESFUN14:27
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S holds E is Element of COM (S,M)
proof end;

theorem :: MESFUN14:28
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f a.e.= g,M holds
f a.e.= g, COM M
proof end;

theorem Th29: :: MESFUN14:29
for f, g being PartFunc of REAL,REAL st f a.e.= g, B-Meas holds
f a.e.= g, L-Meas
proof end;

theorem Th30: :: MESFUN14:30
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E1 being Element of S
for E2 being Element of COM (S,M)
for f being PartFunc of X,ExtREAL st E1 = E2 & f is E1 -measurable holds
f is E2 -measurable
proof end;

theorem :: MESFUN14:31
for E1 being Element of Borel_Sets
for E2 being Element of L-Field
for f being PartFunc of REAL,ExtREAL st E1 = E2 & f is E1 -measurable holds
f is E2 -measurable by Th30, MEASUR12:def 11;

theorem Th32: :: MESFUN14:32
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for F being Finite_Sep_Sequence of S holds F is Finite_Sep_Sequence of COM (S,M)
proof end;

theorem Th33: :: MESFUN14:33
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds
f is_simple_func_in COM (S,M)
proof end;

theorem Th34: :: MESFUN14:34
for X being set
for S being SigmaField of X
for M being sigma_Measure of S holds {} is thin of M
proof end;

theorem Th35: :: MESFUN14:35
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S holds M . E = (COM M) . E
proof end;

theorem Th36: :: MESFUN14:36
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative holds
integral (M,f) = integral ((COM M),f)
proof end;

theorem Th37: :: MESFUN14:37
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for E being Element of S st E = dom f & f is E -measurable & f is nonnegative holds
integral+ (M,f) = integral+ ((COM M),f)
proof end;

theorem Th38: :: MESFUN14:38
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_integrable_on M holds
( f is_integrable_on COM M & Integral (M,f) = Integral ((COM M),f) )
proof end;

theorem :: MESFUN14:39
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f, g being PartFunc of X,REAL st ( E = dom f or E = dom g ) & f a.e.= g,M holds
f - g a.e.= (X --> 0) | E,M
proof end;

theorem Th40: :: MESFUN14:40
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f, g being PartFunc of X,REAL st E = dom (f - g) & f - g a.e.= (X --> 0) | E,M holds
f | E a.e.= g | E,M
proof end;

theorem Th41: :: MESFUN14:41
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f being PartFunc of X,REAL st E = dom f & M . E < +infty & f is bounded & f is E -measurable holds
f is_integrable_on M
proof end;

theorem Th42: :: MESFUN14:42
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL holds
( f a.e.= g,M iff ( max+ f a.e.= max+ g,M & max- f a.e.= max- g,M ) )
proof end;

theorem Th43: :: MESFUN14:43
for X being non empty set
for f being PartFunc of X,REAL holds
( max+ (R_EAL f) = R_EAL (max+ f) & max- (R_EAL f) = R_EAL (max- f) )
proof end;

theorem Th44: :: MESFUN14:44
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for E being Element of S st M is complete & f is_integrable_on M & f a.e.= g,M & E = dom f & E = dom g holds
( g is_integrable_on M & Integral (M,f) = Integral (M,g) )
proof end;

Lm6: for a being Real holds {a} is Element of Borel_Sets
proof end;

theorem Th45: :: MESFUN14:45
for f being PartFunc of REAL,ExtREAL
for a being Real st a in dom f holds
ex A being Element of Borel_Sets st
( A = {a} & f is A -measurable & f | A is_integrable_on B-Meas & Integral (B-Meas,(f | A)) = 0 )
proof end;

theorem Th46: :: MESFUN14:46
for f being PartFunc of REAL,REAL
for a being Real st a in dom f holds
ex A being Element of Borel_Sets st
( A = {a} & f is A -measurable & f | A is_integrable_on B-Meas & Integral (B-Meas,(f | A)) = 0 )
proof end;

theorem :: MESFUN14:47
for f being PartFunc of REAL,ExtREAL st f is_integrable_on B-Meas holds
( f is_integrable_on L-Meas & Integral (B-Meas,f) = Integral (L-Meas,f) ) by Th38, MEASUR12:def 11, MEASUR12:def 12;

theorem Th48: :: MESFUN14:48
for f being PartFunc of REAL,REAL st f is_integrable_on B-Meas holds
( f is_integrable_on L-Meas & Integral (B-Meas,f) = Integral (L-Meas,f) )
proof end;

theorem Th49: :: MESFUN14:49
for A being non empty closed_interval Subset of REAL
for A1 being Element of L-Field
for f being PartFunc of REAL,REAL st A = A1 & A c= dom f & f || A is bounded & f is_integrable_on A holds
( f is A1 -measurable & f | A1 is_integrable_on L-Meas & integral (f || A) = Integral (L-Meas,(f | A)) )
proof end;

theorem :: MESFUN14:50
for a, b being Real
for f being PartFunc of REAL,REAL st a <= b & [.a,b.] c= dom f & f || ['a,b'] is bounded & f is_integrable_on ['a,b'] holds
integral (f,a,b) = Integral (L-Meas,(f | [.a,b.]))
proof end;