:: The First Mean Value Theorem for Integrals :: by Keiko Narita , Noboru Endou and Yasunari Shidama :: :: Received October 30, 2007 :: Copyright (c) 2007 Association of Mizar Users environ vocabularies PARTFUN1, MEASURE1, FINSEQ_1, RELAT_1, ABSVALUE, FUNCT_1, ORDINAL2, LATTICES, FINSEQ_2, FINSEQ_4, CARD_3, BINOP_1, SETWISEO, COMPLEX1, SEQ_1, SEQ_2, MEASURE6, BOOLE, ARYTM, ARYTM_1, POWER, MESFUNC1, TARSKI, ARYTM_3, SQUARE_1, RLVECT_1, GROUP_1, PROB_1, INTEGRA1, MESFUNC2, MESFUNC5, SUPINF_1, SUPINF_2, MESFUNC7, FUNCT_3, RFUNCT_3, FINSET_1, VALUED_0, XXREAL_2; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, VALUED_0, XREAL_0, REAL_1, XXREAL_0, XXREAL_2, MEASURE1, NAT_1, COMPLEX1, SUPINF_1, RELAT_1, RELSET_1, SETWISEO, PARTFUN1, FINSEQ_1, FINSEQ_2, SETWOP_2, BINOP_1, FUNCT_2, NEWTON, SQUARE_1, PROB_1, SUPINF_2, EXTREAL1, POWER, MESFUNC5, MESFUNC1, MESFUNC2, MEASURE6; constructors REAL_1, NAT_1, DOMAIN_1, FINSOP_1, EXTREAL1, BINOP_1, NEWTON, POWER, MESFUNC1, MEASURE6, MESFUNC2, MEASURE3, SETWISEO, EXTREAL2, SQUARE_1, MESFUNC5, SUPINF_1; registrations SUBSET_1, NAT_1, RELSET_1, XREAL_0, MEMBERED, ORDINAL1, FINSEQ_1, MEASURE1, NUMBERS, XXREAL_0, XCMPLX_0, XBOOLE_0, VALUED_0, POWER; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; definitions TARSKI, MESFUNC1, MEASURE6, MESFUNC5, XCMPLX_0, NUMBERS; theorems ABSVALUE, SETWISEO, POWER, HOLDER_1, TARSKI, SUPINF_1, PARTFUN1, FUNCT_1, SUPINF_2, EXTREAL1, EXTREAL2, BINOP_1, MESFUNC1, FINSEQ_1, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_1, MESFUNC2, NEWTON, XREAL_1, SQUARE_1, COMPLEX1, XXREAL_0, REAL_2, FINSEQ_2, MESFUNC5, FINSOP_1, NAT_1, RELAT_1, FUNCT_3, MEASURE1, MESFUNC6, MEASURE6, ORDINAL1, VALUED_0, XXREAL_2; schemes FUNCT_2, NAT_1, PARTFUN2, BINOP_1, BINOP_2; begin :: Lemmas for extended real valued functions reserve X for non empty set, S for SigmaField of X, M for sigma_Measure of S, f,g for PartFunc of X,ExtREAL, E for Element of S; theorem Th1: (for x be Element of X st x in dom f holds f.x <= g.x) implies g-f is nonnegative proof assume A1: for x be Element of X st x in dom f holds f.x <= g.x; now let y be R_eal; assume y in rng (g-f); then consider x being set such that A2: x in dom (g-f) & y = (g-f).x by FUNCT_1:def 5; dom (g-f) = (dom g /\ dom f)\((g"{+infty} /\ f"{+infty}) \/ (g"{-infty} /\ f"{-infty})) by MESFUNC1:def 4; then x in dom g /\ dom f by A2,XBOOLE_0:def 4; then A4: x in dom f & x in dom g by XBOOLE_0:def 3; 0. <= g.x-f.x by A1,A4,SUPINF_2:72; then 0. <=(g-f).x by A2,MESFUNC1:def 4; hence 0 <= y by A2; end; then rng (g-f) is nonnegative by SUPINF_2:def 15; hence g-f is nonnegative by SUPINF_2:def 22; end; theorem Th2: for Y be set, f be PartFunc of X,ExtREAL, r be Real holds (r(#)f)|Y = r(#)(f|Y) proof let Y be set, f be PartFunc of X,ExtREAL, r be Real; A1: dom ((r(#)f)|Y) = dom (r(#)f) /\ Y by RELAT_1:90 .= dom f /\ Y by MESFUNC1:def 6 .= dom (f|Y) by RELAT_1:90 .= dom (r(#)(f|Y)) by MESFUNC1:def 6; now let x be Element of X; assume A2: x in dom ((r(#)f)|Y); then x in dom (r(#)f) /\ Y by RELAT_1:90; then A3: x in dom (r(#)f) & x in Y by XBOOLE_0:def 3; then x in dom f by MESFUNC1:def 6; then x in dom f /\ Y by A3,XBOOLE_0:def 3; then A4: x in dom (f|Y) by RELAT_1:90; then A5: x in dom (r(#)(f|Y)) by MESFUNC1:def 6; thus ((r(#)f)|Y).x = (r(#)f).x by A2,FUNCT_1:68 .= (R_EAL r)*((f.x)) by A3,MESFUNC1:def 6 .= (R_EAL r)*((f|Y).x) by A4,FUNCT_1:68 .= (r(#)(f|Y)).x by A5,MESFUNC1:def 6; end; hence thesis by A1,PARTFUN1:34; end; theorem Th3: f is_integrable_on M & g is_integrable_on M & g-f is nonnegative implies ex E be Element of S st E = dom f /\ dom g & Integral(M,f|E) <= Integral(M,g|E) proof assume that A1: f is_integrable_on M & g is_integrable_on M and A2: g-f is nonnegative; A3: ex E2 be Element of S st E2 = dom g & g is_measurable_on E2 by A1,MESFUNC5:def 17; set h=(-1)(#)f; A4: h is_integrable_on M & Integral(M,h) = R_EAL (-1) * Integral(M,f) by A1,MESFUNC5:116; then consider E be Element of S such that A5: E = dom h /\ dom g & Integral(M,h+g) = Integral(M,h|E)+Integral(M,g|E) by A1,MESFUNC5:115; g+(-f) is nonnegative by A2,MESFUNC2:9; then A6: h+g is nonnegative by MESFUNC2:11; ex E3 be Element of S st E3 = dom h & h is_measurable_on E3 by A4,MESFUNC5:def 17; then ex A be Element of S st A = dom(h+g) & (h+g) is_measurable_on A by A3,MESFUNC5:53; then A7: 0 <= Integral(M,h|E)+Integral(M,g|E) by A5,A6,MESFUNC5:96; A8: f|E is_integrable_on M by A1,MESFUNC5:103; take E; h|E = (-1)(#)(f|E) by Th2; then A9: 0 <= R_EAL(-1) * Integral(M,f|E) + Integral(M,g|E) by A7,A8,MESFUNC5:116; -infty < Integral(M,f|E) & Integral(M,f|E) < +infty by A8,MESFUNC5:102; then reconsider c1=Integral(M,f|E) as Real by EXTREAL1:1; g|E is_integrable_on M by A1,MESFUNC5:103; then -infty < Integral(M,g|E) & Integral(M,g|E) < +infty by MESFUNC5:102; then reconsider c2=Integral(M,g|E) as Real by EXTREAL1:1; R_EAL (-1) * Integral(M,f|E) = (-1)*c1 by EXTREAL1:13; then 0 <= -c1 + c2 by A9,SUPINF_2:1; then 0 +c1 <=-c1+c2+c1 by XREAL_1:8; hence thesis by A5,MESFUNC1:def 6; end; begin :: Sigma finite set registration let X; cluster nonnegative PartFunc of X,ExtREAL; existence proof consider f be PartFunc of X,ExtREAL; take |.f.|; now let x be set; assume x in dom |.f.|; then (|.f.|).x = |.f.x.| by MESFUNC1:def 10; hence 0. <= (|.f.|).x by EXTREAL2:51; end; hence thesis by SUPINF_2:71; end; end; definition let X,f; redefine func |.f.| -> nonnegative PartFunc of X,ExtREAL; correctness proof now let x be set; assume x in dom |.f.|; then (|.f.|).x = |.f.x.| by MESFUNC1:def 10; hence 0. <= (|.f.|).x by EXTREAL2:51; end; hence thesis by SUPINF_2:71; end; end; theorem f is_integrable_on M implies ex F be Function of NAT,S st ( for n be Element of NAT holds F.n = dom f /\ great_eq_dom(|.f.|, R_EAL(1/(n+1))) ) & dom f \ eq_dom(f, 0.) = union rng F & for n be Element of NAT holds F.n in S & M.(F.n) <+infty proof assume A1: f is_integrable_on M; then consider E be Element of S such that A2: E = dom f & f is_measurable_on E by MESFUNC5:def 17; A3: |.f.| is_measurable_on E by A2,MESFUNC2:29; A4: dom |.f.| = E by A2,MESFUNC1:def 10; defpred P[Element of NAT,set] means $2 = E /\ great_eq_dom(|.f.|, R_EAL(1/($1+1))); A5: for n be Element of NAT ex Z be Element of S st P[n,Z] proof let n be Element of NAT; take Z = E /\ great_eq_dom(|.f.|, R_EAL(1/(n+1))); thus thesis by A3,A4,MESFUNC1:31; end; consider F be Function of NAT,S such that A6: for n be Element of NAT holds P[n,F.n] from FUNCT_2:sch 10(A5); take F; for n be Element of NAT holds F.n = E /\ great_eq_dom(|.f.|, R_EAL(0+1/(n+1))) by A6; then A7: E /\ great_dom(|.f.|, R_EAL 0) = union rng F by MESFUNC1:26; now let x be set; assume A8: x in E /\ great_dom(|.f.|, 0.); then A9: x in E & x in great_dom(|.f.|, 0.) by XBOOLE_0:def 3; reconsider z=x as Element of X by A8; A10: 0. < (|.f.|).z by A9,MESFUNC1:def 14; x in dom |.f.| by A2,A9,MESFUNC1:def 10; then A11: 0. < |.f.z.| by A10,MESFUNC1:def 10; not x in eq_dom(f, 0.) proof assume x in eq_dom(f, 0.); then f.z = 0. by MESFUNC1:def 16; hence contradiction by A11,EXTREAL2:53; end; hence x in E \ eq_dom(f, 0.) by A9,XBOOLE_0:def 4; end; then A12: E /\ great_dom(|.f.|, 0.) c= E \ eq_dom(f, 0.) by TARSKI:def 3; now let x be set; assume A13: x in E \ eq_dom(f, 0.); then A14: x in E & not x in eq_dom(f, 0.) by XBOOLE_0:def 4; reconsider z=x as Element of X by A13; reconsider y=f.z as R_eal; not y = 0. by A2,A14,MESFUNC1:def 16; then A15: 0. < |.f.z.| by EXTREAL2:52; A16: x in dom |.f.| by A2,A14,MESFUNC1:def 10; then 0. < (|.f.|).z by A15,MESFUNC1:def 10; then x in great_dom(|.f.|, 0.) by A16,MESFUNC1:def 14; hence x in E /\ great_dom(|.f.|, 0.) by A14,XBOOLE_0:def 3; end; then A17: E \ eq_dom(f, 0.) c= E /\ great_dom(|.f.|, 0.) by TARSKI:def 3; for n be Element of NAT holds F.n in S & M.(F.n) <+infty proof let n be Element of NAT; set d = R_EAL(1/(n+1)); set En=F.n; set g= (|.f.|)|En; A18: F.n = E /\ great_eq_dom(|.f.| ,R_EAL(1/(n+1))) by A6; then A19: F.n c= E & F.n c= great_eq_dom(|.f.|, R_EAL(1/(n+1))) by XBOOLE_1:17; A20: dom g = En by A4,A18,RELAT_1:91,XBOOLE_1:17; A21: |.f.| is_measurable_on En by A3,A18,MESFUNC1:34,XBOOLE_1:17; dom |.f.| /\ En = E /\ En by A2,MESFUNC1:def 10; then dom |.f.| /\ En = En by A18,XBOOLE_1:17,28; then A22: g is_measurable_on En by A21,MESFUNC5:48; A23: g is nonnegative by MESFUNC5:21; consider nf be PartFunc of X,ExtREAL such that A24: nf is_simple_func_in S & dom nf = En & for x be set st x in En holds nf.x=d by MESFUNC5:47; for x be set st x in dom nf holds nf.x >= 0 by A24; then A25: nf is nonnegative by SUPINF_2:71; A26: nf is_measurable_on En by A24,MESFUNC2:37; for x be Element of X st x in dom nf holds nf.x <= g.x proof let x be Element of X; assume A27: x in dom nf; then A28: g.x = |.f.| .x by A20,A24,FUNCT_1:68; R_EAL(1/(n+1)) <= |.f.| .x by A19,A24,A27,MESFUNC1:def 15; hence thesis by A24,A27,A28; end; then A29: integral+(M,nf) <= integral+(M,g) by A20,A22,A23,A24,A25,A26,MESFUNC5:91; A30: integral+(M,g) =Integral(M,g) & integral+(M,nf) = Integral(M,nf) & Integral(M,nf) = integral'(M,nf) by A20,A22,A23,A24,A25,MESFUNC5:94,95; then A31: integral+(M,nf) = R_EAL(1/(n+1)) * M.(En) by A24,MESFUNC5:110; |.f.| is_integrable_on M by A1,A2,MESFUNC5:106; then A32: Integral(M,|.f.|) < +infty by MESFUNC5:102; (|.f.|)|E=|.f.| by A4,RELAT_1:98; then Integral(M,g) <= Integral(M,|.f.|) by A2,A4,A19,MESFUNC2:29 ,MESFUNC5:99; then integral+(M,nf) <= Integral(M,|.f.|) by A29,A30,XXREAL_0:2; then A33: R_EAL(1/(n+1)) * M.En < +infty by A31,A32,XXREAL_0:2; set z = R_EAL(1/(n+1)); z < +infty by XXREAL_0:9; then z* M.En / z = M.En & +infty / z = +infty by EXTREAL2:17,19; hence thesis by A33,EXTREAL1:51; end; hence thesis by A2,A6,A7,A12,A17,XBOOLE_0:def 10; end; begin :: The first mean value theorem for integrals notation let F be Relation; synonym F is extreal-yielding for F is ext-real-valued; end; definition let k be natural number; let x be Element of ExtREAL; redefine func k |-> x -> FinSequence of ExtREAL; coherence by FINSEQ_2:77; end; registration cluster extreal-yielding FinSequence; existence proof consider f being FinSequence of ExtREAL; f is extreal-yielding; hence thesis; end; end; definition canceled; func multextreal -> BinOp of ExtREAL means :Def2: for x,y be Element of ExtREAL holds it.(x,y) = x*y; existence from BINOP_1:sch 4; uniqueness from BINOP_2:sch 2; end; registration cluster multextreal -> commutative associative; coherence proof A1: for a,b be Element of ExtREAL holds multextreal.(a,b) = multextreal.(b,a) proof let a, b be Element of ExtREAL; multextreal.(a,b) = a * b by Def2; hence thesis by Def2; end; for a,b,c be Element of ExtREAL holds multextreal.(a, multextreal.(b,c)) = multextreal.(multextreal.(a,b),c) proof let a, b, c be Element of ExtREAL; multextreal.(a, multextreal.(b,c)) = multextreal.(a, b * c) by Def2; then multextreal.(a, multextreal.(b,c)) = a * (b * c) by Def2; then multextreal.(a, multextreal.(b,c)) = a * b * c by EXTREAL1:23; then multextreal.(a, multextreal.(b,c)) = multextreal.(a * b, c) by Def2; hence thesis by Def2; end; hence thesis by A1,BINOP_1:def 2,def 3; end; end; Lm1: 1. is_a_unity_wrt multextreal proof for r be Element of ExtREAL holds multextreal.(1.,r) = r proof let r be Element of ExtREAL; multextreal.(1.,r) = 1. * r by Def2; hence thesis by EXTREAL2:4; end; then A1: 1. is_a_left_unity_wrt multextreal by BINOP_1:def 5; for r be Element of ExtREAL holds multextreal.(r,1.) = r proof let r be Element of ExtREAL; multextreal.(r,1.) = r * 1. by Def2; hence thesis by EXTREAL2:4; end; then 1. is_a_right_unity_wrt multextreal by BINOP_1:def 6; hence thesis by A1,BINOP_1:def 7; end; theorem Th5: the_unity_wrt multextreal = 1 by Lm1,BINOP_1:def 8; registration cluster multextreal -> having_a_unity; coherence by Lm1,Th5,SETWISEO:22; end; definition let F be extreal-yielding FinSequence; func Product F -> Element of ExtREAL means :Def3: ex f being FinSequence of ExtREAL st f = F & it = multextreal $$ f; existence proof rng F c= ExtREAL by VALUED_0:def 2; then reconsider f = F as FinSequence of ExtREAL by FINSEQ_1:def 4; take multextreal $$ f; thus thesis; end; uniqueness; end; registration let x be Element of ExtREAL, n be natural number; cluster n |-> x -> extreal-yielding; coherence; end; definition let x be Element of ExtREAL; let k be natural number; func x |^ k equals Product (k |-> x); coherence; end; definition let x be Element of ExtREAL, k be natural number; redefine func x |^ k -> R_eal; coherence; end; registration cluster <*>ExtREAL -> extreal-yielding; coherence; end; registration let r be Element of ExtREAL; cluster <*r*> -> extreal-yielding; coherence; end; theorem Th6: Product (<*>ExtREAL) = 1 proof Product <*>ExtREAL = multextreal $$ (<*>ExtREAL ) by Def3; hence thesis by Th5,FINSOP_1:11; end; theorem Th7: for r be Element of ExtREAL holds Product (<*r*>) = r proof let r be Element of ExtREAL; reconsider r' = r as Element of ExtREAL; reconsider F = <*r'*> as FinSequence of ExtREAL; multextreal $$ F = r by FINSOP_1:12; hence thesis by Def3; end; registration let f,g be extreal-yielding FinSequence; cluster f^g -> extreal-yielding; coherence proof A1: rng f c= ExtREAL & rng g c= ExtREAL by VALUED_0:def 2; rng (f^g) = rng f \/ rng g by FINSEQ_1:44; then rng (f^g) c= ExtREAL by A1,XBOOLE_1:8; hence thesis by VALUED_0:def 2; end; end; theorem Th8: for F being extreal-yielding FinSequence, r be Element of ExtREAL holds Product (F^<*r*>) = Product F * r proof let F be extreal-yielding FinSequence, r be Element of ExtREAL; rng F c= ExtREAL & rng (F^<*r*>) c= ExtREAL by VALUED_0:def 2; then reconsider Fr = F^<*r*>, Ff = F as FinSequence of ExtREAL by FINSEQ_1:def 4; reconsider Ff1=Ff as extreal-yielding FinSequence; Product (F^<*r*>) = multextreal $$ Fr by Def3; then Product (F^<*r*>) = multextreal.(multextreal $$ Ff,r) by FINSOP_1:5; then Product (F^<*r*>) = multextreal.(Product Ff1,r) by Def3; hence thesis by Def2; end; theorem Th9: for x be Element of ExtREAL holds x|^1 = x proof let x be Element of ExtREAL; Product(1 |-> x) = Product(<*x*>) by FINSEQ_2:73; hence x|^1 = x by Th7; end; theorem Th10: for x be Element of ExtREAL, k be natural number holds x|^(k+1) = x|^k*x proof let x be Element of ExtREAL; defpred P[Nat] means x|^($1+1) = x|^$1*x; x|^(0+1) = Product(<*x*>) by FINSEQ_2:73; then x|^(0+1) = x by Th7; then x|^(0+1) =1. * x by EXTREAL2:4; then A1: P[0] by Th6,FINSEQ_2:72; A2: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume x|^(k+1) = x|^k*x; reconsider k1=k+1 as Element of NAT; Product((k1+1) |-> x) = Product((k1 |-> x) ^ <*x*>) by FINSEQ_2:74; hence thesis by Th8; end; for k be Nat holds P[k] from NAT_1:sch 2(A1,A2); hence thesis; end; definition let k be natural number, X,f; func f|^k -> PartFunc of X,ExtREAL means :Def5: dom it = dom f & for x be Element of X st x in dom it holds it.x = (f.x)|^k; existence proof defpred X[set] means $1 in dom f; deffunc U(set) = (f.$1) |^ k; consider f3 being PartFunc of X, ExtREAL such that A1: for d be Element of X holds d in dom f3 iff X[d] and A2: for d be Element of X st d in dom f3 holds f3/.d = U(d) from PARTFUN2:sch 2; take f3; (for x be set st x in dom f3 holds x in dom f) & for x be set st x in dom f holds x in dom f3 by A1; then dom f3 c= dom f & dom f c= dom f3 by TARSKI:def 3; hence dom f3 = dom f by XBOOLE_0:def 10; let d be Element of X; assume A3: d in dom f3; then f3/.d = (f.d) |^ k by A2; hence thesis by A3,PARTFUN1:def 8; end; uniqueness proof let f1,f2 be PartFunc of X, ExtREAL; assume that A4: dom f1= dom f & for d being Element of X st d in dom f1 holds f1.d=(f.d) |^ k and A5: dom f2= dom f & for d being Element of X st d in dom f2 holds f2.d=(f.d) |^ k; for d being Element of X st d in dom f holds f1.d = f2.d proof let d be Element of X; assume d in dom f; then f1.d=(f.d) |^ k & f2.d=(f.d) |^ k by A4,A5; hence f1.d = f2.d; end; hence f1=f2 by A4,A5,PARTFUN1:34; end; end; theorem Th11: for x be Element of ExtREAL, y be real number, k be natural number st x=y holds x|^k = y|^k proof let x be Element of ExtREAL, y be real number, k be natural number; assume A1: x=y; defpred P[natural number] means x|^$1=y|^$1; x|^0 = 1. by Th6,FINSEQ_2:72; then A2: P[0] by NEWTON:9; A3: for k be natural number st P[k] holds P[k+1] proof let k be natural number; reconsider y1=y as Element of REAL by XREAL_0:def 1; assume P[k]; then (x|^k)*x = (y1|^k)*y1 by A1,EXTREAL1:13; then (x|^k)*x = y|^(k+1) by NEWTON:11; hence P[k+1] by Th10; end; for k be natural number holds P[k] from NAT_1:sch 2(A2,A3); hence thesis; end; theorem Th12: for x be Element of ExtREAL, k be natural number st 0 <=x holds 0 <= x|^k proof let x be Element of ExtREAL, k be natural number; assume A1: 0 <=x; defpred P[natural number] means 0 <= x|^$1; A2: P[0] by Th6,FINSEQ_2:72; A3: for k be natural number st P[k] holds P[k+1] proof let k be natural number; assume A4: P[k]; x|^(k+1)=(x|^k)*x by Th10; hence P[k+1] by A1,A4,EXTREAL2:45; end; for k be natural number holds P[k] from NAT_1:sch 2(A2,A3); hence thesis; end; theorem Th13: for k be natural number st 1<=k holds +infty|^k =+infty proof defpred P[Nat] means +infty|^$1 = +infty; A1: P[1] by Th9; A2: for k be non empty Nat st P[k] holds P[k+1] proof let k be non empty Nat; assume A3: P[k]; +infty|^(k+1)=(+infty|^k)*+infty by Th10; hence P[k+1] by A3,EXTREAL1:def 1; end; for k be non empty Nat holds P[k] from NAT_1:sch 10(A1,A2); hence thesis; end; theorem Th14: for k be natural number, X,S,f,E st E c= dom f & f is_measurable_on E holds (|.f.|) |^ k is_measurable_on E proof let k be natural number; let X,S,f,E; reconsider k1=k as Element of NAT by ORDINAL1:def 13; assume A1: E c= dom f & f is_measurable_on E; A2: dom ((|.f.|)|^k) = dom |.f.| by Def5; then A3: dom ((|.f.|)|^k) = dom f by MESFUNC1:def 10; per cases; suppose A4: k = 0; A5: for r be real number st 1 < r holds E /\ less_dom((|.f.|)|^k,R_EAL r) is_measurable_on S proof let r be real number; assume A6: 1 < r; E c= less_dom((|.f.|)|^k,R_EAL r) proof let x be set; assume A7: x in E; then ((|.f.|)|^k).x = ((|.f.|).x)|^k by A1,A3,Def5; then ((|.f.|)|^k).x < r by A4,A6,Th6,FINSEQ_2:72; hence x in less_dom((|.f.|)|^k,R_EAL r) by A1,A3,A7,MESFUNC1:def 12; end; then E /\ less_dom((|.f.|)|^k,R_EAL r) = E by XBOOLE_1:28; hence E /\ less_dom((|.f.|) |^k,R_EAL r) is_measurable_on S; end; A8: E c= dom ((|.f.|)|^k) by A1,A2,MESFUNC1:def 10; for r be real number holds E /\ less_dom((|.f.|)|^k,R_EAL r) is_measurable_on S proof let r be real number; now assume A9: r <= 1; E c= great_eq_dom((|.f.|)|^k,R_EAL r) proof let x be set; assume A10: x in E; then ((|.f.|)|^k).x = ((|.f.|).x)|^k by A1,A3,Def5; then r <= ((|.f.|)|^k).x by A4,A9,Th6,FINSEQ_2:72; hence x in great_eq_dom((|.f.|)|^k,R_EAL r) by A1,A3,A10,MESFUNC1:def 15; end; then E /\ great_eq_dom((|.f.|)|^k,R_EAL r) = E by XBOOLE_1:28; then E /\ less_dom((|.f.|)|^k,R_EAL r) = E \ E by A8,MESFUNC1:21; hence E /\ less_dom((|.f.|)|^k,R_EAL r) is_measurable_on S; end; hence thesis by A5; end; hence (|.f.|)|^ k is_measurable_on E by MESFUNC1:def 17; end; suppose A11: k <> 0; then A12: 1 <= k by NAT_1:14; A13: 1/k * k = 1 by A11,XCMPLX_1:88; A14: for r be real number st 0 < r holds great_eq_dom((|.f.|)|^k,R_EAL r) = great_eq_dom(|.f.|,R_EAL r to_power (1/k)) proof let r be real number; assume A15: 0 < r; A16: great_eq_dom(|.f.|,R_EAL r to_power (1/k)) c= great_eq_dom((|.f.|)|^k,R_EAL r) proof let x be set; assume A17: x in great_eq_dom(|.f.|,R_EAL r to_power (1/k)); then A18: x in dom |.f.| by MESFUNC1:def 15; then |.f.| .x = |.f.x.| by MESFUNC1:def 10; then A19: 0 <= |.f.| .x by EXTREAL2:51; A20: ((|.f.|)|^k).x = (|.f.| .x)|^k by A2,A18,Def5; A21: now assume |.f.| .x = +infty; then ((|.f.|).x) |^k = +infty by A11,Th13,NAT_1:14; hence r <= ((|.f.|)|^k).x by A20,XXREAL_0:3; end; now assume |.f.| .x <> +infty; then reconsider fx = |.f.| .x as Element of REAL by A19,SUPINF_2:2; A22: ((|.f.|)|^k).x = fx|^k by A20,Th11; A23: R_EAL r to_power (1/k) <= |.f.| .x by A17,MESFUNC1:def 15; A24: 0 < r to_power (1/k) by A15,POWER:39; reconsider R = r to_power (1/k) as Real by XREAL_0:def 1; R to_power k1 = r to_power (1/k*k) by A15,POWER:38; then A25: r to_power 1 <= fx to_power k by A12,A13,A23,A24,HOLDER_1:3; thus r <=((|.f.|) |^k).x by A22,A25,POWER:30; end; hence x in great_eq_dom((|.f.|)|^k,R_EAL r) by A2,A18,A21,MESFUNC1:def 15; end; great_eq_dom((|.f.|)|^k,R_EAL r) c= great_eq_dom(|.f.|,R_EAL r to_power (1/k)) proof let x be set; assume A26: x in great_eq_dom((|.f.|)|^k,R_EAL r); then A27: x in dom ((|.f.|)|^k) by MESFUNC1:def 15; then A28: |.f.| .x = |.f.x.| by A2,MESFUNC1:def 10; then A29: 0 <= |.f.| .x by EXTREAL2:51; per cases; suppose |.f.| .x = +infty; then R_EAL r to_power (1/k) <= |.f.| .x by XXREAL_0:3; hence x in great_eq_dom(|.f.|, R_EAL r to_power (1/k)) by A2,A27,MESFUNC1:def 15; end; suppose |.f.| .x <> +infty; then reconsider fx= |.f.| .x as Element of REAL by A29,SUPINF_2:2; A30: 0 < 1/k by A12; A31: r <= ((|.f.|)|^k).x by A26,MESFUNC1:def 15; ((|.f.|)|^k).x = ((|.f.|).x)|^k by A27,Def5; then ((|.f.|)|^k).x = fx|^k by Th11; then A32: r <= fx to_power k1 by A31; r is Real by XREAL_0:def 1; then A33: r to_power (1/k) <= (fx to_power k) to_power (1/k) by A15,A30,A32,HOLDER_1:3; 0 < k by A11; then (fx to_power k) to_power (1/k) = fx to_power (k * 1/k) by A28,EXTREAL2:51,HOLDER_1:2; then (fx to_power k) to_power (1/k) = fx by A13,POWER:30; hence x in great_eq_dom(|.f.|, R_EAL r to_power (1/k)) by A2,A27,A33,MESFUNC1:def 15; end; end; hence thesis by A16,XBOOLE_0:def 10; end; A34: |.f.| is_measurable_on E by A1,MESFUNC2:29; for r be real number holds E /\ great_eq_dom((|.f.|)|^k,R_EAL r) is_measurable_on S proof let r be real number; per cases; suppose A35: r <= 0; E c= great_eq_dom((|.f.|)|^k,R_EAL r) proof let x be set; assume A36: x in E; then A37: ((|.f.|)|^k).x = ((|.f.|).x)|^k by A1,A3,Def5; (|.f.|).x = |.f.x.| by A1,A2,A3,A36,MESFUNC1:def 10; then r <= ((|.f.|)|^k).x by A35,A37,Th12,EXTREAL2:51; hence x in great_eq_dom((|.f.|)|^k,R_EAL r) by A1,A3,A36,MESFUNC1:def 15; end; then E /\ great_eq_dom((|.f.|)|^k,R_EAL r) = E by XBOOLE_1:28; hence E /\ great_eq_dom((|.f.|)|^k,R_EAL r) is_measurable_on S; end; suppose 0 = inf F & c <= sup F & Integral(M, (f(#)|.g.|)|E) = R_EAL c * Integral(M, (|.g.|)|E) proof let M be sigma_Measure of S, f,g be PartFunc of X, ExtREAL, E be Element of S, F be non empty Subset of ExtREAL; assume A1: dom f /\ dom g = E & rng f = F & g is finite & f is_measurable_on E & rng f is bounded & g is_integrable_on M; then consider E1 be Element of S such that A2: E1 = dom g & g is_measurable_on E1 by MESFUNC5:def 17; A3: E1 = dom |.g.| & |.g.| is_measurable_on E1 by A2,MESFUNC1:def 10,MESFUNC2:29; then A4: g is_measurable_on E & |.g.| is_measurable_on E by A1,A2,MESFUNC1:34 ,XBOOLE_1:17; A5: rng f is bounded_below & rng f is bounded_above by A1,XXREAL_2:def 11; A6: f is finite by A1,Th16; A7: rng f is Subset of REAL by A1,Th16,MESFUNC2:35; then not +infty in rng f & not -infty in rng f; then rng f <> {+infty} & rng f <> {-infty} by TARSKI:def 1; then reconsider k0=inf F, l0=sup F as Real by A1,A5,XXREAL_2:57,58; |.inf F.|=abs k0 & |.sup F.|=abs l0 by EXTREAL2:49; then reconsider k1= |.inf F.|, l1= |.sup F.| as Real; A8: dom |.g.| = dom g by MESFUNC1:def 10; A9: E c= dom f & E c= dom g by A1,XBOOLE_1:17; then A10: E c= dom |.g.| by MESFUNC1:def 10; A11: dom (f(#)g) = E by A1,MESFUNC1:def 5; then A12: dom((f(#)g)|E) = E by RELAT_1:91; then A13: dom (|.(f(#)g)|E.|) = E by MESFUNC1:def 10; dom ( ((k1+l1)(#)|.g.|)|E ) = dom ( (k1+l1)(#)(|.g.|)|E ) by Th2; then dom ( ((k1+l1)(#)|.g.|)|E ) = dom ((|.g.|)|E) by MESFUNC1:def 6; then A14: dom ( ((k1+l1)(#)|.g.|)|E ) = E by A10,RELAT_1:91; A15: dom ((k1+l1)(#)|.g.|) = dom |.g.| by MESFUNC1:def 6; A16: dom (f(#)|.g.|) = dom f /\ dom |.g.| by MESFUNC1:def 5; then A17: dom (f(#)|.g.|) = E by A1,MESFUNC1:def 10; A18: dom ((f(#)|.g.|)|E) = dom (f(#)|.g.|) /\ E by FUNCT_1:68; A19: inf F is LowerBound of rng f & sup F is UpperBound of rng f by A1,XXREAL_2:def 3,def 4; A20: for x be Element of X st x in E holds |. f.x .| <= |.inf F.| + |.sup F.| proof let x be Element of X; assume x in E; then A21: f.x in rng f by A9,FUNCT_1:12; then reconsider fx=f.x as Real by A7; A22: k0 <=fx & fx <=l0 by A19,A21,XXREAL_2:def 1,def 2; l0 <= abs l0 & 0 <= abs k0 by COMPLEX1:132,162; then l0+abs k0 <=abs l0 + abs k0 & l0+0 <=l0+abs k0 by XREAL_1:8; then A23: l0 <=abs l0 + abs k0 by XXREAL_0:2; 0 <= abs l0 by COMPLEX1:132; then A24: -abs k0 -abs l0 <= -abs k0 -0 by XREAL_1:12; -abs k0 <= k0 by COMPLEX1:162; then -abs k0 -abs l0 <= k0 by A24,XXREAL_0:2; then -(abs k0 + abs l0) <= fx & fx <= abs k0 + abs l0 by A22,A23,XXREAL_0:2; then A25: abs fx <= abs k0 + abs l0 by ABSVALUE:12; abs fx = |.f.x.| & abs k0= |.inf F.| & abs l0 = |.sup F.| by EXTREAL2:49; hence |.f.x.| <= |.inf F.| + |.sup F.| by A25,SUPINF_2:1; end; A26: |.g.| is_integrable_on M by A1,A2,MESFUNC5:106; then A27: (|.g.|)|E is_integrable_on M by MESFUNC5:103; (k1+l1)(#)|.g.| is_integrable_on M by A26,MESFUNC5:116; then A28: ((k1+l1)(#)|.g.|)|E is_integrable_on M by MESFUNC5:103; A29: f(#)g is_measurable_on E by A1,A4,A6,Th15; dom (f(#)g) /\ E = E by A11; then A30: (f(#)g)|E is_measurable_on E by A29,MESFUNC5:48; A31: for x be Element of X st x in dom ((f(#)g)|E) holds |.((f(#)g)|E).x.| <= (((k1+l1)(#)|.g.|)|E).x proof let x be Element of X; assume A32: x in dom ((f(#)g)|E); then A33: ((f(#)g)|E).x = (f(#)g).x by FUNCT_1:70; dom (f|E) = E & dom (g|E) = E by A1,RELAT_1:91,XBOOLE_1:17; then A34: (f|E).x = f.x & (g|E).x = g.x by A12,A32,FUNCT_1:70; 0 <= |.(g|E).x.| by EXTREAL2:51; then A35: |.(f|E).x.|*|.(g|E).x.| <= (|.inf F.| + |.sup F.|)*|.(g|E).x.| by A12,A20,A32,A34,EXTREAL1:42; A36: (((k1+l1)(#)|.g.|)|E).x = ((k1+l1)(#)|.g.|).x by A12,A14,A32,FUNCT_1:70; |.(f(#)g).x.| = |. f.x * g.x .| by A11,A12,A32,MESFUNC1:def 5; then A37: |.((f(#)g)|E).x.| = |.(f|E).x.|*|.(g|E).x.| by A33,A34,EXTREAL2:56; ((k1+l1)(#)|.g.|).x = R_EAL(k1+l1) * |.g.| .x by A10,A12,A15,A32,MESFUNC1:def 6; then (((k1+l1)(#)|.g.|)|E).x = R_EAL(k1+l1)*|.(g|E).x.| by A10,A12,A32,A34,A36,MESFUNC1:def 10; hence thesis by A35,A37,SUPINF_2:1; end; then (f(#)g)|E is_integrable_on M by A12,A14,A28,A30,MESFUNC5:108; then A38: |.((f(#)g)|E).| is_integrable_on M by A12,A30,MESFUNC5:106; for x be Element of X st x in dom |.g.| holds |. |.g.| .x.| < +infty proof let x be Element of X; assume A39: x in dom |.g.|; then |. |.g.| .x.| = |.|.g.x.|.| by MESFUNC1:def 10; then |. |.g.| .x.| = |.g.x.| by EXTREAL2:70; hence thesis by A1,A8,A39,MESFUNC2:def 1; end; then A40: |.g.| is finite by MESFUNC2:def 1; dom f /\ dom |.g.| = E by A1,MESFUNC1:def 10; then A41: f(#)|.g.| is_measurable_on E by A1,A4,A6,A40,Th15; dom (f(#)|.g.|) /\ E = E by A17; then A42: (f(#)|.g.|)|E is_measurable_on E by A41,MESFUNC5:48; for x be Element of X st x in dom ((f(#)|.g.|)|E) holds |.((f(#)|.g.|)|E).x.| <= |.((f(#)g)|E).| .x proof let x be Element of X; assume A43: x in dom ((f(#)|.g.|)|E); then |. (f(#)|.g.|).x.| = |. f.x*|.g.|.x .| by A17,A18,MESFUNC1:def 5 .= |. f.x*|.g.x.| .| by A1,A8,A9,A16,A18,A43,MESFUNC1:def 10 .= |.f.x.| * |. |.g.x.| .| by EXTREAL2:56 .= |.f.x.|*|.g.x.| by EXTREAL2:70; then A44: |. (f(#)|.g.|).x.| = |. f.x*g.x .| by EXTREAL2:56; dom |.f(#)g.| = E by A11,MESFUNC1:def 10; then A45: |.(f(#)g).|.x = |.(f(#)g).x.| by A17,A18,A43,MESFUNC1:def 10; A46: ((f(#)|.g.|)|E).x = (f(#)|.g.|).x by A43,FUNCT_1:70; |. ((f(#)g)|E).x .| = |. (f(#)g).x .| by A12,A17,A18,A43,FUNCT_1:70; then |.((f(#)g)|E).| .x = |. f(#)g .| .x by A13,A17,A18,A43,A45,MESFUNC1:def 10; hence thesis by A11,A17,A18,A43,A44,A45,A46,MESFUNC1:def 5; end; then A47: (f(#)|.g.|)|E is_integrable_on M by A13,A17,A18,A38,A42,MESFUNC5:108; A48: for x be Element of X st x in E holds inf F*|.g.x.| <= (f.x)*|.g.x.| & (f.x)*|.g.x.| <= sup F*|.g.x.| proof let x be Element of X; assume x in E; then f.x in rng f by A9,FUNCT_1:12; then A49: inf F <= f.x & f.x <= sup F by A19,XXREAL_2:def 1,def 2; 0 <= |.g.x.| by EXTREAL2:51; hence thesis by A49,EXTREAL1:42; end; A50: dom (k0(#)|.g.|) = dom |.g.| & dom (l0(#)|.g.|) = dom |.g.| by MESFUNC1:def 6; then A51: dom ((k0(#)|.g.|)|E) = E & dom ((l0(#)|.g.|)|E) = E by A10,RELAT_1:91; A52: dom (f(#)|.g.|) c= dom (l0(#)|.g.|) by A16,A50,XBOOLE_1:17; Integral(M, (k0(#)|.g.|)|E) = Integral(M, k0(#)((|.g.|)|E)) & Integral(M, (l0(#)|.g.|)|E) = Integral(M, l0(#)((|.g.|)|E)) by Th2; then A53: Integral(M, (k0(#)|.g.|)|E) = R_EAL k0 * Integral(M, (|.g.|)|E) & Integral(M, (l0(#)|.g.|)|E) = R_EAL l0 * Integral(M, (|.g.|)|E) by A27,MESFUNC5:116; k0(#)|.g.| is_integrable_on M by A26,MESFUNC5:116; then A54: (k0(#)|.g.|)|E is_integrable_on M by MESFUNC5:103; for x be Element of X st x in dom ((k0(#)|.g.|)|E) holds ((k0(#)|.g.|)|E).x <= ((f(#)|.g.|)|E).x proof let x be Element of X; assume A55: x in dom ((k0(#)|.g.|)|E); then (k0(#)|.g.|).x = (R_EAL k0)*(|.g.|).x & (f(#)|.g.|).x = (f.x)*(|.g.|.x) by A10,A17,A50,A51,MESFUNC1:def 5,def 6; then (k0(#)|.g.|).x = (R_EAL k0)*|.g.x.| & (f(#)|.g.|).x = (f.x)*|.g.x.| by A10,A51,A55,MESFUNC1:def 10; then A56: (k0(#)|.g.|).x <= (f(#)|.g.|).x by A48,A51,A55; ((k0(#)|.g.|)|E).x = (k0(#)|.g.|).x by A55,FUNCT_1:70; hence thesis by A17,A18,A51,A55,A56,FUNCT_1:70; end; then (f(#)|.g.|)|E - (k0(#)|.g.|)|E is nonnegative by Th1; then consider V1 be Element of S such that A57: V1 = dom((k0(#)|.g.|)|E) /\ dom((f(#)|.g.|)|E) & Integral(M,((k0(#)|.g.|)|E)|V1) <= Integral(M,((f(#)|.g.|)|E)|V1) by A47,A54,Th3; A58: ((k0(#)|.g.|)|E)|V1 = (k0(#)|.g.|)|E & ((f(#)|.g.|)|E)|V1 = (f(#)|.g.|)|E by A17,A18,A51,A57,RELAT_1:97; l0(#)|.g.| is_integrable_on M by A26,MESFUNC5:116; then A59: (l0(#)|.g.|)|E is_integrable_on M by MESFUNC5:103; for x be Element of X st x in dom ((f(#)|.g.|)|E) holds ((f(#)|.g.|)|E).x <= ((l0(#)|.g.|)|E).x proof let x be Element of X; assume A60: x in dom ((f(#)|.g.|)|E); then (f(#)|.g.|).x = (f.x)*(|.g.|).x & (l0(#)|.g.|).x = (R_EAL l0)*(|. g.|.x) by A17,A18,A52,MESFUNC1:def 5,def 6; then (f(#)|.g.|).x = (f.x)*|.g.x.| & (l0(#)|.g.|).x = (R_EAL l0)*|.g.x .| by A10,A17,A18,A60,MESFUNC1:def 10; then A61: (f(#)|.g.|).x <= (l0(#)|.g.|).x by A17,A18,A48,A60; ((f(#)|.g.|)|E).x = (f(#)|.g.|).x by A60,FUNCT_1:70; hence thesis by A17,A18,A51,A60,A61,FUNCT_1:70; end; then (l0(#)|.g.|)|E - (f(#)|.g.|)|E is nonnegative by Th1; then consider V2 be Element of S such that A62: V2 = dom((l0(#)|.g.|)|E) /\ dom((f(#)|.g.|)|E) & Integral(M,((f(#)|.g.|)|E)|V2) <= Integral(M,((l0(#)|.g.|)|E)|V2) by A47,A59,Th3; A63: ((f(#)|.g.|)|E)|V2 = (f(#)|.g.|)|E & ((l0(#)|.g.|)|E)|V2 = (l0(#)|.g.|)|E by A17,A18,A51,A62,RELAT_1:97; A64: -infty < Integral(M, (f(#)|.g.|)|E) & Integral(M, (f(#)|.g.|)|E) < +infty by A47,MESFUNC5:102; ex c be Element of REAL st c >= inf F & c <= sup F & Integral(M,(f(#)|.g.|)|E) = R_EAL c * Integral(M,(|.g.|)|E) proof per cases; suppose A65: Integral(M, (|.g.|)|E) <> 0.; then A66: Integral(M, (|.g.|)|E) > 0. by A3,MESFUNC5:98; A67: -infty < Integral(M, (|.g.|)|E) & Integral(M, (|.g.|)|E) < +infty by A27,MESFUNC5:102; then reconsider c1=Integral(M, (|.g.|)|E) as Real by EXTREAL1:1; A68: Integral(M, (|.g.|)|E)/Integral(M, (|.g.|)|E) =c1/c1 by A65,EXTREAL1:32; inf F * Integral(M, (|.g.|)|E) = k0*c1 & sup F * Integral(M, (|.g.|)|E) = l0*c1 by EXTREAL1:13; then A69: (inf F * Integral(M, (|.g.|)|E)) / Integral(M, (|.g.|)|E) = k0 *c1 /c1 & (sup F * Integral(M, (|.g.|)|E)) / Integral(M, (|.g.|)|E) = l0*c1/c1 by A65,EXTREAL1:32; k0*c1/c1=k0*(c1/c1) & l0*c1/c1=l0*(c1/c1); then A70: inf F * Integral(M, (|.g.|)|E) / Integral(M, (|.g.|)|E) = inf F *(Integral(M, (|.g.|)|E) / Integral(M, (|.g.|)|E)) & sup F * Integral(M, (|.g.|)|E) / Integral(M, (|.g.|)|E) = sup F *(Integral(M, (|.g.|)|E) / Integral(M, (|.g.|)|E)) by A68,A69,EXTREAL1:13; inf F * (Integral(M,(|.g.|)|E) / Integral(M,(|.g.|)|E)) = inf F * 1. & sup F * (Integral(M,(|.g.|)|E) / Integral(M,(|.g.|)|E)) = sup F * 1. by A65,A67,EXTREAL1:34; then A71: inf F * (Integral(M, (|.g.|)|E) / Integral(M, (|.g.|)|E)) = inf F & sup F * (Integral(M, (|.g.|)|E) / Integral(M, (|.g.|)|E)) = sup F by EXTREAL2:4; set c2 = Integral(M, (f(#)|.g.|)|E) / Integral(M, (|.g.|)|E); reconsider c3 = Integral(M, (f(#)|.g.|)|E) as Real by A64,EXTREAL1:1; Integral(M, (f(#)|.g.|)|E) / Integral(M, (|.g.|)|E) = c3 /c1 by A65,EXTREAL1:32; then reconsider c = c2 as Element of REAL; A72: c >= inf F & c <= sup F by A53,A57,A58,A62,A63,A66,A67,A70,A71,EXTREAL1:48; Integral(M, (f(#)|.g.|)|E) / Integral(M, (|.g.|)|E) = c3 / c1 & Integral(M, (|.g.|)|E) / Integral(M, (|.g.|)|E) = c1 / c1 by A65,EXTREAL1:32; then Integral(M,(|.g.|)|E) * ( Integral(M,(f(#)|.g.|)|E) / Integral(M,(|.g.|)|E) ) = c1 * (c3 / c1) & c3 * (c1 / c1) = Integral(M, (f(#)|.g.|)|E) * ( Integral(M, (|.g.|)|E) / Integral(M, (|.g.|)|E) ) by EXTREAL1:13; then R_EAL c * Integral(M, (|.g.|)|E) = Integral(M, (f(#)|.g.|)|E) by A65,A67,EXTREAL2:19; hence thesis by A72; end; suppose A73: Integral(M, (|.g.|)|E) = 0.; consider y be set such that A74: y in F by XBOOLE_0:def 1; reconsider y as Element of ExtREAL by A74; inf F <= y & y <= sup F by A74,XXREAL_2:3,4; then A75: inf F <= k0 & k0 <= sup F by XXREAL_0:2; 0. <= Integral(M, (f(#)|.g.|)|E) by A53,A57,A58,A73,EXTREAL1:22; then A76: Integral(M, (f(#)|.g.|)|E) = 0. by A53,A62,A63,A73,EXTREAL1:22; R_EAL k0 * Integral(M, (|.g.|)|E) = 0. by A73,EXTREAL1:22; hence thesis by A75,A76; end; end; hence thesis by A12,A14,A28,A30,A31,MESFUNC5:108; end; begin :: Selected properties of integrals reserve E1,E2 for Element of S; reserve x,A for set; reserve a,b for real number; theorem Th18: (|.f.|)|A = |.(f|A).| proof A1: dom((|.f.|)|A) = dom |.f.| /\ A & dom(f|A) = dom f /\ A by FUNCT_1:68; then A2: dom((|.f.|)|A) = dom f /\ A & dom|.(f|A).| = dom f /\ A by MESFUNC1:def 10; now let x be Element of X; assume A3: x in dom((|.f.|)|A); then A4: ((|.f.|)|A).x = (|.f.|).x by FUNCT_1:70; x in dom f by A2,A3,XBOOLE_0:def 3; then A5: x in dom |.f.| by MESFUNC1:def 10; (|.(f|A).|).x = |. (f|A).x .| by A2,A3,MESFUNC1:def 10; then (|.(f|A).|).x = |. f.x .| by A1,A2,A3,FUNCT_1:70; hence ((|.f.|)|A).x = (|.(f|A).|).x by A4,A5,MESFUNC1:def 10; end; hence thesis by A2,PARTFUN1:34; end; theorem Th19: dom(|.f.|+|.g.|) = dom f /\ dom g & dom |.f+g.| c= dom |.f.| proof set F = |.f.|; set G = |.g.|; A1: dom(|.f.|+|.g.|) = (dom F /\ dom G)\((F"{-infty} /\ G"{+infty}) \/ (F"{+infty} /\ G"{-infty})) by MESFUNC1:def 3; F is without-infty & G is without-infty by MESFUNC5:18; then not -infty in rng F & not -infty in rng G by MESFUNC5:def 3; then F"{-infty} = {} & G"{-infty} = {} by FUNCT_1:142; then dom(|.f.|+|.g.|) = dom f /\ dom G by A1,MESFUNC1:def 10; hence dom(|.f.|+|.g.|) = dom f /\ dom g by MESFUNC1:def 10; dom |.f+g.| = dom(f+g) by MESFUNC1:def 10 .= (dom f /\ dom g) \((f"{-infty} /\ g"{+infty}) \/ (f"{+infty} /\ g"{-infty})) by MESFUNC1:def 3 .= dom f /\ (dom g \((f"{-infty} /\ g"{+infty}) \/ (f"{+infty} /\ g"{-infty}))) by XBOOLE_1:49; then dom |.f+g.| c= dom f by XBOOLE_1:17; hence dom |.f+g.| c= dom |.f.| by MESFUNC1:def 10; end; theorem Th20: (|.f.|)|(dom |.f+g.|) + (|.g.|)|(dom |.f+g.|) = (|.f.|+|.g.|)|(dom |.f+g.|) proof A1: dom |.f+g.| c= dom |.f.| & dom |.f+g.| c= dom |.g.| by Th19; then A2: dom |.f+g.| c= dom f & dom |.f+g.| c= dom g by MESFUNC1:def 10; dom(f|(dom |.f+g.|)) = dom f /\ dom |.f+g.| & dom(g|(dom |.f+g.|)) = dom g /\ dom |.f+g.| by FUNCT_1:68; then A3: dom(f|(dom |.f+g.|)) = dom |.f+g.| & dom(g|(dom |.f+g.|)) = dom |.f+g.| by A2,XBOOLE_1:28; then A4: dom |.(f|(dom |.f+g.|)).| = dom |.f+g.| & dom |.(g|(dom |.f+g.|)).| = dom |.f+g.| by MESFUNC1:def 10; A5: (|.f.|)|(dom |.f+g.|) = |.(f|(dom |.f+g.|)).| & (|.g.|)|(dom |.f+g.|) = |.(g|(dom |.f+g.|)).| by Th18; then A6: dom((|.f.|)|(dom |.f+g.|) + (|.g.|)|(dom |.f+g.|)) = dom (f|(dom |.f+g.|)) /\ dom (g|(dom |.f+g.|)) by Th19 .= dom |.f+g.| by A3; dom |.f+g.| /\ dom |.f+g.| c= dom f /\ dom g by A2,XBOOLE_1:27; then A7: dom |.f+g.| c= dom(|.f.|+|.g.|) by Th19; then A8: dom((|.f.|+|.g.|)|(dom |.f+g.|)) = dom |.f+g.| by RELAT_1:91; now let x be Element of X; assume A9: x in dom((|.f.|+|.g.|)|(dom |.f+g.|)); then A10: ((|.f.|+|.g.|)|(dom |.f+g.|)).x = (|.f.|+|.g.|).x by FUNCT_1:70 .= (|.f.|).x + (|.g.|).x by A7,A8,A9,MESFUNC1:def 3 .= |. f.x .| + (|.g.|).x by A1,A8,A9,MESFUNC1:def 10; A11: x in dom |.f+g.| by A7,A9,RELAT_1:91; then ((|.f.|)|(dom |.f+g.|) + (|.g.|)|(dom |.f+g.|)).x = ((|.f.|)|(dom |.f+g.|)).x + ((|.g.|)|(dom |.f+g.|)).x by A6,MESFUNC1:def 3 .= |.(f|(dom |.f+g.|)).x .| + |.(g|(dom |.f+g.|)).|.x by A4,A5,A11,MESFUNC1:def 10 .= |.(f|(dom |.f+g.|)).x .| + |.(g|(dom |.f+g.|)).x .| by A4,A11,MESFUNC1:def 10 .= |. f.x .| + |.(g|(dom |.f+g.|)).x .| by A11,FUNCT_1:72 .= |. f.x .| + |. g.x .| by A11,FUNCT_1:72; hence ((|.f.|+|.g.|)|(dom |.f+g.|)).x = ((|.f.|)|(dom |.f+g.|) + (|.g.|)|(dom |.f+g.|)).x by A1,A8,A9,A10,MESFUNC1:def 10; end; hence thesis by A6,A8,PARTFUN1:34; end; theorem Th21: x in dom |.f+g.| implies (|.f+g.|).x <= (|.f.|+|.g.|).x proof assume A1: x in dom |.f+g.|; then A2: x in dom (f+g) by MESFUNC1:def 10; then x in (dom f /\ dom g) \ ((f"{-infty} /\ g"{+infty}) \/ (f"{+infty} /\ g"{-infty})) by MESFUNC1:def 3; then x in dom f /\ dom g & not x in (f"{-infty} /\ g"{+infty}) \/ (f"{+infty} /\ g"{-infty}) by XBOOLE_0:def 4; then A3: x in dom f & x in dom g & not x in (f"{-infty} /\ g"{+infty}) & not x in (f"{+infty} /\ g"{-infty}) by XBOOLE_0:def 2,def 3; then (not x in f"{-infty} or not x in g"{+infty}) & (not x in f"{+infty} or not x in g"{-infty}) by XBOOLE_0:def 3; then (not f.x in {-infty} or not g.x in {+infty}) & (not f.x in {+infty} or not g.x in {-infty}) by A3,FUNCT_1:def 13; then (f.x <> -infty or g.x <> +infty) & (f.x <> +infty or g.x <> -infty) by TARSKI:def 1; then |. f.x + g.x .| <= |. f.x .| + |. g.x .| by EXTREAL2:61; then A4: |. (f+g).x .| <= |. f.x .| + |. g.x .| by A2,MESFUNC1:def 3; A5: dom |.f+g.| c= dom |.f.| & dom |.f+g.| c= dom |.g.| by Th19; then A6: |. f.x .| = |.f.| .x & |. g.x .| = |.g.| .x by A1,MESFUNC1:def 10; x in dom |.f.| & x in dom |.g.| by A1,A5; then x in dom f & x in dom g by MESFUNC1:def 10; then x in dom f /\ dom g by XBOOLE_0:def 3; then x in dom(|.f.| + |.g.|) by Th19; then |. f.x .| + |. g.x .| = (|.f.| + |.g.|).x by A6,MESFUNC1:def 3; hence thesis by A1,A4,MESFUNC1:def 10; end; theorem f is_integrable_on M & g is_integrable_on M implies ex E be Element of S st E = dom(f+g) & Integral(M,(|.f+g.|)|E) <= Integral(M,(|.f.|)|E) + Integral(M,(|.g.|)|E) proof assume A1: f is_integrable_on M & g is_integrable_on M; then (ex A be Element of S st A = dom f & f is_measurable_on A) & (ex A be Element of S st A = dom g & g is_measurable_on A) by MESFUNC5:def 17; then A2: |.f.| is_integrable_on M & |.g.| is_integrable_on M by A1,MESFUNC5:106; then A3: |.f.|+|.g.| is_integrable_on M by MESFUNC5:114; set F = |.f.|; set G = |.g.|; A4: f+g is_integrable_on M by A1,MESFUNC5:114; then ex A be Element of S st A = dom(f+g) & f+g is_measurable_on A by MESFUNC5:def 17; then A5: |.f+g.| is_integrable_on M by A4,MESFUNC5:106; for x be Element of X st x in dom |.f+g.| holds (|.f+g.|).x <= (|.f.|+|.g.|).x by Th21; then (|.f.|+|.g.|) - |.f+g.| is nonnegative by Th1; then consider E be Element of S such that A6: E = dom(|.f.|+|.g.|) /\ dom |.f+g.| & Integral(M,(|.f+g.|)|E) <= Integral(M,(|.f.|+|.g.|)|E) by A3,A5,Th3; take E; F|E is_integrable_on M & G|E is_integrable_on M by A2,MESFUNC5:103; then consider E1 be Element of S such that A7: E1 = dom (F|E) /\ dom (G|E) & Integral(M,F|E+G|E) = Integral(M,(F|E)|E1) + Integral(M,(G|E)|E1) by MESFUNC5:115; A8: dom (|.f.|+|.g.|) = dom f /\ dom g by Th19; A9: dom |.f+g.| = dom(f+g) by MESFUNC1:def 10 .= (dom f /\ dom g) \((f"{-infty} /\ g"{+infty}) \/ (f"{+infty} /\ g"{-infty})) by MESFUNC1:def 3; then A10: E = dom |.f+g.| by A6,A8,XBOOLE_1:28,36; dom(F|E) = dom F /\ E & dom(G|E) = dom G /\ E by FUNCT_1:68; then dom(F|E) = dom f /\ E & dom(G|E) = dom g /\ E by MESFUNC1:def 10; then E1 = (dom f /\ E /\ E) /\ dom g by A7,XBOOLE_1:16; then E1 = (dom f /\ (E /\ E)) /\ dom g by XBOOLE_1:16; then E1 = dom f /\ dom g /\ E by XBOOLE_1:16; then E1 = E by A6,A8,A9,XBOOLE_1:28,36; then (F|E)|E1 = F|E & (G|E)|E1 = G|E by FUNCT_1:82; hence thesis by A6,A7,A10,Th20,MESFUNC1:def 10; end; theorem Th23: max+(chi(A,X)) = chi(A,X) proof A1: dom max+(chi(A,X)) = dom chi(A,X) by MESFUNC2:def 2; now let x be Element of X; assume A2: x in dom max+(chi(A,X)); then A3: (max+(chi(A,X))).x = max((chi(A,X)).x,0.) by MESFUNC2:def 2; A4: (chi(A,X)).x in rng chi(A,X) by A1,A2,FUNCT_1:12; rng chi(A,X) c= {0,1} by FUNCT_3:48; then (chi(A,X)).x = 0 or (chi(A,X)).x = 1 by A4,TARSKI:def 2; hence (max+(chi(A,X))).x = (chi(A,X)).x by A3,XXREAL_0:def 9; end; hence thesis by A1,PARTFUN1:34; end; theorem Th24: M.E < +infty implies chi(E,X) is_integrable_on M & Integral(M,chi(E,X)) = M.E & Integral(M,(chi(E,X))|E) = M.E proof assume A1: M.E < +infty; reconsider XX = X as Element of S by MEASURE1:21; A2: XX = dom chi(E,X) & chi(E,X) is_measurable_on XX by FUNCT_3:def 3,MESFUNC2:32; then A3: XX = dom(max+(chi(E,X))) & max+(chi(E,X)) is_measurable_on XX by Th23; set F = XX \ E; for x be set st x in dom max+(chi(E,X)) holds 0. <= (max+(chi(E,X))).x by MESFUNC2:14; then A4: max+(chi(E,X)) is nonnegative by SUPINF_2:71; then A5: (max+(chi(E,X)))|E is nonnegative by MESFUNC5:21; A6: integral+(M,(max+ chi(E,X))|(E\/F)) = integral+(M,(max+ chi(E,X))|E) + integral+(M,(max+ chi(E,X))|F) by A3,A4,MESFUNC5:87,XBOOLE_1:79; A7: XX /\ F = F & XX /\ E = E by XBOOLE_1:28; then A8: dom((max+(chi(E,X)))|F) = F & dom((max+(chi(E,X)))|E) = E by A3,FUNCT_1:68; max+(chi(E,X)) is_measurable_on E & max+(chi(E,X)) is_measurable_on F by A3,MESFUNC1:34; then A9: (max+(chi(E,X)))|E is_measurable_on E & (max+(chi(E,X)))|F is_measurable_on F by A3,A7,MESFUNC5:48; E \/ F = XX by A7,XBOOLE_1:51; then A10: (max+ chi(E,X))|(E\/F) = max+ chi(E,X) by A3,RELAT_1:98; now let x be Element of X; assume A11: x in dom((max+(chi(E,X)))|F); then chi(E,X).x = 0 by A8,FUNCT_3:43; then (max+(chi(E,X))).x = 0 by Th23; hence ((max+(chi(E,X)))|F).x = 0 by A11,FUNCT_1:70; end; then integral+(M,(max+ chi(E,X))|F) = 0 by A8,A9,MESFUNC5:93; then A12: integral+(M,max+ chi(E,X)) = integral+(M,(max+ chi(E,X))|E) by A6,A10,SUPINF_2:18; A13: now let x be set; assume A14: x in dom((max+(chi(E,X)))|E); then chi(E,X).x = 1 by A8,FUNCT_3:def 3; then (max+(chi(E,X))).x = 1 by Th23; hence ((max+(chi(E,X)))|E).x = 1 by A14,FUNCT_1:70; end; then (max+(chi(E,X)))|E is_simple_func_in S by A8,MESFUNC6:2; then integral+(M,max+ chi(E,X)) = integral'(M,(max+ chi(E,X))|E) by A4,A12,MESFUNC5:21,83; then A15: integral+(M,max+ chi(E,X)) = R_EAL 1 * M.(dom((max+(chi(E,X)))|E)) by A8,A13,MESFUNC5:110; then A16: integral+(M,max+ chi(E,X)) < +infty by A1,A8,EXTREAL2:4; A17: XX = dom(max- chi(E,X)) & max- chi(E,X) is_measurable_on XX by A2,MESFUNC2:28,def 3; now let x be Element of X; assume A18: x in dom(max- chi(E,X)); A19: now assume x in E; then A20: chi(E,X).x = 1 by FUNCT_3:def 3; then ex c be Real st c = chi(E,X).x & -(chi(E,X).x) = -c by SUPINF_2:def 3; hence max(-(chi(E,X).x),0.) = 0. by A20,XXREAL_0:def 9; end; now assume not x in E; then chi(E,X).x = 0. by FUNCT_3:def 3; hence max(-(chi(E,X).x),0.) = 0. by EXTREAL1:24; end; hence (max-(chi(E,X))).x = 0 by A18,A19,MESFUNC2:def 3; end; then A21: integral+(M,max- chi(E,X)) = 0 by A17,MESFUNC5:93; hence chi(E,X) is_integrable_on M by A2,A16,MESFUNC5:def 17; Integral(M,chi(E,X)) = R_EAL 1 * M.E by A8,A15,A21,MEASURE6:21; hence Integral(M,chi(E,X)) = M.E by EXTREAL2:4; A22: E = dom((chi(E,X))|E) & (chi(E,X))|E is_measurable_on E by A8,A9,Th23; A23: (chi(E,X))|E is nonnegative by A5,Th23; A24: (chi(E,X))|E = (max+ chi(E,X))|E by Th23; Integral(M,(chi(E,X))|E) =integral+(M,(chi(E,X))|E) by A22,A23,MESFUNC5:94; hence Integral(M,(chi(E,X))|E) = M.E by A8,A12,A15,A24,EXTREAL2:4; end; theorem Th25: M.(E1/\E2) < +infty implies Integral(M,(chi(E1,X))|E2) = M.(E1/\E2) proof assume A1: M.(E1/\E2) < +infty; reconsider XX = X as Element of S by MEASURE1:21; A2: XX = dom chi(E1,X) & chi(E1,X) is_measurable_on XX by FUNCT_3:def 3,MESFUNC2:32; now let x be set; assume x in dom chi(E1,X); then A3: (chi(E1,X)).x in rng chi(E1,X) by FUNCT_1:12; rng chi(E1,X) c= {0,1} by FUNCT_3:48; hence 0. <= (chi(E1,X)).x by A3; end; then A4: chi(E1,X) is nonnegative by SUPINF_2:71; E1 /\ E2 misses E2 \ E1 & E2 = (E1 /\ E2) \/ (E2 \ E1) by XBOOLE_1:51,89; then A5: Integral(M,(chi(E1,X))|E2) = Integral(M,(chi(E1,X))|(E1/\E2)) + Integral(M,(chi(E1,X))|(E2\E1)) by A2,A4,MESFUNC5:97; A6: dom((chi(E1,X))|(E1/\E2)) = dom(chi(E1,X)) /\ (E1/\E2) by FUNCT_1:68 .= X /\ (E1/\E2) by FUNCT_3:def 3; A7: dom(chi(E1/\E2,X)|(E1/\E2)) = dom(chi(E1/\E2,X)) /\ (E1/\E2) by FUNCT_1:68 .= X /\ (E1/\E2) by FUNCT_3:def 3; now let x be Element of X; assume A8: x in dom((chi(E1,X))|(E1/\E2)); then A9: x in X & x in E1 /\ E2 by A6,XBOOLE_0:def 3; then A10: x in E1 by XBOOLE_0:def 3; A11: ((chi(E1,X))|(E1/\E2)).x = (chi(E1,X)).x by A8,FUNCT_1:70 .= 1 by A10,FUNCT_3:def 3; (chi(E1/\E2,X)|(E1/\E2)).x = (chi(E1/\E2,X)).x by A6,A7,A8,FUNCT_1:70; hence ((chi(E1,X))|(E1/\E2)).x = (chi(E1/\E2,X)|(E1/\E2)).x by A9,A11,FUNCT_3:def 3; end; then (chi(E1,X))|(E1/\E2) = chi(E1/\E2,X)|(E1/\E2) by A6,A7,PARTFUN1:34; then A12: Integral(M,(chi(E1,X))|(E1/\E2)) = M.(E1/\E2) by A1,Th24; set F = E2\E1; A13: F = dom((chi(E1,X))|(E2\E1)) by A2,RELAT_1:91; then F = dom(chi(E1,X)) /\ F by FUNCT_1:68; then A14: (chi(E1,X))|(E2\E1) is_measurable_on F by MESFUNC2:32,MESFUNC5:48; now let x be Element of X; assume A15: x in dom ((chi(E1,X))|(E2\E1)); E2 \ E1 c= X \ E1 by XBOOLE_1:33; then (chi(E1,X)).x = 0 by A13,A15,FUNCT_3:43; hence 0= ((chi(E1,X))|(E2\E1)).x by A15,FUNCT_1:70; end; then integral+(M,(chi(E1,X))|(E2\E1)) = 0 by A13,A14,MESFUNC5:93; then Integral(M,(chi(E1,X))|(E2\E1)) = 0. by A4,A13,A14,MESFUNC5:21,94; hence thesis by A5,A12,SUPINF_2:18; end; theorem f is_integrable_on M & E c= dom f & M.E < +infty & (for x be Element of X st x in E holds a <= f.x & f.x <= b) implies (R_EAL a)*M.E <= Integral(M,f|E) & Integral(M,f|E) <= (R_EAL b)*M.E proof reconsider a1=a,b1=b as Element of REAL by XREAL_0:def 1; assume that A1: f is_integrable_on M and A2: E c= dom f and A3: M.E < +infty and A4: for x be Element of X st x in E holds a <= f.x & f.x <= b; set C = chi(E,X); A5: f|E is_integrable_on M by A1,MESFUNC5:103; chi(E,X) is_integrable_on M by A3,Th24; then A6: C|E is_integrable_on M by MESFUNC5:103; then A7: a1(#)(C|E) is_integrable_on M & b1(#)(C|E) is_integrable_on M by MESFUNC5:116; for x be Element of X st x in dom(a1(#)(C|E)) holds (a1(#)(C|E)).x <= (f|E).x proof let x be Element of X; assume A8: x in dom(a1(#)(C|E)); then A9: x in dom(C|E) by MESFUNC1:def 6; then x in dom C /\ E by FUNCT_1:68; then A10: x in dom chi(E,X) & x in E by XBOOLE_0:def 3; then a <= f.x by A4; then A11: a <= (f|E).x by A10,FUNCT_1:72; (a1(#)(C|E)).x = R_EAL a * (C|E).x by A8,MESFUNC1:def 6 .= R_EAL a * C.x by A9,FUNCT_1:70 .= R_EAL a * 1. by A10,FUNCT_3:def 3; hence thesis by A11,EXTREAL2:4; end; then (f|E) - (a1(#)(C|E)) is nonnegative by Th1; then consider E1 be Element of S such that A12: E1 = dom(f|E) /\ dom(a1(#)(C|E)) & Integral(M,(a1(#)(C|E))|E1) <= Integral(M,(f|E)|E1) by A5,A7,Th3; dom(f|E) = dom f /\ E by FUNCT_1:68; then A13: dom(f|E) = E by A2,XBOOLE_1:28; dom(a1(#)(C|E)) = dom(C|E) & dom(b1(#)(C|E)) = dom(C|E) by MESFUNC1:def 6; then dom(a1(#)(C|E)) = dom C /\ E & dom(b1(#)(C|E)) = dom C /\ E by FUNCT_1:68; then dom(a1(#)(C|E)) = X /\ E & dom(b1(#)(C|E)) = X /\ E by FUNCT_3:def 3; then A14: dom(a1(#)(C|E)) = E & dom(b1(#)(C|E)) = E by XBOOLE_1:28; for x be Element of X st x in dom(f|E) holds (f|E).x <= (b1(#)(C|E)).x proof let x be Element of X; assume A15: x in dom(f|E); then A16: x in dom(C|E) by A13,A14,MESFUNC1:def 6; then x in dom C /\ E by FUNCT_1:68; then A17: x in dom chi(E,X) & x in E by XBOOLE_0:def 3; then f.x <= b by A4; then A18: (f|E).x <= b by A17,FUNCT_1:72; (b1(#)(C|E)).x = R_EAL b * (C|E).x by A13,A14,A15,MESFUNC1:def 6 .= R_EAL b * C.x by A16,FUNCT_1:70 .= R_EAL b * 1. by A17,FUNCT_3:def 3; hence thesis by A18,EXTREAL2:4; end; then (b1(#)(C|E)) - (f|E) is nonnegative by Th1; then consider E2 be Element of S such that A19: E2 = dom(f|E) /\ dom(b1(#)(C|E)) & Integral(M,(f|E)|E2) <= Integral(M,(b1(#)(C|E))|E2) by A5,A7,Th3; A20: (a1(#)(C|E))|E1 = a1(#)(C|E) & (b1(#)(C|E))|E2 = b1(#)(C|E) & (f|E)|E1 = f|E & (f|E)|E2 = f|E by A12,A13,A14,A19,RELAT_1:98; E = E/\E; then Integral(M,C|E) = M.E by A3,Th25; hence thesis by A6,A12,A19,A20,MESFUNC5:116; end;