:: 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 b₁ being Division of A st b₁ divide_into_equal n by A1, Lm3;
uniqueness
for b₁, b₂ being Division of A st b₁ divide_into_equal n & b₂ divide_into_equal n holds
b₁ = b₂

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 b₃ being Division of A holds
( b₃ = EqDiv (A,n) iff b₃ 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;