:: Integral of Measurable Function :: by Noboru Endou and Yasunari Shidama :: :: Received May 24, 2006 :: Copyright (c) 2006-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, SUPINF_1, COMPLEX1, ARYTM_1, XXREAL_0, ARYTM_3, MEASURE6, NAT_1, CARD_1, NEWTON, RELAT_1, REAL_1, SUBSET_1, INT_1, PARTFUN1, FUNCT_1, SUPINF_2, XBOOLE_0, PROB_1, MESFUNC2, VALUED_0, RAT_1, MESFUNC1, TARSKI, MEASURE1, VALUED_1, RFUNCT_3, FINSEQ_1, MESFUNC3, CARD_3, ZFMISC_1, SEQ_2, ORDINAL2, XCMPLX_0, XXREAL_2, SEQFUNC, PBOOLE, INTEGRA1, FINSET_1, MEMBERED, SETLIM_1, INTEGRA5, FUNCT_3, MESFUNC5, FUNCT_7; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, XXREAL_2, XXREAL_3, REAL_1, RELAT_1, FUNCT_1, FINSEQ_1, RELSET_1, FINSET_1, PARTFUN1, FUNCT_2, INT_1, NAT_D, RAT_1, MEMBERED, SUPINF_1, SUPINF_2, MEASURE1, EXTREAL1, NAT_1, MESFUNC1, MESFUNC2, MESFUNC3, FINSEQOP, RFUNCT_3, PROB_1, MEASURE6, NEWTON, SEQFUNC, SETLIM_1, VALUED_0; constructors WELLORD2, REAL_1, SQUARE_1, NAT_D, FINSEQOP, LIMFUNC1, SEQFUNC, NEWTON, RFUNCT_3, MEASURE6, EXTREAL1, MESFUNC1, BINARITH, MESFUNC2, KURATO_0, MESFUNC3, SETLIM_1, SUPINF_1, RELSET_1, XREAL_0; registrations SUBSET_1, ORDINAL1, RELSET_1, PARTFUN1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, RAT_1, MEMBERED, COMPLEX1, FINSEQ_1, MEASURE1, VALUED_0, XXREAL_2, XXREAL_3, XCMPLX_0, NEWTON, EXTREAL1; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin theorem :: MESFUNC5:1 for x,y be R_eal holds |.x-y.| = |.y-x.|; theorem :: MESFUNC5:2 for x,y be R_eal holds y-x <= |.x-y.|; theorem :: MESFUNC5:3 for x,y be R_eal, e be Real st |.x-y.| < e & not ( x = +infty & y = +infty or x = -infty & y = -infty ) holds x <> +infty & x <> -infty & y <> +infty & y <>-infty; theorem :: MESFUNC5:4 for n be Nat, p be ExtReal st 0 <= p & p < n ex k be Nat st 1 <= k & k <= 2|^n*n & (k-1)/(2|^n) <= p & p < k/(2|^n); theorem :: MESFUNC5:5 for n,k be Nat, p be ExtReal st k <= 2|^n*n & n <= p holds k/(2|^n) <= p; theorem :: MESFUNC5:6 for x,y,k being ExtReal st 0 <= k holds k*max(x,y) = max (k*x,k*y) & k*min(x,y) = min(k*x,k*y); theorem :: MESFUNC5:7 for x,y,k being R_eal st k <= 0 holds k*min(x,y) = max(k*x,k*y) & k* max(x,y) = min(k*x,k*y); begin :: Lemmas for partial function of non empty set,extended real numbers definition let IT be set; attr IT is nonpositive means :: MESFUNC5:def 1 for x being R_eal holds x in IT implies x <= 0; end; definition let R be Relation; attr R is nonpositive means :: MESFUNC5:def 2 rng R is nonpositive; end; theorem :: MESFUNC5:8 for X being set, F being PartFunc of X,ExtREAL holds F is nonpositive iff for n being object holds F.n <= 0.; theorem :: MESFUNC5:9 for X being set, F being PartFunc of X,ExtREAL st for n being set st n in dom F holds F.n <= 0. holds F is nonpositive; definition let R be Relation; attr R is without-infty means :: MESFUNC5:def 3 not -infty in rng R; attr R is without+infty means :: MESFUNC5:def 4 not +infty in rng R; end; definition let X be non empty set, f be PartFunc of X,ExtREAL; redefine attr f is without-infty means :: MESFUNC5:def 5 for x being object holds -infty < f.x; redefine attr f is without+infty means :: MESFUNC5:def 6 for x being object holds f.x < +infty; end; theorem :: MESFUNC5:10 for X be non empty set, f be PartFunc of X,ExtREAL holds (for x be set st x in dom f holds -infty < f.x) iff f is without-infty; theorem :: MESFUNC5:11 for X be non empty set, f be PartFunc of X,ExtREAL holds (for x be set st x in dom f holds f.x < +infty) iff f is without+infty; theorem :: MESFUNC5:12 for X be non empty set, f be PartFunc of X,ExtREAL st f is nonnegative holds f is without-infty; theorem :: MESFUNC5:13 for X be non empty set, f be PartFunc of X,ExtREAL st f is nonpositive holds f is without+infty; registration let X be non empty set; cluster nonnegative -> without-infty for PartFunc of X,ExtREAL; cluster nonpositive -> without+infty for PartFunc of X,ExtREAL; end; theorem :: MESFUNC5: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 holds f is without+infty & f is without-infty ; theorem :: MESFUNC5:15 for X be non empty set, Y be set, f be PartFunc of X,ExtREAL st f is nonnegative holds f|Y is nonnegative; theorem :: MESFUNC5:16 for X be non empty set, f,g be PartFunc of X,ExtREAL st f is without-infty & g is without-infty holds dom(f+g)=dom f /\ dom g; theorem :: MESFUNC5:17 for X be non empty set, f,g be PartFunc of X,ExtREAL st f is without-infty & g is without+infty holds dom(f-g)=dom f /\ dom g; theorem :: MESFUNC5:18 for X be non empty set, S be SigmaField of X, f,g be PartFunc of X,ExtREAL, F be Function of RAT,S, r be Real, A be Element of S st f is without-infty & g is without-infty & (for p be Rational holds F.p = A /\ less_dom(f,p) /\ (A /\ less_dom(g, (r-(p qua Complex))))) holds A /\ less_dom(f+g,r) = union rng F; definition let X be non empty set; let f be PartFunc of X,REAL; func R_EAL f -> PartFunc of X,ExtREAL equals :: MESFUNC5:def 7 f; end; theorem :: MESFUNC5:19 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X,ExtREAL st f is nonnegative & g is nonnegative holds f+g is nonnegative; theorem :: MESFUNC5:20 for X be non empty set, f be PartFunc of X,ExtREAL,c be Real st f is nonnegative holds (0 <= c implies c(#)f is nonnegative) & (c <= 0 implies c(#)f is nonpositive); theorem :: MESFUNC5:21 for X be non empty set, f,g be PartFunc of X,ExtREAL st (for x be set st x in dom f /\ dom g holds g.x <= f.x & -infty < g.x & f.x < +infty) holds f-g is nonnegative; theorem :: MESFUNC5:22 for X be non empty set, f,g be PartFunc of X,ExtREAL st f is nonnegative & g is nonnegative holds dom(f+g)=dom f /\ dom g & f+g is nonnegative; theorem :: MESFUNC5:23 for X be non empty set, f,g,h be PartFunc of X,ExtREAL st f is nonnegative & g is nonnegative & h is nonnegative holds dom(f+g+h) = dom f /\ dom g /\ dom h & f+g+h is nonnegative & for x be set st x in dom f /\ dom g /\ dom h holds (f+g+h).x=f.x+g.x+h.x; theorem :: MESFUNC5:24 for X be non empty set, f,g being PartFunc of X,ExtREAL st f is without-infty & g is without-infty holds dom(max+(f+g) + max- f) = dom f /\ dom g & dom(max-(f+g) + max+ f) = dom f /\ dom g & dom(max+(f+g) + max- f + max- g) = dom f /\ dom g & dom(max-(f+g) + max+ f + max+ g) = dom f /\ dom g & max+(f+g ) + max-f is nonnegative & max-(f+g) + max+f is nonnegative; theorem :: MESFUNC5:25 for X being non empty set, f,g being PartFunc of X,ExtREAL st f is without-infty & f is without+infty & g is without-infty & g is without+infty holds max+(f+g) + max- f + max- g = max-(f+g) + max+ f + max+ g; theorem :: MESFUNC5:26 for C being non empty set, f being PartFunc of C,ExtREAL, c be Real st 0 <= c holds max+(c(#)f) = c(#)max+f & max-(c(#)f) = c(#)max-f; theorem :: MESFUNC5:27 for C being non empty set, f being PartFunc of C,ExtREAL, c be Real st 0 <= c holds max+((-c)(#)f) = c(#)max-f & max-((-c)(#)f) = c(#)max+f; theorem :: MESFUNC5:28 for X be non empty set, f be PartFunc of X,ExtREAL, A be set holds max+(f|A)=max+f|A & max-(f|A)=max-f|A; theorem :: MESFUNC5:29 for X be non empty set, f,g be PartFunc of X,ExtREAL, B be set st B c= dom(f+g) holds dom((f+g)|B) =B & dom(f|B+g|B)=B & (f+g)|B = f|B+g|B; theorem :: MESFUNC5:30 for X be non empty set, f be PartFunc of X,ExtREAL, a be R_eal holds eq_dom(f,a) = f"{a}; begin :: Lemmas for measurable function and simple valued function theorem :: MESFUNC5:31 for X be non empty set, S be SigmaField of X, f,g be PartFunc of X,ExtREAL, A be Element of S st f is without-infty & g is without-infty & f is A-measurable & g is A-measurable holds f+g is A-measurable; theorem :: MESFUNC5:32 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 & dom f = {} holds 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) & Sum x = 0; theorem :: MESFUNC5:33 for X be non empty set, S be SigmaField of X, f be PartFunc of X ,ExtREAL, A be Element of S, r,s be Real st f is A-measurable & A c= dom f holds A /\ great_eq_dom(f, r) /\ less_dom(f, s) in S; theorem :: MESFUNC5:34 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL, A be Element of S st f is_simple_func_in S holds f|A is_simple_func_in S; theorem :: MESFUNC5:35 for X be non empty set, S be SigmaField of X, A be Element of S, F be Finite_Sep_Sequence of S, G be FinSequence st dom F = dom G & (for n be Nat st n in dom F holds G.n = F.n /\ A) holds G is Finite_Sep_Sequence of S; theorem :: MESFUNC5:36 for X be non empty set, S be SigmaField of X, f be PartFunc of X ,ExtREAL, A be Element of S, F,G be Finite_Sep_Sequence of S, a be FinSequence of ExtREAL st dom F = dom G & (for n be Nat st n in dom F holds G.n = F.n /\ A) & F,a are_Re-presentation_of f holds G,a are_Re-presentation_of f|A; theorem :: MESFUNC5:37 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 dom f is Element of S; theorem :: MESFUNC5:38 for X be non empty set, S be SigmaField of X, f,g be PartFunc of X,ExtREAL st f is_simple_func_in S & g is_simple_func_in S holds f+g is_simple_func_in S; theorem :: MESFUNC5:39 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL,c be Real st f is_simple_func_in S holds c(#)f is_simple_func_in S; theorem :: MESFUNC5:40 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X,ExtREAL st f is_simple_func_in S & g is_simple_func_in S & (for x be object st x in dom(f-g) holds g.x <= f.x) holds f-g is nonnegative; theorem :: MESFUNC5:41 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, A be Element of S, c be R_eal st c <> +infty & c <> -infty holds ex f be PartFunc of X,ExtREAL st f is_simple_func_in S & dom f = A & for x be object st x in A holds f.x=c; theorem :: MESFUNC5:42 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL, B,BF be Element of S st f is B-measurable & BF = dom f /\ B holds f|B is BF-measurable; theorem :: MESFUNC5:43 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, A be Element of S, f,g being PartFunc of X,ExtREAL st A c= dom f & f is A-measurable & g is A-measurable & f is without-infty & g is without-infty holds max+(f+g) + max-f is A-measurable; theorem :: MESFUNC5:44 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, A be Element of S, f,g being PartFunc of X,ExtREAL st A c= dom f /\ dom g & f is A-measurable & g is A-measurable & f is without-infty & g is without-infty holds max-(f+g) + max+f is A-measurable; theorem :: MESFUNC5:45 for X be non empty set, S being SigmaField of X, M being sigma_Measure of S, A being set st A in S holds 0 <= M.A; theorem :: MESFUNC5:46 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X,ExtREAL st (ex E1 be Element of S st E1=dom f & f is E1-measurable) & (ex E2 be Element of S st E2=dom g & g is E2-measurable ) & f"{+infty} in S & f"{-infty} in S & g"{+infty} in S & g"{-infty} in S holds dom(f+g) in S; theorem :: MESFUNC5:47 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X,ExtREAL st (ex E1 be Element of S st E1=dom f & f is E1-measurable) & (ex E2 be Element of S st E2=dom g & g is E2-measurable ) holds ex E be Element of S st E=dom(f+g) & (f+g) is E-measurable; theorem :: MESFUNC5:48 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL, A,B be Element of S st dom f = A holds f is B-measurable iff f is (A/\B)-measurable; theorem :: MESFUNC5:49 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL st ( ex A be Element of S st dom f = A ) for c be Real, B be Element of S st f is B-measurable holds c(#)f is B-measurable; begin :: Sequence of extended real numbers definition mode ExtREAL_sequence is sequence of ExtREAL; end; definition let seq be ExtREAL_sequence; attr seq is convergent_to_finite_number means :: MESFUNC5:def 8 ex g be Real st for p be Real st 0

R_eal means :: MESFUNC5:def 12 ( ex g be Real st it = g & (for p be Real st 0

+infty & (for n be Nat holds L.n <= K) holds sup rng L < +infty; theorem :: MESFUNC5:59 for L be ExtREAL_sequence st L is without-infty holds sup rng L <> +infty iff ex K be Real st 0 ExtREAL_sequence means :: MESFUNC5:def 13 for n be Nat holds it.n = (H.n).x; end; definition let D1,D2 be set, F be sequence of PFuncs(D1,D2), n be Nat; redefine func F.n -> PartFunc of D1,D2; end; theorem :: MESFUNC5:64 for X be non empty set, S be SigmaField of X, f be PartFunc of X,ExtREAL st (ex A be Element of S st A = dom f & f is A-measurable) & f qua ext-real-valued Function is nonnegative ex F be Functional_Sequence of X,ExtREAL st (for n be Nat holds F.n is_simple_func_in S & dom(F.n) = dom f) & (for n be Nat holds F.n is nonnegative) & (for n,m be Nat st n <=m holds for x be Element of X st x in dom f holds (F.n).x <= (F.m).x ) & for x be Element of X st x in dom f holds (F#x) is convergent & lim(F#x) = f.x; begin :: Integral of non negative simple valued function 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; func integral'(M,f) -> Element of ExtREAL equals :: MESFUNC5:def 14 integral(M,f) if dom f <> {} otherwise 0.; end; theorem :: MESFUNC5:65 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X,ExtREAL st f is_simple_func_in S & g is_simple_func_in S & f is nonnegative & g is nonnegative holds dom(f+g) = dom f /\ dom g & integral'(M,f+g) = integral'(M,f|dom(f+g)) + integral'(M,g|dom(f+g )); theorem :: MESFUNC5:66 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL,c be Real st f is_simple_func_in S & f is nonnegative & 0 <= c holds integral'(M,c(#)f) = (c)*integral'(M,f); theorem :: MESFUNC5:67 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL, A,B be Element of S st f is_simple_func_in S & f is nonnegative & A misses B holds integral'(M,f|(A\/B)) = integral'(M,f|A) + integral'(M,f|B); theorem :: MESFUNC5:68 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 0 <= integral'(M,f); theorem :: MESFUNC5:69 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative & g is_simple_func_in S & g is nonnegative & (for x be object st x in dom(f-g) holds g.x <= f.x) holds dom (f-g) = dom f /\ dom g & integral'(M,f|dom(f-g))= integral'(M,f-g)+integral'(M,g|dom(f-g)); theorem :: MESFUNC5:70 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X,ExtREAL st f is_simple_func_in S & g is_simple_func_in S & f is nonnegative & g is nonnegative & (for x be object st x in dom(f-g) holds g.x <= f.x) holds integral'(M,g|dom(f-g)) <= integral'(M,f| dom(f-g)); theorem :: MESFUNC5:71 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL, c be R_eal st 0 <= c & f is_simple_func_in S & (for x be object st x in dom f holds f.x=c) holds integral'(M,f) = c*(M.(dom f)); theorem :: MESFUNC5:72 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|eq_dom(f,0)) = 0; theorem :: MESFUNC5:73 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, B be Element of S, f be PartFunc of X,ExtREAL st f is_simple_func_in S & M.B=0 & f is nonnegative holds integral'(M,f|B) = 0; theorem :: MESFUNC5:74 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, g be PartFunc of X,ExtREAL, F be Functional_Sequence of X,ExtREAL, L be ExtREAL_sequence st g is_simple_func_in S & (for x be object st x in dom g holds 0 < g.x) & (for n be Nat holds F.n is_simple_func_in S) & (for n be Nat holds dom (F.n) = dom g) & (for n be Nat holds F.n is nonnegative) & (for n,m be Nat st n <=m holds for x be Element of X st x in dom g holds (F.n).x <= (F.m).x ) & (for x be Element of X st x in dom g holds (F#x) is convergent & g.x <= lim(F#x) ) & (for n be Nat holds L.n = integral'(M,F.n)) holds L is convergent & integral'(M ,g) <= lim(L); theorem :: MESFUNC5:75 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, g be PartFunc of X,ExtREAL, F be Functional_Sequence of X,ExtREAL st g is_simple_func_in S & g is nonnegative & (for n be Nat holds F.n is_simple_func_in S) & (for n be Nat holds dom(F.n) = dom g) & (for n be Nat holds F.n is nonnegative) & (for n,m be Nat st n <=m holds for x be Element of X st x in dom g holds (F.n).x <= (F.m).x ) & (for x be Element of X st x in dom g holds (F#x) is convergent & g.x <= lim(F#x) ) holds ex G be ExtREAL_sequence st (for n be Nat holds G.n = integral'(M,F.n)) & G is convergent & sup(rng G)= lim (G) & integral'(M,g) <= lim(G); theorem :: MESFUNC5:76 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, A be Element of S, F,G be Functional_Sequence of X,ExtREAL, K,L be ExtREAL_sequence st (for n be Nat holds F.n is_simple_func_in S & dom(F.n)=A ) & (for n be Nat holds F.n is nonnegative) & (for n,m be Nat st n <=m holds for x be Element of X st x in A holds (F.n).x <= (F.m).x ) & (for n be Nat holds G. n is_simple_func_in S & dom(G.n)=A) & (for n be Nat holds G.n is nonnegative) & (for n,m be Nat st n <=m holds for x be Element of X st x in A holds (G.n).x <= (G.m).x ) & (for x be Element of X st x in A holds F#x is convergent & G#x is convergent & lim(F#x) = lim(G#x)) & (for n be Nat holds K.n=integral'(M,F.n) & L.n=integral'(M,G.n)) holds K is convergent & L is convergent & lim K = lim L ; 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 that ex A be Element of S st A = dom f & f is A-measurable and f is nonnegative; func integral+(M,f) -> Element of ExtREAL means :: MESFUNC5:def 15 ex F be Functional_Sequence of X,ExtREAL, K be ExtREAL_sequence st (for n be Nat holds F.n is_simple_func_in S & dom(F.n) = dom f) & (for n be Nat holds F.n is nonnegative) & (for n,m be Nat st n <=m holds for x be Element of X st x in dom f holds (F.n).x <= (F.m).x ) & (for x be Element of X st x in dom f holds F#x is convergent & lim(F#x) = f.x) & (for n be Nat holds K.n=integral'(M,F.n)) & K is convergent & it=lim K; end; theorem :: MESFUNC5:77 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'(M,f); theorem :: MESFUNC5:78 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X,ExtREAL st ( ex A be Element of S st A = dom f & f is A-measurable ) & ( ex B be Element of S st B = dom g & g is B-measurable ) & f is nonnegative & g is nonnegative holds ex C be Element of S st C = dom (f+g) & integral+(M,f+g) = integral+(M,f|C) + integral+(M,g|C); theorem :: MESFUNC5:79 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL st (ex A be Element of S st A = dom f & f is A-measurable) & f is nonnegative holds 0 <= integral+(M,f); theorem :: MESFUNC5:80 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL, A be Element of S st (ex E be Element of S st E = dom f & f is E-measurable ) & f is nonnegative holds 0<= integral+(M,f|A ); theorem :: MESFUNC5:81 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL, A,B be Element of S st (ex E be Element of S st E = dom f & f is E-measurable) & f is nonnegative & A misses B holds integral+(M,f|(A\/B)) = integral+(M,f|A)+integral+(M,f|B); theorem :: MESFUNC5:82 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL, A be Element of S st (ex E be Element of S st E = dom f & f is E-measurable ) & f is nonnegative & M.A = 0 holds integral+ (M,f|A) = 0; theorem :: MESFUNC5:83 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL, A,B be Element of S st (ex E be Element of S st E = dom f & f is E-measurable ) & f is nonnegative & A c= B holds integral+(M,f|A) <= integral+(M,f|B); theorem :: MESFUNC5:84 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL, E,A be Element of S st f is nonnegative & E = dom f & f is E-measurable & M.A =0 holds integral+(M,f|(E\A)) = integral+(M, f); theorem :: MESFUNC5:85 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X,ExtREAL st (ex E be Element of S st E = dom f & E= dom g & f is E-measurable & g is E-measurable) & f is nonnegative & g is nonnegative & (for x be Element of X st x in dom g holds g.x <= f.x) holds integral+(M,g) <= integral+(M,f); theorem :: MESFUNC5:86 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL, c be Real st 0 <= c & (ex A be Element of S st A = dom f & f is A-measurable) & f is nonnegative holds integral+(M,c(#)f ) = c * integral+(M,f); theorem :: MESFUNC5:87 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL st (ex A be Element of S st A = dom f & f is A-measurable) & (for x be Element of X st x in dom f holds 0= f.x) holds integral+(M,f) = 0; begin :: Integral of measurable function 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; ::$N Lebesgue Measure and Integration ::$N Integral of Measurable Function func Integral(M,f) -> Element of ExtREAL equals :: MESFUNC5:def 16 integral+(M,max+f)-integral+ (M,max-f); end; theorem :: MESFUNC5:88 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL st (ex A be Element of S st A = dom f & f is A-measurable) & f is nonnegative holds Integral(M,f) =integral+(M,f); theorem :: MESFUNC5:89 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+(M,f) & Integral(M,f) = integral'(M,f); theorem :: MESFUNC5:90 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL st (ex A be Element of S st A = dom f & f is A-measurable) & f is nonnegative holds 0 <= Integral(M,f); theorem :: MESFUNC5:91 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL, A,B be Element of S st (ex E be Element of S st E = dom f & f is E-measurable ) & f is nonnegative & A misses B holds Integral(M ,f|(A\/B)) = Integral(M,f|A)+Integral(M,f|B); theorem :: MESFUNC5:92 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL, A be Element of S st (ex E be Element of S st E = dom f & f is E-measurable ) & f is nonnegative holds 0<= Integral(M,f|A); theorem :: MESFUNC5:93 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL, A,B be Element of S st (ex E be Element of S st E = dom f & f is E-measurable ) & f is nonnegative & A c= B holds Integral(M,f|A ) <= Integral(M,f|B); theorem :: MESFUNC5:94 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL, A be Element of S st (ex E be Element of S st E = dom f & f is E-measurable) & M.A = 0 holds Integral(M,f|A)=0; theorem :: MESFUNC5:95 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL, E,A be Element of S st E = dom f & f is E-measurable & M.A =0 holds Integral(M,f|(E\A)) = Integral(M,f); 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; pred f is_integrable_on M means :: MESFUNC5:def 17 (ex A be Element of S st A = dom f & f is A-measurable ) & integral+(M,max+ f) < +infty & integral+(M,max- f) < +infty; end; theorem :: MESFUNC5:96 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 0 <= integral+(M,max+f) & 0 <= integral+(M,max-f) & -infty < Integral(M,f) & Integral(M,f) < +infty; theorem :: MESFUNC5:97 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL, A be Element of S st f is_integrable_on M holds integral+(M,max+(f|A)) <= integral+(M,max+ f) & integral+(M,max-(f|A)) <= integral+(M,max- f) & f|A is_integrable_on M; theorem :: MESFUNC5:98 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL, A,B be Element of S st f is_integrable_on M & A misses B holds Integral(M,f|(A\/B)) = Integral(M,f|A) + Integral(M,f|B); theorem :: MESFUNC5:99 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL, A,B be Element of S st f is_integrable_on M & B = ( dom f)\A holds f|A is_integrable_on M & Integral(M,f) = Integral(M,f|A)+ Integral(M,f|B); theorem :: MESFUNC5:100 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL st (ex A be Element of S st A = dom f & f is A-measurable ) holds f is_integrable_on M iff |.f.| is_integrable_on M; theorem :: MESFUNC5:101 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 |. Integral(M,f) .| <= Integral(M,|.f.|); theorem :: MESFUNC5:102 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X,ExtREAL st ( ex A be Element of S st A = dom f & f is A-measurable ) & dom f = dom g & g is_integrable_on M & ( for x be Element of X st x in dom f holds |.f.x .| <= g.x ) holds f is_integrable_on M & Integral(M,|.f.|) <= Integral(M,g); theorem :: MESFUNC5:103 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL, r be Real st dom f in S & 0 <= r & dom f <> {} & (for x be object st x in dom f holds f.x = r) holds integral(M,f) = r * M.(dom f); theorem :: MESFUNC5:104 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL, r be Real st dom f in S & 0 <= r & (for x be object st x in dom f holds f.x = r) holds integral'(M,f) = r * M.(dom f); theorem :: MESFUNC5:105 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" {+infty} in S & f"{-infty} in S & M.(f"{+infty})=0 & M.(f"{-infty})=0 & f"{ +infty} \/ f"{-infty} in S & M.(f"{+infty} \/ f"{-infty})=0; theorem :: MESFUNC5:106 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M & f is nonnegative & g is nonnegative holds f+g is_integrable_on M; theorem :: MESFUNC5:107 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds dom (f+g) in S; theorem :: MESFUNC5:108 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds f+g is_integrable_on M; theorem :: MESFUNC5:109 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds ex E be Element of S st E = dom f /\ dom g & Integral(M,f+g)=Integral(M,f |E)+Integral(M,g|E); theorem :: MESFUNC5:110 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL, c be Real st f is_integrable_on M holds c(#)f is_integrable_on M & Integral(M,c(#)f) = c * Integral(M,f); 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; let B be Element of S; func Integral_on(M,B,f) -> Element of ExtREAL equals :: MESFUNC5:def 18 Integral(M,f|B); end; theorem :: MESFUNC5:111 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X,ExtREAL, B be Element of S st f is_integrable_on M & g is_integrable_on M & B c= dom(f+g) holds f+g is_integrable_on M & Integral_on(M ,B,f+g) = Integral_on(M,B,f) + Integral_on(M,B,g); theorem :: MESFUNC5:112 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,ExtREAL, c be Real, B be Element of S st f is_integrable_on M holds f|B is_integrable_on M & Integral_on(M,B,c(#)f) = c * Integral_on (M,B,f);