:: Relationship between the {R}iemann and {L}ebesgue Integrals
:: by Noboru Endou
::
:: Received September 30, 2021
:: Copyright (c) 2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FUNCT_1, NUMBERS, SUBSET_1, SUPINF_2, ARYTM_3, CARD_1, RELAT_1,
TARSKI, ORDINAL2, XXREAL_0, NAT_1, XXREAL_2, ORDINAL1, XBOOLE_0,
FUNCOP_1, MEASURE5, SUPINF_1, REAL_1, PROB_1, MEASURE1, MEASURE7,
XCMPLX_0, XXREAL_1, ARYTM_1, CARD_3, FINSEQ_1, ORDINAL4, VALUED_0,
MESFUNC5, SEQ_2, NEWTON, COMPLEX1, SEQ_1, MEASURE3, REWRITE1, MEASUR12,
PARTFUN1, INTEGRA1, INTEGRA2, INTEGRA4, MEMBERED, MESFUNC8, INTEGRA5,
REALSET1, MESFUNC1, MEASURE6, SEQ_4, SEQFUNC, MESFUNC2, RFUNCT_3,
MESFUNC3, FINSEQ_2, PBOOLE, MESFUN10, MESFUN14, FUNCT_3, FDIFF_1, POWER,
VALUED_1, MEASURE2, LPSPACE1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, SEQ_1, FUNCOP_1, FUNCT_1,
RELSET_1, PARTFUN1, VALUED_1, FINSEQ_1, FINSEQ_2, RVSUM_1, SEQ_2, SEQ_4,
VALUED_0, FUNCT_2, XXREAL_2, XXREAL_1, XXREAL_0, MEMBERED, MEASURE3,
XXREAL_3, XCMPLX_0, EXTREAL1, COMPLEX1, XREAL_0, NUMBERS, MEASURE2,
SUPINF_1, RFUNCT_3, RINFSUP2, SUPINF_2, NAT_1, RCOMP_1, MEASURE1,
MEASURE5, MESFUNC1, MESFUNC2, MESFUNC3, MESFUNC6, MESFUNC5, MESFUNC8,
MESFUN10, PROB_1, NAT_D, PROB_3, NEWTON, MEASUR12, INTEGRA1, INTEGRA2,
POWER, RFUNCT_1, FDIFF_1, INTEGRA3, INTEGRA4, INTEGRA5, SEQFUNC,
LPSPACE1;
constructors SUPINF_1, MEASURE6, EXTREAL1, PROB_3, RVSUM_1, FINSEQOP,
MEASUR11, SEQ_4, NEWTON, COMSEQ_2, MEASUR12, INTEGRA2, INTEGRA4,
INTEGRA5, NAT_D, MESFUNC6, MESFUNC2, SEQFUNC, MESFUNC3, MESFUNC8,
MESFUN10, RINFSUP2, INTEGRA3, FDIFF_1, LPSPACE1, PROB_4;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, FUNCT_2, NUMBERS, XREAL_0,
MEMBERED, MEASURE1, VALUED_0, XXREAL_2, RELSET_1, MEASURE5, NAT_1,
FINSEQ_1, RELAT_1, FINSET_1, XXREAL_0, CARD_1, XXREAL_1, ZFMISC_1,
FUNCOP_1, XXREAL_3, MEASURE3, MEASUR12, INTEGRA1, PARTFUN1, SEQ_4,
NEWTON, SEQM_3, MESFUNC8;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
begin
theorem :: MESFUN14:1
for X be non empty set, f be PartFunc of X,ExtREAL holds
rng max+f c= rng f \/ {0} & rng max-f c= rng (-f) \/ {0};
theorem :: MESFUN14:2
for X be non empty set, f be PartFunc of X,ExtREAL st f is real-valued
holds -f is real-valued & max+f is real-valued & max-f is real-valued;
theorem :: MESFUN14:3
for X be non empty set, f be PartFunc of X,ExtREAL st
f is without-infty without+infty holds f is PartFunc of X,REAL;
theorem :: MESFUN14:4
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be 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;
theorem :: MESFUN14:5
for a,b be 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;
theorem :: MESFUN14:6
for a,b be 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;
theorem :: MESFUN14:7
for A1 be Element of Borel_Sets, A2 be Element of L-Field,
f be PartFunc of REAL,ExtREAL
st A1 = A2 & f is A1-measurable holds f is A2-measurable;
theorem :: MESFUN14:8
for a,b be Real, A be non empty closed_interval Subset of REAL
st a < b & A = [.a,b.] holds
for n be Nat st n > 0 ex D be Division of A st D divide_into_equal n;
definition
let F be FinSequence of Borel_Sets;
let n be Nat;
redefine func F.n -> ext-real-membered set;
end;
theorem :: MESFUN14:9
for a,b be Real, A be non empty closed_interval Subset of REAL,
D be Division of A st A = [.a,b.] holds
ex F be Finite_Sep_Sequence of Borel_Sets
st dom D = dom F
& union rng F = A
& for k be 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 < len D implies F.k = [. D.(k-'1), D.k .[)
& (k = len D implies F.k = [. D.(k-'1), D.k.]));
theorem :: MESFUN14:10
for a,b be Real, A be non empty closed_interval Subset of REAL,
D be Division of A, f be PartFunc of A,REAL st A = [.a,b.] holds
ex F be Finite_Sep_Sequence of Borel_Sets, g be PartFunc of REAL,ExtREAL
st dom F = dom D
& union rng F = A
& (for k be 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 < 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 be Real st x in dom g holds
ex k be Nat st 1 <= k <= len F & x in F.k
& g.x = lower_bound rng(f|divset(D,k));
theorem :: MESFUN14:11
for a,b be Real, A be non empty closed_interval Subset of REAL,
D be Division of A, f be PartFunc of A,REAL st A = [.a,b.] holds
ex F be Finite_Sep_Sequence of Borel_Sets, g be PartFunc of REAL,ExtREAL
st dom F = dom D
& union rng F = A
& (for k be 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 < 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 be Real st x in dom g holds
ex k be Nat st 1 <= k <= len F & x in F.k
& g.x = upper_bound rng(f|divset(D,k));
theorem :: MESFUN14:12
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, F be Finite_Sep_Sequence of S,
a be FinSequence of ExtREAL, n be Nat
st f is_simple_func_in S & F,a are_Re-presentation_of f & n in dom F
holds F.n = {} or a.n is Real;
definition
let A be non empty closed_interval Subset of REAL;
let n be Nat;
assume n > 0 & vol A > 0;
func EqDiv(A,n) -> Division of A means
:: MESFUN14:def 1
it divide_into_equal n;
end;
theorem :: MESFUN14:13
for A be non empty closed_interval Subset of REAL, n be Nat st
vol A > 0 & len EqDiv(A,2|^n) = 1 holds n = 0;
theorem :: MESFUN14:14
for a,b be Real, A be non empty closed_interval Subset of REAL
st a < b & A = [.a,b.] holds
ex D be DivSequence of A st
for n be Nat holds D.n divide_into_equal 2|^n;
theorem :: MESFUN14:15
for A be non empty closed_interval Subset of REAL, D be Division of A,
n,k be Nat st D divide_into_equal n & k in dom D
holds vol divset(D,k) = (vol A)/n;
theorem :: MESFUN14:16
for x be Complex, r be natural Number st x <> 0 holds (x|^r)" = x"|^r;
theorem :: MESFUN14:17
for A be non empty closed_interval Subset of REAL, T be sequence of divs A st
vol A > 0 & (for n be Nat holds T.n = EqDiv(A,2|^n)) holds
delta T is 0-convergent non-zero;
theorem :: MESFUN14:18
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S,
f be PartFunc of X,ExtREAL, F be Finite_Sep_Sequence of S,
a,x be 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 be Nat st i in dom x holds x.i=a.i*(M*F).i)
holds Integral(M,f)=Sum(x);
theorem :: MESFUN14:19
for A be non empty closed_interval Subset of REAL, f be PartFunc of A,REAL,
D be Division of A st f is bounded & A c= dom f holds
ex F be Finite_Sep_Sequence of Borel_Sets,
g be PartFunc of REAL,ExtREAL st
dom F = dom D
& union rng F = A
& (for k be 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 < 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 be Real st x in dom g holds
ex k be Nat st 1 <= 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 be Real st x in A holds lower_bound rng f <= g.x <= f.x;
theorem :: MESFUN14:20
for A be non empty closed_interval Subset of REAL, f be PartFunc of A,REAL,
D be Division of A st f is bounded & A c= dom f holds
ex F be Finite_Sep_Sequence of Borel_Sets,
g be PartFunc of REAL,ExtREAL st
dom F = dom D
& union rng F = A
& (for k be 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 < 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 be Real st x in dom g holds
ex k be Nat st 1 <= 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 be Real st x in A holds upper_bound rng f >= g.x >= f.x;
theorem :: MESFUN14:21
for A be non empty closed_interval Subset of REAL, f be PartFunc of A,REAL
st f is bounded & A c= dom f & vol A > 0 holds
ex F be with_the_same_dom Functional_Sequence of REAL,ExtREAL,
I be ExtREAL_sequence st
A = dom(F.0)
& (for n be Nat holds
F.n is_simple_func_in Borel_Sets
& Integral(B-Meas,F.n) = lower_sum(f,EqDiv(A,2|^n))
& (for x be Real st x in A holds lower_bound rng f <= (F.n).x <= f.x) )
& (for n,m be Nat st n <= m holds for x be Element of REAL st x in A holds
(F.n).x <= (F.m).x)
& (for x be 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 be Nat holds I.n = Integral(B-Meas,F.n))
& I is convergent & lim I = Integral(B-Meas,lim F);
theorem :: MESFUN14:22
for A be non empty closed_interval Subset of REAL, f be PartFunc of A,REAL
st f is bounded & A c= dom f & vol A > 0 holds
ex F be with_the_same_dom Functional_Sequence of REAL,ExtREAL,
I be ExtREAL_sequence st
A = dom(F.0)
& (for n be Nat holds
F.n is_simple_func_in Borel_Sets
& Integral(B-Meas,F.n) = upper_sum(f,EqDiv(A,2|^n))
& (for x be Real st x in A holds upper_bound rng f >= (F.n).x >= f.x) )
& (for n,m be Nat st n <= m holds for x be Element of REAL st x in A holds
(F.n).x >= (F.m).x)
& (for x be 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 be Nat holds I.n = Integral(B-Meas,F.n))
& I is convergent & lim I = Integral(B-Meas,lim F);
begin :: Properties of Complete Measure Space
theorem :: MESFUN14:23
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, E be Element of S, n be 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;
theorem :: MESFUN14:24
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, E be 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;
theorem :: MESFUN14:25
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,REAL, E be 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;
theorem :: MESFUN14:26
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f,g be PartFunc of X,REAL, E1 be Element of S
st M is complete & f is E1-measurable & f a.e.= g,M & E1 = dom f
holds g is E1-measurable;
theorem :: MESFUN14:27
for X be set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S holds E is Element of COM(S,M);
theorem :: MESFUN14:28
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f,g be PartFunc of X,REAL st f a.e.= g,M holds f a.e.= g,COM M;
theorem :: MESFUN14:29
for f,g be PartFunc of REAL,REAL st f a.e.= g,B-Meas holds f a.e.= g,L-Meas;
theorem :: MESFUN14:30
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
E1 be Element of S, E2 be Element of COM(S,M), f be PartFunc of X,ExtREAL
st E1 = E2 & f is E1-measurable holds f is E2-measurable;
theorem :: MESFUN14:31
for E1 be Element of Borel_Sets,
E2 be Element of L-Field, f be PartFunc of REAL,ExtREAL
st E1 = E2 & f is E1-measurable holds f is E2-measurable;
theorem :: MESFUN14:32
for X be set, S be SigmaField of X, M be sigma_Measure of S,
F be Finite_Sep_Sequence of S
holds F is Finite_Sep_Sequence of COM(S,M);
theorem :: MESFUN14:33
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL st f is_simple_func_in S holds
f is_simple_func_in COM(S,M);
theorem :: MESFUN14:34
for X be set, S be SigmaField of X, M be sigma_Measure of S
holds {} is thin of M;
theorem :: MESFUN14:35
for X be set, S be SigmaField of X, M be sigma_Measure of S, E be Element of S
holds M.E = (COM M).E;
theorem :: MESFUN14:36
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative
holds integral(M,f) = integral(COM M,f);
theorem :: MESFUN14:37
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, E be Element of S
st E = dom f & f is E-measurable & f is nonnegative
holds integral+(M,f) = integral+(COM M,f);
theorem :: MESFUN14:38
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL st f is_integrable_on M
holds f is_integrable_on (COM M) & Integral(M,f) = Integral(COM M,f);
begin :: Relation Between Riemann and Lebesgue Integrals
theorem :: MESFUN14:39
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S, f,g be 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;
theorem :: MESFUN14:40
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S, f,g be 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;
theorem :: MESFUN14:41
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S, f be PartFunc of X,REAL st E = dom f &
M.E < +infty & f is bounded & f is E-measurable
holds f is_integrable_on M;
theorem :: MESFUN14:42
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f,g be 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;
theorem :: MESFUN14:43
for X be non empty set, f be PartFunc of X,REAL holds
max+(R_EAL f) = R_EAL(max+f) & max-(R_EAL f) = R_EAL(max-f);
theorem :: MESFUN14:44
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f,g be PartFunc of X,REAL, E be 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);
theorem :: MESFUN14:45
for f be PartFunc of REAL,ExtREAL, a be Real st a in dom f
ex A be Element of Borel_Sets
st A = {a} & f is A-measurable & f|A is_integrable_on B-Meas &
Integral(B-Meas,f|A) = 0;
theorem :: MESFUN14:46
for f be PartFunc of REAL,REAL, a be Real st a in dom f
ex A be Element of Borel_Sets
st A = {a} & f is A-measurable & f|A is_integrable_on B-Meas &
Integral(B-Meas,f|A) = 0;
theorem :: MESFUN14:47
for f be 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);
theorem :: MESFUN14:48
for f be 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);
theorem :: MESFUN14:49
for A be non empty closed_interval Subset of REAL, A1 be Element of L-Field,
f be 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);
theorem :: MESFUN14:50
for a,b be Real, f be 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.]);