:: Lebesgue Integral of Simple Valued Function :: by Yasunari Shidama and Noboru Endou :: :: Received September 25, 2004 :: Copyright (c) 2004-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 NUMBERS, NAT_1, FUNCT_1, ZFMISC_1, FINSEQ_1, RELAT_1, CARD_3, ARYTM_3, SUBSET_1, XXREAL_0, TARSKI, XBOOLE_0, FINSEQ_2, ARYTM_1, PARTFUN1, BINOP_2, ORDINAL4, CARD_1, FUNCOP_1, PROB_1, MESFUNC2, FUNCT_3, SUPINF_2, PROB_2, MEASURE1, XXREAL_2, ORDINAL2, SUPINF_1, XREAL_0, MESFUNC1, VALUED_0, COMPLEX1, SETFAM_1, FINSET_1, FINSOP_1, INTEGRA1, REAL_1, MESFUNC3; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, XREAL_0, FINSEQ_1, SETFAM_1, FUNCOP_1, FINSOP_1, FUNCT_3, FINSET_1, PROB_1, PROB_2, XXREAL_0, XXREAL_2, XXREAL_3, NAT_1, REAL_1, XCMPLX_0, SUPINF_1, SUPINF_2, MEASURE1, FINSEQOP, FINSEQ_2, BINOP_1, BINOP_2, RVSUM_1, EXTREAL1, MESFUNC1, MESFUNC2; constructors PARTFUN1, BINOP_1, SETWISEO, REAL_1, NAT_1, FINSEQOP, PROB_2, FINSOP_1, RVSUM_1, MEASURE3, MEASURE6, EXTREAL1, MESFUNC1, BINARITH, MESFUNC2, BINOP_2, SUPINF_1, RELSET_1, NUMBERS; registrations SUBSET_1, RELAT_1, ORDINAL1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, MEASURE1, FINSET_1, VALUED_0, CARD_1, CARD_3, XXREAL_3, RELSET_1; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin :: Integral of Simple Valued Function theorem :: MESFUNC3:1 for n,m be Nat, a be Function of [:Seg n,Seg m:],REAL for p,q be FinSequence of REAL st ( dom p=Seg n & for i be Nat st i in dom p holds ex r be FinSequence of REAL st (dom r = Seg m & p.i = Sum r & for j be Nat st j in dom r holds r.j=a.[i,j])) & ( dom q=Seg m & for j be Nat st j in dom q holds ex s be FinSequence of REAL st (dom s = Seg n & q.j = Sum s & for i be Nat st i in dom s holds s.i=a.[i,j])) holds Sum p = Sum q; theorem :: MESFUNC3:2 for F be FinSequence of ExtREAL, f be FinSequence of REAL st F=f holds Sum(F)=Sum(f); theorem :: MESFUNC3:3 for X be non empty set, S be SigmaField of X, f be PartFunc of X, ExtREAL st f is_simple_func_in S holds ex F be Finite_Sep_Sequence of S, a be FinSequence of ExtREAL st dom f = union rng F & dom F= dom a & (for n be Nat st n in dom F for x be object st x in F.n holds f.x = a.n) & for x be object st x in dom f ex ax be FinSequence of ExtREAL st dom ax = dom a & for n be Nat st n in dom ax holds ax.n=a.n*(chi(F.n,X)).x; theorem :: MESFUNC3:4 for X be set, F be FinSequence of X holds F is disjoint_valued iff for i,j be Nat st i in dom F & j in dom F & i <> j holds F.i misses F.j; theorem :: MESFUNC3:5 for X be non empty set, A be set, S be SigmaField of X, F be Finite_Sep_Sequence of S, G be FinSequence of S st dom G = dom F & for i be Nat st i in dom G holds G.i = A /\ F.i holds G is Finite_Sep_Sequence of S; theorem :: MESFUNC3:6 for X be non empty set, A be set, F,G be FinSequence of X st dom G = dom F & (for i be Nat st i in dom G holds G.i = A /\ F.i) holds union rng G = A /\ union rng F; theorem :: MESFUNC3:7 for X be set, F be FinSequence of X, i be Nat st i in dom F holds F.i c= union rng F & F.i /\ union rng F = F.i; theorem :: MESFUNC3:8 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, F be Finite_Sep_Sequence of S holds dom F = dom (M*F); theorem :: MESFUNC3:9 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, F be Finite_Sep_Sequence of S holds M.(union rng F) = Sum(M*F); theorem :: MESFUNC3:10 for F,G be FinSequence of ExtREAL, a be R_eal st (a is real or ( for i be Nat st i in dom F holds F.i < 0.) or for i be Nat st i in dom F holds 0. < F.i ) & dom F = dom G & for i be Nat st i in dom G holds G.i=a*F.i holds Sum(G)=a*Sum(F); theorem :: MESFUNC3:11 for F be FinSequence of REAL holds F is FinSequence of ExtREAL; definition let X be non empty set; let S be SigmaField of X; let f be PartFunc of X,ExtREAL; let F be Finite_Sep_Sequence of S; let a be FinSequence of ExtREAL; pred F,a are_Re-presentation_of f means :: MESFUNC3:def 1 dom f = union rng F & dom F= dom a & for n be Nat st n in dom F for x be object st x in F.n holds f.x=a.n; end; theorem :: MESFUNC3:12 for X be non empty set, S be SigmaField of X, f be PartFunc of X, ExtREAL st f is_simple_func_in S ex F be Finite_Sep_Sequence of S, a be FinSequence of ExtREAL st F,a are_Re-presentation_of f; theorem :: MESFUNC3:13 for X be non empty set, S be SigmaField of X, F be Finite_Sep_Sequence of S holds ex G be Finite_Sep_Sequence of S st union rng F = union rng G & for n be Nat st n in dom G holds (G.n <> {} & ex m be Nat st m in dom F & F.m = G.n); theorem :: MESFUNC3:14 for X be non empty set, S be SigmaField of X, f be PartFunc of X ,ExtREAL st f is_simple_func_in S & f is nonnegative holds ex F be Finite_Sep_Sequence of S, a be FinSequence of ExtREAL st F,a are_Re-presentation_of f & a.1=0. & for n be Nat st 2 <= n & n in dom a holds 0. < a.n & a.n < +infty; theorem :: MESFUNC3:15 for X be non empty set, S be SigmaField of X, f be PartFunc of X, ExtREAL, F be Finite_Sep_Sequence of S, a be FinSequence of ExtREAL, x be Element of X st F,a are_Re-presentation_of f & x in dom f holds ex ax be FinSequence of ExtREAL st dom ax= dom a & (for n be Nat st n in dom ax holds ax .n=a.n*(chi(F.n,X)).x) & f.x=Sum(ax); theorem :: MESFUNC3:16 for p be FinSequence of ExtREAL, q be FinSequence of REAL st p=q holds Sum(p) = Sum(q); theorem :: MESFUNC3:17 for p be FinSequence of ExtREAL st not -infty in rng p & +infty in rng p holds Sum(p) = +infty; definition let X be non empty set; let S be SigmaField of X; let M be sigma_Measure of S; let f be PartFunc of X,ExtREAL; assume f is_simple_func_in S & f is nonnegative; func integral(M,f) -> Element of ExtREAL means :: MESFUNC3:def 2 ex F be Finite_Sep_Sequence of S, a, x be FinSequence of ExtREAL st F,a are_Re-presentation_of f & a.1 =0. & (for n be Nat st 2 <= n & n in dom a holds 0. < a.n & a.n < +infty ) & dom x = dom F & (for n be Nat st n in dom x holds x .n=a.n*(M*F).n) & it=Sum(x); end; begin :: Additional Lemma theorem :: MESFUNC3:18 for a be FinSequence of ExtREAL, p,N be Element of ExtREAL st N = len a & (for n be Nat st n in dom a holds a.n = p) holds Sum(a) = N * p;