0 implies Integral(M,f) = +infty; theorem :: MESFUNC9:14 Integral(M,chi(E,X)) = M.E & Integral(M,(chi(E,X))|E) = M.E; theorem :: MESFUNC9:15 E c= dom f & E c= dom g & f is_measurable_on E & g is_measurable_on E & f is nonnegative & (for x be Element of X st x in E holds f.x <= g.x) implies Integral(M,f|E) <= Integral(M,g|E); begin :: Selected Properties of Extended Real Sequence definition let s be ext-real-valued Function; func Partial_Sums s -> ExtREAL_sequence means :: MESFUNC9:def 1 it.0=s.0 & for n be Nat holds it.(n+1) = it.n + s.(n+1); end; definition let s be ext-real-valued Function; attr s is summable means :: MESFUNC9:def 2 Partial_Sums s is convergent; end; definition let s be ext-real-valued Function; func Sum s -> R_eal equals :: MESFUNC9:def 3 lim Partial_Sums s; end; theorem :: MESFUNC9:16 seq is nonnegative implies Partial_Sums seq is nonnegative & Partial_Sums seq is non-decreasing; theorem :: MESFUNC9:17 (for n be Nat holds 0 < seq.n) implies for m be Nat holds 0 < ( Partial_Sums seq).m; theorem :: MESFUNC9:18 F is with_the_same_dom & (for n be Nat holds G.n = (F.n)|D) implies G is with_the_same_dom; theorem :: MESFUNC9:19 D c= dom(F.0) & (for n be Nat holds G.n = (F.n)|D) & (for x be Element of X st x in D holds F#x is convergent) implies (lim F)|D = lim G; theorem :: MESFUNC9:20 F is with_the_same_dom & E c= dom(F.0) & (for m be Nat holds F.m is_measurable_on E & G.m= (F.m)|E) implies G.n is_measurable_on E; theorem :: MESFUNC9:21 E c= dom(F.0) & G is with_the_same_dom & (for x be Element of X st x in E holds F#x is summable) & (for n be Nat holds G.n= (F.n)|E) implies for x be Element of X st x in E holds G#x is summable; begin :: Partial Sums of Functional Sequence and their Properties definition let X be non empty set, F be Functional_Sequence of X,ExtREAL; func Partial_Sums F -> Functional_Sequence of X,ExtREAL means :: MESFUNC9:def 4 it.0 = F.0 & for n be Nat holds it.(n+1) = it.n + F.(n+1); end; definition let X be set, F be Functional_Sequence of X,ExtREAL; attr F is additive means :: MESFUNC9:def 5 for n,m be Nat st n <> m holds for x be set st x in dom(F.n) /\ dom(F.m) holds (F.n).x <> +infty or (F.m).x <> -infty; end; theorem :: MESFUNC9:22 z in dom((Partial_Sums F).n) & m <= n implies z in dom(( Partial_Sums F).m) & z in dom(F.m); theorem :: MESFUNC9:23 z in dom((Partial_Sums F).n) & ((Partial_Sums F).n).z = +infty implies ex m be Nat st m <= n & (F.m).z = +infty; theorem :: MESFUNC9:24 F is additive & z in dom((Partial_Sums F).n) & ((Partial_Sums F).n).z = +infty & m <= n implies (F.m).z <> -infty; theorem :: MESFUNC9:25 z in dom((Partial_Sums F).n) & ((Partial_Sums F).n).z = -infty implies ex m be Nat st m <= n & (F.m).z = -infty; theorem :: MESFUNC9:26 F is additive & z in dom((Partial_Sums F).n) & ((Partial_Sums F).n).z = -infty & m <= n implies (F.m).z <> +infty; theorem :: MESFUNC9:27 F is additive implies ((Partial_Sums F).n)"{-infty} /\ (F.(n+1)) "{+infty} = {} & ((Partial_Sums F).n)"{+infty} /\ (F.(n+1))"{-infty} = {}; theorem :: MESFUNC9:28 F is additive implies dom((Partial_Sums F).n) = meet{dom(F.k) where k is Element of NAT : k <= n}; theorem :: MESFUNC9:29 F is additive & F is with_the_same_dom implies dom((Partial_Sums F).n) = dom(F.0); theorem :: MESFUNC9:30 (for n be Nat holds F.n is nonnegative) implies F is additive; theorem :: MESFUNC9:31 F is additive & (for n holds G.n = (F.n)|D) implies G is additive; theorem :: MESFUNC9:32 F is additive & F is with_the_same_dom & D c= dom(F.0) & x in D implies (Partial_Sums(F#x)).n = ((Partial_Sums F)#x).n; theorem :: MESFUNC9:33 F is additive & F is with_the_same_dom & D c= dom(F.0) & x in D implies ( Partial_Sums(F#x) is convergent_to_finite_number iff (Partial_Sums F) #x is convergent_to_finite_number ) & ( Partial_Sums(F#x) is convergent_to_+infty iff (Partial_Sums F)#x is convergent_to_+infty ) & ( Partial_Sums(F#x) is convergent_to_-infty iff (Partial_Sums F)#x is convergent_to_-infty ) & ( Partial_Sums(F#x) is convergent iff (Partial_Sums F) #x is convergent ); theorem :: MESFUNC9:34 F is additive & F is with_the_same_dom & dom f c= dom(F.0) & x in dom f & F#x is summable & f.x = Sum(F#x) implies f.x = lim((Partial_Sums F)# x); theorem :: MESFUNC9:35 (for m be Nat holds F.m is_simple_func_in S) implies F is additive & (Partial_Sums F).n is_simple_func_in S; theorem :: MESFUNC9:36 (for m be Nat holds F.m is nonnegative) implies (Partial_Sums F) .n is nonnegative; theorem :: MESFUNC9:37 F is with_the_same_dom & x in dom(F.0) & (for k be Nat holds F.k is nonnegative) & n <= m implies ((Partial_Sums F).n).x <= ((Partial_Sums F).m) .x; theorem :: MESFUNC9:38 F is with_the_same_dom & x in dom(F.0) & (for m be Nat holds F.m is nonnegative) implies (Partial_Sums F)#x is non-decreasing & (Partial_Sums F) #x is convergent; theorem :: MESFUNC9:39 (for m be Nat holds F.m is without-infty) implies (Partial_Sums F).n is without-infty; theorem :: MESFUNC9:40 (for m be Nat holds F.m is without+infty) implies (Partial_Sums F).n is without+infty; theorem :: MESFUNC9:41 (for n be Nat holds F.n is_measurable_on E & F.n is without-infty) implies (Partial_Sums F).m is_measurable_on E; theorem :: MESFUNC9:42 F is additive & F is with_the_same_dom & G is additive & G is with_the_same_dom & x in dom(F.0) /\ dom(G.0) & (for k be Nat, y be Element of X st y in dom(F.0) /\ dom(G.0) holds (F.k).y <= (G.k).y) implies ((Partial_Sums F).n).x <= ((Partial_Sums G).n).x; theorem :: MESFUNC9:43 for X be non empty set, F be Functional_Sequence of X,ExtREAL st F is additive & F is with_the_same_dom holds Partial_Sums F is with_the_same_dom; theorem :: MESFUNC9:44 dom(F.0) = E & F is additive & F is with_the_same_dom & (for n be Nat holds (Partial_Sums F).n is_measurable_on E) & (for x be Element of X st x in E holds F#x is summable) implies lim(Partial_Sums F) is_measurable_on E; theorem :: MESFUNC9:45 (for n be Nat holds F.n is_integrable_on M) implies for m be Nat holds (Partial_Sums F).m is_integrable_on M; theorem :: MESFUNC9:46 E = dom(F.0) & F is additive & F is with_the_same_dom & (for n be Nat holds F.n is_measurable_on E & F.n is nonnegative & I.n = Integral(M,F.n )) implies Integral(M,(Partial_Sums F).m) = (Partial_Sums I).m; begin theorem :: MESFUNC9:47 E c= dom f & f is nonnegative & f is_measurable_on E & F is additive & (for n holds F.n is_simple_func_in S & F.n is nonnegative & E c= dom(F.n)) & ( for x st x in E holds F#x is summable & f.x = Sum(F#x)) implies ex I be ExtREAL_sequence st (for n holds I.n = Integral(M,(F.n)|E)) & I is summable & Integral(M,f|E) = Sum I; theorem :: MESFUNC9:48 E c= dom f & f is nonnegative & f is_measurable_on E implies ex g be Functional_Sequence of X,ExtREAL st g is additive & (for n be Nat holds g.n is_simple_func_in S & g.n is nonnegative & g.n is_measurable_on E) & (for x be Element of X st x in E holds g#x is summable & f.x = Sum(g#x)) & ex I be ExtREAL_sequence st (for n be Nat holds I.n = Integral(M,(g.n)|E)) & I is summable & Integral(M,f|E) = Sum I; registration let X be non empty set; cluster additive with_the_same_dom for Functional_Sequence of X,ExtREAL; end; definition let C,D,X be non empty set, F be Function of [:C,D:],PFuncs(X,ExtREAL); let c be Element of C, d be Element of D; redefine func F.(c,d) -> PartFunc of X,ExtREAL; end; definition let C,D,X be non empty set; let F be Function of [:C,D:],X; let c be Element of C; func ProjMap1(F,c) -> Function of D,X means :: MESFUNC9:def 6 for d be Element of D holds it.d = F.(c,d); end; definition let C,D,X be non empty set; let F be Function of [:C,D:],X; let d be Element of D; func ProjMap2(F,d) -> Function of C,X means :: MESFUNC9:def 7 for c be Element of C holds it.c = F.(c,d); end; definition let X,Y be set, F be Function of [:NAT,NAT:],PFuncs(X,Y), n be Nat; func ProjMap1(F,n) -> Functional_Sequence of X,Y means :: MESFUNC9:def 8 for m be Nat holds it.m = F.(n,m); func ProjMap2(F,n) -> Functional_Sequence of X,Y means :: MESFUNC9:def 9 for m be Nat holds it.m = F.(m,n); end; definition let X be non empty set, F be sequence of Funcs(NAT,PFuncs(X,ExtREAL)), n be Nat; redefine func F.n -> Functional_Sequence of X,ExtREAL; end; theorem :: MESFUNC9:49 E = dom(F.0) & F is with_the_same_dom & (for n be Nat holds F.n is nonnegative & F.n is_measurable_on E ) implies ex FF be sequence of Funcs(NAT,PFuncs(X,ExtREAL)) st for n be Nat holds (for m be Nat holds (FF.n).m is_simple_func_in S & dom((FF.n).m) = dom(F.n)) & (for m be Nat holds (FF.n).m is nonnegative) & (for j,k be Nat st j <= k holds for x be Element of X st x in dom(F.n) holds ((FF.n).j).x <= ((FF.n).k).x) & for x be Element of X st x in dom(F.n) holds (FF.n)#x is convergent & lim((FF.n)#x) = (F.n).x; theorem :: MESFUNC9:50 E = dom(F.0) & F is additive & F is with_the_same_dom & (for n be Nat holds F.n is_measurable_on E & F.n is nonnegative) implies ex I be ExtREAL_sequence st for n be Nat holds I.n = Integral(M,F.n) & Integral(M,( Partial_Sums F).n) = (Partial_Sums I).n; theorem :: MESFUNC9:51 E c= dom(F.0) & F is additive & F is with_the_same_dom & (for n be Nat holds F.n is nonnegative & F.n is_measurable_on E) & (for x be Element of X st x in E holds F#x is summable) implies ex I be ExtREAL_sequence st (for n be Nat holds I.n = Integral(M,(F.n)|E)) & I is summable & Integral(M,(lim( Partial_Sums F))|E) = Sum I; :: Lebesgue Monotone Convergence Theorem ::$N Lebesgue's Monotone Convergence Theorem theorem :: MESFUNC9:52 E = dom(F.0) & F.0 is nonnegative & F is with_the_same_dom & (for n be Nat holds F.n is_measurable_on E) & (for n,m be Nat st n <=m holds for x be Element of X st x in E holds (F.n).x <= (F.m).x ) & (for x be Element of X st x in E holds F#x is convergent) implies ex I be ExtREAL_sequence st (for n be Nat holds I.n = Integral(M,F.n)) & I is convergent & Integral(M,lim F) = lim I;