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