:: The First Mean Value Theorem for Integrals :: by Keiko Narita , Noboru Endou and Yasunari Shidama :: :: Received October 30, 2007 :: Copyright (c) 2007-2017 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, XBOOLE_0, PROB_1, MEASURE1, PARTFUN1, SUBSET_1, RELAT_1, FUNCT_1, XXREAL_0, ARYTM_1, SUPINF_2, SUPINF_1, CARD_1, REAL_1, VALUED_1, INTEGRA5, MESFUNC5, ARYTM_3, MESFUNC1, COMPLEX1, TARSKI, MESFUNC2, VALUED_0, FINSEQ_1, BINOP_1, SETWISEO, CARD_3, FINSEQ_2, NEWTON, ORDINAL4, NAT_1, POWER, SQUARE_1, XXREAL_2, ORDINAL2, RFUNCT_3, FUNCT_3, MESFUNC7, XCMPLX_0, ORDINAL1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, VALUED_0, XXREAL_3, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, XXREAL_0, XXREAL_2, MEASURE1, NAT_1, SUPINF_1, RELAT_1, RELSET_1, SETWISEO, PARTFUN1, FUNCT_1, 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, FINSOP_1, EXTREAL1, BINOP_1, NEWTON, POWER, MESFUNC1, MEASURE6, MESFUNC2, MEASURE3, SETWISEO, SQUARE_1, MESFUNC5, SUPINF_1, RELSET_1, BINOP_2, FINSEQ_2; registrations SUBSET_1, NAT_1, RELSET_1, XREAL_0, MEMBERED, ORDINAL1, FINSEQ_1, MEASURE1, NUMBERS, XXREAL_0, XBOOLE_0, VALUED_0, POWER, XXREAL_3, SQUARE_1, NEWTON, CARD_1; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; definitions TARSKI; equalities MESFUNC1, MESFUNC5, XCMPLX_0, SQUARE_1, SUPINF_2; expansions TARSKI, MESFUNC1, MESFUNC5; theorems ABSVALUE, SETWISEO, POWER, HOLDER_1, TARSKI, PARTFUN1, FUNCT_1, SUPINF_2, EXTREAL1, BINOP_1, MESFUNC1, FINSEQ_1, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_1, MESFUNC2, NEWTON, XREAL_1, COMPLEX1, XXREAL_0, FINSEQ_2, MESFUNC5, FINSOP_1, NAT_1, RELAT_1, FUNCT_3, MEASURE1, MESFUNC6, ORDINAL1, VALUED_0, XXREAL_2, XXREAL_3; 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 ExtReal; assume y in rng (g-f); then consider x being object such that A2: x in dom (g-f) and A3: y = (g-f).x by FUNCT_1:def 3; reconsider x as set by TARSKI:1; 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 5; then x in dom f by XBOOLE_0:def 4; then 0. <= g.x-f.x by A1,XXREAL_3:40; hence 0 <= y by A2,A3,MESFUNC1:def 4; end; then rng (g-f) is nonnegative by SUPINF_2:def 9; hence thesis by SUPINF_2:def 12; 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: now let x be Element of X; assume A2: x in dom ((r(#)f)|Y); then A3: x in dom (r(#)f) /\ Y by RELAT_1:61; then A4: x in Y by XBOOLE_0:def 4; A5: x in dom (r(#)f) by A3,XBOOLE_0:def 4; then x in dom f by MESFUNC1:def 6; then x in dom f /\ Y by A4,XBOOLE_0:def 4; then A6: x in dom (f|Y) by RELAT_1:61; then A7: x in dom (r(#)(f|Y)) by MESFUNC1:def 6; thus ((r(#)f)|Y).x = (r(#)f).x by A2,FUNCT_1:47 .= (r)*((f.x)) by A5,MESFUNC1:def 6 .= (r)*((f|Y).x) by A6,FUNCT_1:47 .= (r(#)(f|Y)).x by A7,MESFUNC1:def 6; end; dom ((r(#)f)|Y) = dom (r(#)f) /\ Y by RELAT_1:61 .= dom f /\ Y by MESFUNC1:def 6 .= dom (f|Y) by RELAT_1:61 .= dom (r(#)(f|Y)) by MESFUNC1:def 6; hence thesis by A1,PARTFUN1:5; end; reconsider jj = 1 as Real; 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 and A2: g is_integrable_on M and A3: g-f is nonnegative; set h=(-jj)(#)f; A4: h is_integrable_on M by A1,MESFUNC5:110; then consider E be Element of S such that A5: E = dom h /\ dom g and A6: Integral(M,h+g) = Integral(M,h|E)+Integral(M,g|E) by A2,MESFUNC5:109; A7: ex E3 be Element of S st E3 = dom h & h is_measurable_on E3 by A4; A8: g|E is_integrable_on M by A2,MESFUNC5:97; then A9: Integral(M,g|E) < +infty by MESFUNC5:96; -infty < Integral(M,g|E) by A8,MESFUNC5:96; then reconsider c2=Integral(M,g|E) as Element of REAL by A9,XXREAL_0:14; take E; A10: h|E = (-jj)(#)(f|E) by Th2; g+(-f) is nonnegative by A3,MESFUNC2:8; then A11: h+g is nonnegative by MESFUNC2:9; A12: f|E is_integrable_on M by A1,MESFUNC5:97; then A13: Integral(M,f|E) < +infty by MESFUNC5:96; -infty < Integral(M,f|E) by A12,MESFUNC5:96; then reconsider c1=Integral(M,f|E) as Element of REAL by A13,XXREAL_0:14; A14: (-jj qua ExtReal) * Integral(M,f|E) = (-jj)*c1 by EXTREAL1:1 .= -c1; ex E2 be Element of S st E2 = dom g & g is_measurable_on E2 by A2; then ex A be Element of S st A = dom(h+g) & (h+g) is_measurable_on A by A7, MESFUNC5:47; then 0 <= Integral(M,h|E)+Integral(M,g|E) by A6,A11,MESFUNC5:90; then 0 <= (-jj qua ExtReal) * Integral(M,f|E) + Integral(M,g|E) by A12,A10,MESFUNC5:110; then 0 <= -c1 + c2 by A14,XXREAL_3:def 2; then 0 +c1 <=-c1+c2+c1 by XREAL_1:6; hence thesis by A5,MESFUNC1:def 6; end; begin :: Sigma finite set registration let X; cluster nonnegative for PartFunc of X,ExtREAL; existence proof set f = the PartFunc of X,ExtREAL; take |.f.|; now let x be object; assume x in dom |.f.|; then (|.f.|).x = |.f.x.| by MESFUNC1:def 10; hence 0. <= (|.f.|).x by EXTREAL1:14; end; hence thesis by SUPINF_2:52; end; end; registration let X,f; cluster |.f.| -> nonnegative for PartFunc of X,ExtREAL; correctness proof now let x be object; assume x in dom |.f.|; then (|.f.|).x = |.f.x.| by MESFUNC1:def 10; hence 0. <= (|.f.|).x by EXTREAL1:14; end; hence thesis by SUPINF_2:52; end; end; theorem f is_integrable_on M implies ex F be sequence of S st ( for n be Element of NAT holds F.n = dom f /\ great_eq_dom(|.f.|, (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 and A3: f is_measurable_on E; defpred P[Element of NAT,set] means \$2 = E /\ great_eq_dom(|.f.|, (1/( \$1+1))); A4: dom |.f.| = E by A2,MESFUNC1:def 10; now let x be object; assume A5: x in E \ eq_dom(f, 0.); then reconsider z=x as Element of X; reconsider y=f.z as R_eal; A6: x in E by A5,XBOOLE_0:def 5; then A7: x in dom |.f.| by A2,MESFUNC1:def 10; not x in eq_dom(f, 0.) by A5,XBOOLE_0:def 5; then not y = 0. by A2,A6,MESFUNC1:def 15; then 0. < |.f.z.| by EXTREAL1:15; then 0. < (|.f.|).z by A7,MESFUNC1:def 10; then x in great_dom(|.f.|, 0.) by A7,MESFUNC1:def 13; hence x in E /\ great_dom(|.f.|, 0.) by A6,XBOOLE_0:def 4; end; then A8: E \ eq_dom(f, 0.) c= E /\ great_dom(|.f.|, 0.); now let x be object; assume A9: x in E /\ great_dom(|.f.|, 0.); then reconsider z=x as Element of X; x in great_dom(|.f.|, 0.) by A9,XBOOLE_0:def 4; then A10: 0. < (|.f.|).z by MESFUNC1:def 13; A11: x in E by A9,XBOOLE_0:def 4; then x in dom |.f.| by A2,MESFUNC1:def 10; then A12: 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 15; hence contradiction by A12,EXTREAL1:16; end; hence x in E \ eq_dom(f, 0.) by A11,XBOOLE_0:def 5; end; then A13: E /\ great_dom(|.f.|, 0.) c= E \ eq_dom(f, 0.); A14: |.f.| is_measurable_on E by A2,A3,MESFUNC2:27; A15: for n be Element of NAT ex Z be Element of S st P[n,Z] proof let n be Element of NAT; take E /\ great_eq_dom(|.f.|, (1/(n+1))); thus thesis by A14,A4,MESFUNC1:27; end; consider F be sequence of S such that A16: for n be Element of NAT holds P[n,F.n] from FUNCT_2:sch 3(A15); A17: for n be Element of NAT holds F.n in S & M.(F.n) <+infty proof let n be Element of NAT; set d = (1/(n+1)); set En=F.n; set g= (|.f.|)|En; A18: g is nonnegative by MESFUNC5:15; set z = (1/(n+1)); A19: (|.f.|)|E=|.f.| by A4,RELAT_1:69; A20: F.n = E /\ great_eq_dom(|.f.| ,(1/(n+1))) by A16; then A21: dom g = En by A4,RELAT_1:62,XBOOLE_1:17; dom |.f.| /\ En = E /\ En by A2,MESFUNC1:def 10; then A22: dom |.f.| /\ En = En by A20,XBOOLE_1:17,28; |.f.| is_measurable_on En by A14,A20,MESFUNC1:30,XBOOLE_1:17; then A23: g is_measurable_on En by A22,MESFUNC5:42; then A24: integral+(M,g) =Integral(M,g) by A21,MESFUNC5:15,88; |.f.| is_integrable_on M by A1,MESFUNC5:100; then A25: Integral(M,|.f.|) < +infty by MESFUNC5:96; A26: z* M.En / z = M.En by XXREAL_3:88; F.n c= E by A20,XBOOLE_1:17; then A27: Integral(M,g) <= Integral(M,|.f.|) by A2,A3,A4,A19,MESFUNC2:27,MESFUNC5:93 ; consider nf be PartFunc of X,ExtREAL such that A28: nf is_simple_func_in S and A29: dom nf = En and A30: for x be object st x in En holds nf.x=d by MESFUNC5:41; for x be object st x in dom nf holds nf.x >= 0 by A29,A30; then A31: nf is nonnegative by SUPINF_2:52; then A32: Integral(M,nf) = integral'(M,nf) by A28,MESFUNC5:89; A33: F.n c= great_eq_dom(|.f.|, (1/(n+1))) by A20,XBOOLE_1:17; A34: for x be Element of X st x in dom nf holds nf.x <= g.x proof let x be Element of X; assume A35: x in dom nf; then A36: (1/(n+1)) <= |.f.| .x by A33,A29,MESFUNC1:def 14; g.x = |.f.| .x by A21,A29,A35,FUNCT_1:47; hence thesis by A29,A30,A35,A36; end; nf is_measurable_on En by A28,MESFUNC2:34; then integral+(M,nf) <= integral+(M,g) by A21,A23,A18,A29,A31,A34, MESFUNC5:85; then A37: integral+(M,nf) <= Integral(M,|.f.|) by A24,A27,XXREAL_0:2; A38: +infty / z = +infty by XXREAL_3:83; integral+(M,nf) = Integral(M,nf) by A28,A31,MESFUNC5:89; then integral+(M,nf) = (1/(n+1)) * M.(En) by A29,A30,A32,MESFUNC5:104; then (1/(n+1)) * M.En < +infty by A25,A37,XXREAL_0:2; hence thesis by A26,A38,XXREAL_3:80; end; take F; for n be Element of NAT holds F.n = E /\ great_eq_dom(|.f.|, (0+1/( n+1))) by A16; then E /\ great_dom(|.f.|, 0) = union rng F by MESFUNC1:22; hence thesis by A2,A16,A13,A8,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; registration cluster extreal-yielding for FinSequence; existence proof set f = the FinSequence of ExtREAL; f is extreal-yielding; hence thesis; end; end; definition func multextreal -> BinOp of ExtREAL means :Def1: 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,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 Def1; then multextreal.(a, multextreal.(b,c)) = a * (b * c) by Def1; then multextreal.(a, multextreal.(b,c)) = a * b * c by XXREAL_3:66; then multextreal.(a, multextreal.(b,c)) = multextreal.(a * b, c) by Def1; hence thesis by Def1; end; 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 Def1; hence thesis by Def1; 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.(r,1.) = r proof let r be Element of ExtREAL; multextreal.(r,1.) = r * 1. by Def1; hence thesis by XXREAL_3:81; end; then A1: 1. is_a_right_unity_wrt multextreal by BINOP_1:def 6; for r be Element of ExtREAL holds multextreal.(1.,r) = r proof let r be Element of ExtREAL; multextreal.(1.,r) = 1. * r by Def1; hence thesis by XXREAL_3:81; end; then 1. is_a_left_unity_wrt multextreal by BINOP_1:def 5; 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:14; end; definition let F be extreal-yielding FinSequence; func Product F -> Element of ExtREAL means :Def2: 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 Nat; cluster n |-> x -> extreal-yielding; coherence; end; definition let x be Element of ExtREAL; let k be Nat; func x |^ k -> number equals Product (k |-> x); coherence; end; definition let x be Element of ExtREAL, k be Nat; 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 Def2; hence thesis by Th5,FINSOP_1:10; end; theorem Th7: for r be Element of ExtREAL holds Product (<*r*>) = r proof let r be Element of ExtREAL; reconsider r9 = r as Element of ExtREAL; reconsider F = <*r9*> as FinSequence of ExtREAL; multextreal \$\$ F = r by FINSOP_1:11; hence thesis by Def2; end; registration let f,g be extreal-yielding FinSequence; cluster f^g -> extreal-yielding; coherence proof A1: rng (f^g) = rng f \/ rng g by FINSEQ_1:31; A2: rng g c= ExtREAL by VALUED_0:def 2; rng f c= ExtREAL by VALUED_0:def 2; then rng (f^g) c= ExtREAL by A2,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; A1: rng (F^<*r*>) c= ExtREAL by VALUED_0:def 2; rng F c= ExtREAL by VALUED_0:def 2; then reconsider Fr = F^<*r*>, Ff = F as FinSequence of ExtREAL by A1, FINSEQ_1:def 4; reconsider Ff1=Ff as extreal-yielding FinSequence; Product (F^<*r*>) = multextreal \$\$ Fr by Def2; then Product (F^<*r*>) = multextreal.(multextreal \$\$ Ff,r) by FINSOP_1:4; then Product (F^<*r*>) = multextreal.(Product Ff1,r) by Def2; hence thesis by Def1; 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:59; hence thesis by Th7; end; theorem Th10: for x be Element of ExtREAL, k be Nat holds x|^(k+1) = x|^k*x proof let x be Element of ExtREAL; defpred P[Nat] means x|^(\$1+1) = x|^\$1*x; A1: for k be Nat st P[k] holds P[k+(1 qua Complex)] 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:60; hence thesis by Th8; end; x|^(0+1) = Product(<*x*>) by FINSEQ_2:59; then x|^(0+1) = x by Th7; then x|^(0+1) =1. * x by XXREAL_3:81; then A2: P[0] by Th6,FINSEQ_2:58; for k be Nat holds P[k] from NAT_1:sch 2(A2,A1); hence thesis; end; definition let k be Nat, X,f; func f|^k -> PartFunc of X,ExtREAL means :Def4: dom it = dom f & for x be Element of X st x in dom it holds it.x = (f.x)|^k; existence proof deffunc U(set) = (f.\$1) |^ k; defpred X[set] means \$1 in dom f; 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 object st x in dom f holds x in dom f3 by A1; then A3: dom f c= dom f3; for x be object st x in dom f3 holds x in dom f by A1; then dom f3 c= dom f; hence dom f3 = dom f by A3,XBOOLE_0:def 10; let d be Element of X; assume A4: d in dom f3; then f3/.d = (f.d) |^ k by A2; hence thesis by A4,PARTFUN1:def 6; end; uniqueness proof let f1,f2 be PartFunc of X, ExtREAL; assume that A5: dom f1= dom f and A6: for d being Element of X st d in dom f1 holds f1.d=(f.d) |^ k and A7: dom f2= dom f and A8: 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 A9: d in dom f; then f1.d=(f.d) |^ k by A5,A6; hence thesis by A7,A8,A9; end; hence f1=f2 by A5,A7,PARTFUN1:5; end; end; theorem Th11: for x be Element of ExtREAL, y be Real, k be Nat st x=y holds x|^k = y|^k proof let x be Element of ExtREAL, y be Real, k be Nat; defpred P[Nat] means x|^\$1=y|^\$1; assume A1: x=y; A2: for k be Nat st P[k] holds P[k+1] proof reconsider y1=y as Element of REAL by XREAL_0:def 1; let k be Nat; assume P[k]; then (x|^k)*x = (y|^k)*y by A1,EXTREAL1:1; then (x|^k)*x = y|^(k+1) by NEWTON:6; hence thesis by Th10; end; x|^0 = 1. by Th6,FINSEQ_2:58; then A3: P[0] by NEWTON:4; for k be Nat holds P[k] from NAT_1:sch 2(A3,A2); hence thesis; end; theorem Th12: for x be Element of ExtREAL, k be Nat st 0 <=x holds 0 <= x|^k proof let x be Element of ExtREAL, k be Nat; defpred P[Nat] means 0 <= x|^\$1; assume A1: 0 <=x; A2: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A3: P[k]; x|^(k+1)=(x|^k)*x by Th10; hence thesis by A1,A3; end; A4: P[0] by Th6,FINSEQ_2:58; for k be Nat holds P[k] from NAT_1:sch 2(A4,A2); hence thesis; end; theorem Th13: for k be Nat st 1<=k holds +infty|^k =+infty proof defpred P[Nat] means +infty|^\$1 = +infty; A1: for k be non zero Nat st P[k] holds P[k+1] proof let k be non zero Nat; assume A2: P[k]; +infty|^(k+1)=(+infty|^k)*+infty by Th10; hence thesis by A2,XXREAL_3:def 5; end; A3: P[1] by Th9; for k be non zero Nat holds P[k] from NAT_1:sch 10(A3,A1); hence thesis; end; theorem Th14: for k be Nat, 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 Nat; let X,S,f,E; reconsider k1=k as Element of NAT by ORDINAL1:def 12; assume that A1: E c= dom f and A2: f is_measurable_on E; A3: dom ((|.f.|)|^k) = dom |.f.| by Def4; then A4: dom ((|.f.|)|^k) = dom f by MESFUNC1:def 10; per cases; suppose A5: k = 0; A6: for r be Real st 1 < r holds E /\ less_dom((|.f.|)|^k,r) in S proof let r be Real; assume A7: 1 < r; E c= less_dom((|.f.|)|^k,r) proof let x be object; reconsider xx=x as set by TARSKI:1; assume A8: x in E; then ((|.f.|)|^k).xx = ((|.f.|).xx)|^k by A1,A4,Def4; then ((|.f.|)|^k).xx < r by A5,A7,Th6,FINSEQ_2:58; hence thesis by A1,A4,A8,MESFUNC1:def 11; end; then E /\ less_dom((|.f.|)|^k,r) = E by XBOOLE_1:28; hence thesis; end; A9: E c= dom ((|.f.|)|^k) by A1,A3,MESFUNC1:def 10; for r be Real holds E /\ less_dom((|.f.|)|^k,r) in S proof let r be Real; now assume A10: r <= 1; E c= great_eq_dom((|.f.|)|^k,r) proof let x be object; reconsider xx=x as set by TARSKI:1; assume A11: x in E; then ((|.f.|)|^k).xx = ((|.f.|).xx)|^k by A1,A4,Def4; then r <= ((|.f.|)|^k).xx by A5,A10,Th6,FINSEQ_2:58; hence thesis by A1,A4,A11,MESFUNC1:def 14; end; then E /\ great_eq_dom((|.f.|)|^k,r) = E by XBOOLE_1:28; then E /\ less_dom((|.f.|)|^k,r) = E \ E by A9,MESFUNC1:17; hence thesis; end; hence thesis by A6; end; hence thesis; end; suppose A12: k <> 0; then A13: jj/k * k = 1 by XCMPLX_1:87; A14: for r be Real st 0 < r holds great_eq_dom((|.f.|)|^k,r) = great_eq_dom(|.f.|,r to_power (1/k)) proof let r be Real; assume A15: 0 < r; A16: great_eq_dom((|.f.|)|^k,r) c= great_eq_dom(|.f.|,r to_power (1/k)) proof let x be object; reconsider xx=x as set by TARSKI:1; assume A17: x in great_eq_dom((|.f.|)|^k,r); then A18: x in dom ((|.f.|)|^k) by MESFUNC1:def 14; then A19: |.f.| .xx = |.f.xx.| by A3,MESFUNC1:def 10; then A20: 0 <= |.f.| .xx by EXTREAL1:14; per cases; suppose |.f.| .xx = +infty; then r to_power (1/k) <= |.f.| .xx by XXREAL_0:3; hence thesis by A3,A18,MESFUNC1:def 14; end; suppose |.f.| .xx <> +infty; then reconsider fx= |.f.| .xx as Element of REAL by A20,XXREAL_0:14; A21: r <= ((|.f.|)|^k).xx by A17,MESFUNC1:def 14; ((|.f.|)|^k).xx = ((|.f.|).xx)|^k by A18,Def4; then A22: r <= fx to_power k1 by A21,Th11; (fx to_power k) to_power (jj/k) = fx to_power (k * jj/k) by A12,A19, EXTREAL1:14,HOLDER_1:2; then A23: (fx to_power k) to_power (1/k) = fx by A13,POWER:25; r to_power (jj/k) <= (fx to_power k) to_power (jj/k) by A15 ,A22,HOLDER_1:3; hence thesis by A3,A18,A23,MESFUNC1:def 14; end; end; great_eq_dom(|.f.|,r to_power (1/k)) c= great_eq_dom((|.f.|) |^k,r) proof let x be object; reconsider xx=x as set by TARSKI:1; assume A24: x in great_eq_dom(|.f.|,r to_power (1/k)); then A25: x in dom |.f.| by MESFUNC1:def 14; then A26: ((|.f.|)|^k).xx = (|.f.| .xx)|^k by A3,Def4; |.f.| .xx = |.f.xx.| by A25,MESFUNC1:def 10; then A27: 0 <= |.f.| .xx by EXTREAL1:14; A28: now assume |.f.| .xx <> +infty; then reconsider fx = |.f.| .xx as Element of REAL by A27,XXREAL_0:14; reconsider R = r to_power (1/k) as Real; A29: 0 < r to_power (1/k) by A15,POWER:34; A30: R to_power k1 = r to_power (jj/k*k) by A15,POWER:33; A31: ((|.f.|)|^k).xx = fx|^k by A26,Th11; r to_power (1/k) <= |.f.| .xx by A24,MESFUNC1:def 14; then r to_power 1 <= fx to_power k by A13,A29,A30,HOLDER_1:3; hence r <=((|.f.|) |^k).xx by A31; end; now assume |.f.| .xx = +infty; then ((|.f.|).xx) |^k = +infty by A12,Th13,NAT_1:14; hence r <= ((|.f.|)|^k).xx by A26,XXREAL_0:3; end; hence thesis by A3,A25,A28,MESFUNC1:def 14; end; hence thesis by A16,XBOOLE_0:def 10; end; A32: |.f.| is_measurable_on E by A1,A2,MESFUNC2:27; for r be Real holds E /\ great_eq_dom((|.f.|)|^k,r) in S proof let r be Real; per cases; suppose A33: r <= 0; E c= great_eq_dom((|.f.|)|^k,r) proof let x be object; reconsider xx=x as set by TARSKI:1; assume A34: x in E; then A35: (|.f.|).xx = |.f.xx.| by A1,A3,A4,MESFUNC1:def 10; ((|.f.|)|^k).xx = ((|.f.|).xx)|^k by A1,A4,A34,Def4; then r <= ((|.f.|)|^k).xx by A33,A35,Th12,EXTREAL1:14; hence thesis by A1,A4,A34,MESFUNC1:def 14; end; then E /\ great_eq_dom((|.f.|)|^k,r) = E by XBOOLE_1:28; hence thesis; end; suppose 0 = inf F & c <= sup F & Integral(M, (f(#)|.g.|)|E) = 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 that A1: dom f /\ dom g = E and A2: rng f = F and A3: g is real-valued and A4: f is_measurable_on E and A5: rng f is real-bounded and A6: g is_integrable_on M; A7: dom ((f(#)|.g.|)|E) = dom (f(#)|.g.|) /\ E by RELAT_1:61; A8: rng f is Subset of REAL by A5,Th16,MESFUNC2:32; then not +infty in rng f; then A9: rng f <> {+infty} by TARSKI:def 1; A10: rng f is bounded_above by A5,XXREAL_2:def 11; not -infty in rng f by A8; then A11: rng f <> {-infty} by TARSKI:def 1; rng f is bounded_below by A5,XXREAL_2:def 11; then reconsider k0=inf F, l0=sup F as Element of REAL by A2,A10,A9,A11,XXREAL_2:57,58; A12: |.sup F.|=|.l0 qua Complex.| by EXTREAL1:12; |.inf F.|=|.k0 qua Complex.| by EXTREAL1:12; then reconsider k1= |.inf F.|, l1= |.sup F.| as Real by A12; A13: E c= dom f by A1,XBOOLE_1:17; A14: sup F is UpperBound of rng f by A2,XXREAL_2:def 3; A15: E c= dom g by A1,XBOOLE_1:17; then A16: E c= dom |.g.| by MESFUNC1:def 10; A17: dom |.g.| = dom g by MESFUNC1:def 10; for x be Element of X st x in dom |.g.| holds |. |.g.| .x.| < +infty proof let x be Element of X; assume A18: x in dom |.g.|; then |. |.g.| .x.| = |.|.g.x.|.| by MESFUNC1:def 10; then |. |.g.| .x.| = |.g.x.|; hence thesis by A3,A17,A18,MESFUNC2:def 1; end; then A19: |.g.| is real-valued by MESFUNC2:def 1; A20: f is real-valued by A5,Th16; consider E1 be Element of S such that A21: E1 = dom g and A22: g is_measurable_on E1 by A6; A23: E1 = dom |.g.| by A21,MESFUNC1:def 10; |.g.| is_measurable_on E1 by A21,A22,MESFUNC2:27; then A24: |.g.| is_measurable_on E by A1,A21,MESFUNC1:30,XBOOLE_1:17; dom f /\ dom |.g.| = E by A1,MESFUNC1:def 10; then A25: f(#)|.g.| is_measurable_on E by A4,A24,A20,A19,Th15; A26: |.g.| is_integrable_on M by A6,MESFUNC5:100; then A27: (|.g.|)|E is_integrable_on M by MESFUNC5:97; A28: dom (f(#)|.g.|) = dom f /\ dom |.g.| by MESFUNC1:def 5; then A29: dom (f(#)|.g.|) = E by A1,MESFUNC1:def 10; A30: dom (k0(#)|.g.|) = dom |.g.| by MESFUNC1:def 6; then A31: dom ((k0(#)|.g.|)|E) = E by A16,RELAT_1:62; A32: inf F is LowerBound of rng f by A2,XXREAL_2:def 4; A33: 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; A34: 0 <= |.g.x.| by EXTREAL1:14; assume A35: x in E; then A36: f.x <= sup F by A13,A14,FUNCT_1:3,XXREAL_2:def 1; inf F <= f.x by A13,A32,A35,FUNCT_1:3,XXREAL_2:def 2; hence thesis by A36,A34,XXREAL_3:71; end; 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 A37: x in dom ((k0(#)|.g.|)|E); then A38: ((k0(#)|.g.|)|E).x = (k0(#)|.g.|).x by FUNCT_1:47; (f(#)|.g.|).x = (f.x)*(|.g.|.x) by A29,A31,A37,MESFUNC1:def 5; then A39: (f(#)|.g.|).x = (f.x)*|.g.x.| by A16,A31,A37,MESFUNC1:def 10; (k0(#)|.g.|).x = ( k0)*(|.g.|).x by A16,A30,A31,A37,MESFUNC1:def 6; then (k0(#)|.g.|).x = ( k0)*|.g.x.| by A16,A31,A37,MESFUNC1:def 10; then (k0(#)|.g.|).x <= (f(#)|.g.|).x by A33,A31,A37,A39; hence thesis by A29,A7,A31,A37,A38,FUNCT_1:47; end; then A40: (f(#)|.g.|)|E - (k0(#)|.g.|)|E is nonnegative by Th1; A41: dom (l0(#)|.g.|) = dom |.g.| by MESFUNC1:def 6; then A42: dom ((l0(#)|.g.|)|E) = E by A16,RELAT_1:62; A43: dom (f(#)g) = E by A1,MESFUNC1:def 5; then A44: dom((f(#)g)|E) = E by RELAT_1:62; then A45: dom (|.(f(#)g)|E.|) = E by MESFUNC1:def 10; A46: 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 A47: x in dom ((f(#)|.g.|)|E); then A48: ((f(#)|.g.|)|E).x = (f(#)|.g.|).x by FUNCT_1:47; |. (f(#)|.g.|).x.| = |. f.x*|.g.|.x .| by A29,A7,A47,MESFUNC1:def 5 .= |. f.x*|.g.x.| .| by A1,A17,A15,A28,A7,A47,MESFUNC1:def 10 .= |.f.x.| * |. |.g.x.| .| by EXTREAL1:19 .= |.f.x.|*|.g.x.|; then A49: |. (f(#)|.g.|).x.| = |. f.x*g.x .| by EXTREAL1:19; dom |.f(#)g.| = E by A43,MESFUNC1:def 10; then A50: |.(f(#)g).|.x = |.(f(#)g).x.| by A29,A7,A47,MESFUNC1:def 10; |. ((f(#)g)|E).x .| = |. (f(#)g).x .| by A44,A29,A7,A47,FUNCT_1:47; then |.((f(#)g)|E).| .x = |. f(#)g .| .x by A45,A29,A7,A47,A50, MESFUNC1:def 10; hence thesis by A43,A29,A7,A47,A49,A50,A48,MESFUNC1:def 5; end; Integral(M, (l0(#)|.g.|)|E) = Integral(M, l0(#)((|.g.|)|E)) by Th2; then A51: Integral(M, (l0(#)|.g.|)|E) = l0 * Integral(M, (|.g.|)|E) by A27, MESFUNC5:110; A52: dom (f(#)g) /\ E = E by A43; g is_measurable_on E by A1,A21,A22,MESFUNC1:30,XBOOLE_1:17; then f(#)g is_measurable_on E by A1,A3,A4,A20,Th15; then A53: (f(#)g)|E is_measurable_on E by A52,MESFUNC5:42; A54: for x be Element of X st x in E holds |. f.x .| <= |.inf F.| + |.sup F .| proof 0 <= |.k0 qua Complex.| by COMPLEX1:46; then A55: l0+0 <=l0+|.k0 qua Complex.| by XREAL_1:6; l0 <= |.l0 qua Complex.| by COMPLEX1:76; then l0+|.k0 qua Complex.| <=|.l0 qua Complex.| + |.k0 qua Complex.| by XREAL_1:6; then A56: l0 <=|.l0 qua Complex.| + |.k0 qua Complex.| by A55,XXREAL_0:2; 0 <= |.l0 qua Complex.| by COMPLEX1:46; then A57: -|.k0 qua Complex.| -|.l0 qua Complex.| <= -|.k0 qua Complex.| -0 by XREAL_1:10; -|.k0 qua Complex.| <= k0 by COMPLEX1:76; then A58: -|.k0 qua Complex.| -|.l0 qua Complex.| <= k0 by A57,XXREAL_0:2; let x be Element of X; A59: |.k0 qua Complex.|= |.inf F.| by EXTREAL1:12; assume A60: x in E; then f.x in rng f by A13,FUNCT_1:3; then reconsider fx=f.x as Real by A8; A61: |.l0 qua Complex.| = |.sup F.| by EXTREAL1:12; fx <=l0 by A13,A14,A60,FUNCT_1:3,XXREAL_2:def 1; then A62: fx <= |.k0 qua Complex.| + |.l0 qua Complex.| by A56,XXREAL_0:2; k0 <=fx by A13,A32,A60,FUNCT_1:3,XXREAL_2:def 2; then -(|.k0 qua Complex.| + |.l0 qua Complex.|) <= fx by A58,XXREAL_0:2; then A63: |.fx qua Complex.| <= |.k0 qua Complex.| + |.l0 qua Complex.| by A62,ABSVALUE:5; |.fx qua Complex.| = |.f.x.| by EXTREAL1:12; hence thesis by A63,A59,A61,SUPINF_2:1; end; 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 A64: dom ( ((k1+l1)(#)|.g.|)|E ) = E by A16,RELAT_1:62; A65: dom ((k1+l1)(#)|.g.|) = dom |.g.| by MESFUNC1:def 6; A66: 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 A67: x in dom ((f(#)g)|E); then A68: ((f(#)g)|E).x = (f(#)g).x by FUNCT_1:47; dom (f|E) = E by A1,RELAT_1:62,XBOOLE_1:17; then A69: (f|E).x = f.x by A44,A67,FUNCT_1:47; dom (g|E) = E by A1,RELAT_1:62,XBOOLE_1:17; then A70: (g|E).x = g.x by A44,A67,FUNCT_1:47; 0 <= |.(g|E).x.| by EXTREAL1:14; then A71: |.(f|E).x.|*|.(g|E).x.| <= (|.inf F.| + |.sup F.|)*|.(g|E).x.| by A44,A54 ,A67,A69,XXREAL_3:71; A72: (((k1+l1)(#)|.g.|)|E).x = ((k1+l1)(#)|.g.|).x by A44,A64,A67,FUNCT_1:47; |.(f(#)g).x.| = |. f.x * g.x .| by A43,A44,A67,MESFUNC1:def 5; then A73: |.((f(#)g)|E).x.| = |.(f|E).x.|*|.(g|E).x.| by A68,A69,A70,EXTREAL1:19; ((k1+l1)(#)|.g.|).x = (k1+l1) * |.g.| .x by A16,A44,A65,A67, MESFUNC1:def 6; then (((k1+l1)(#)|.g.|)|E).x = (k1+l1)*|.(g|E).x.| by A16,A44,A67,A70,A72, MESFUNC1:def 10; hence thesis by A71,A73,SUPINF_2:1; end; (k1+l1)(#)|.g.| is_integrable_on M by A26,MESFUNC5:110; then A74: ((k1+l1)(#)|.g.|)|E is_integrable_on M by MESFUNC5:97; then (f(#)g)|E is_integrable_on M by A44,A64,A53,A66,MESFUNC5:102; then A75: |.((f(#)g)|E).| is_integrable_on M by MESFUNC5:100; dom (f(#)|.g.|) /\ E = E by A29; then (f(#)|.g.|)|E is_measurable_on E by A25,MESFUNC5:42; then A76: (f(#)|.g.|)|E is_integrable_on M by A45,A29,A7,A75,A46,MESFUNC5:102; then A77: -infty < Integral(M, (f(#)|.g.|)|E) by MESFUNC5:96; k0(#)|.g.| is_integrable_on M by A26,MESFUNC5:110; then (k0(#)|.g.|)|E is_integrable_on M by MESFUNC5:97; then consider V1 be Element of S such that A78: V1 = dom((k0(#)|.g.|)|E) /\ dom((f(#)|.g.|)|E) and A79: Integral(M,((k0(#)|.g.|)|E)|V1) <= Integral(M,((f(#)|.g.|)|E)|V1) by A76,A40,Th3; A80: ((f(#)|.g.|)|E)|V1 = (f(#)|.g.|)|E by A29,A7,A31,A78,RELAT_1:68; A81: dom (f(#)|.g.|) c= dom (l0(#)|.g.|) by A28,A41,XBOOLE_1:17; 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 A82: x in dom ((f(#)|.g.|)|E); then A83: ((f(#)|.g.|)|E).x = (f(#)|.g.|).x by FUNCT_1:47; (f(#)|.g.|).x = (f.x)*(|.g.|).x by A29,A7,A82,MESFUNC1:def 5; then A84: (f(#)|.g.|).x = (f.x)*|.g.x.| by A16,A29,A7,A82,MESFUNC1:def 10; (l0(#)|.g.|).x = ( l0)*(|. g.|.x) by A29,A7,A81,A82,MESFUNC1:def 6; then (l0(#)|.g.|).x = (l0)*|.g.x .| by A16,A29,A7,A82,MESFUNC1:def 10; then (f(#)|.g.|).x <= (l0(#)|.g.|).x by A29,A7,A33,A82,A84; hence thesis by A29,A7,A42,A82,A83,FUNCT_1:47; end; then A85: (l0(#)|.g.|)|E - (f(#)|.g.|)|E is nonnegative by Th1; Integral(M, (k0(#)|.g.|)|E) = Integral(M, k0(#)((|.g.|)|E)) by Th2; then A86: Integral(M, (k0(#)|.g.|)|E) = k0 * Integral(M, (|.g.|)|E) by A27, MESFUNC5:110; l0(#)|.g.| is_integrable_on M by A26,MESFUNC5:110; then (l0(#)|.g.|)|E is_integrable_on M by MESFUNC5:97; then consider V2 be Element of S such that A87: V2 = dom((l0(#)|.g.|)|E) /\ dom((f(#)|.g.|)|E) and A88: Integral(M,((f(#)|.g.|)|E)|V2) <= Integral(M,((l0(#)|.g.|)|E)|V2) by A76,A85,Th3; A89: ((f(#)|.g.|)|E)|V2 = (f(#)|.g.|)|E by A29,A7,A42,A87,RELAT_1:68; A90: ((l0(#)|.g.|)|E)|V2 = (l0(#)|.g.|)|E by A29,A7,A42,A87,RELAT_1:68; A91: Integral(M, (f(#)|.g.|)|E) < +infty by A76,MESFUNC5:96; A92: ((k0(#)|.g.|)|E)|V1 = (k0(#)|.g.|)|E by A29,A7,A31,A78,RELAT_1:68; ex c be Element of REAL st c >= inf F & c <= sup F & Integral(M,(f(#) |.g.|)|E) = c * Integral(M,(|.g.|)|E) proof per cases; suppose A93: Integral(M, (|.g.|)|E) <> 0.; reconsider c3 = Integral(M, (f(#)|.g.|)|E) as Element of REAL by A77,A91,XXREAL_0:14; set c2 = Integral(M, (f(#)|.g.|)|E) / Integral(M, (|.g.|)|E); A94: Integral(M, (|.g.|)|E) < +infty by A27,MESFUNC5:96; A95: -infty < Integral(M, (|.g.|)|E) by A27,MESFUNC5:96; then reconsider c1=Integral(M, (|.g.|)|E) as Element of REAL by A94,XXREAL_0:14; Integral(M, (f(#)|.g.|)|E) / Integral(M, (|.g.|)|E) = c3 /c1; then reconsider c = c2 as Element of REAL by XREAL_0:def 1; A96: c3 * (c1 / c1) = Integral(M, (f(#)|.g.|)|E) * ( Integral(M, (|.g.| )|E) / Integral(M, (|.g.|)|E) ) by EXTREAL1:1; Integral(M,(|.g.|)|E) * ( Integral(M,(f(#)|.g.|)|E) / Integral(M,( |.g .|)|E) ) = c1 * (c3 / c1) by EXTREAL1:1; then A97: c * Integral(M, (|.g.|)|E) = Integral(M, (f(#)|.g.|)|E) by A93,A96, XXREAL_3:88; A98: Integral(M, (|.g.|)|E) > 0. by A21,A22,A23,A93,MESFUNC2:27,MESFUNC5:92; sup F * Integral(M, (|.g.|)|E) = l0*c1 by EXTREAL1:1; then A99: (sup F * Integral(M, (|.g.|)|E)) / Integral(M, (|.g.|)|E) = l0*c1/ c1; l0*c1/c1=l0*(c1/c1); then A100: sup F * Integral(M, (|.g.|)|E) / Integral(M, (|.g.|)|E) = sup F *( Integral(M, (|.g.|)|E) / Integral(M, (|.g.|)|E)) by A99,EXTREAL1:1; inf F * Integral(M, (|.g.|)|E) = k0*c1 by EXTREAL1:1; then A101: (inf F * Integral(M, (|.g.|)|E)) / Integral(M, (|.g.|)|E) = k0 *c1 /c1; k0*c1/c1=k0*(c1/c1); then A102: inf F * Integral(M, (|.g.|)|E) / Integral(M, (|.g.|)|E) = inf F *( Integral(M, (|.g.|)|E) / Integral(M, (|.g.|)|E)) by A101,EXTREAL1:1; sup F * (Integral(M,(|.g.|)|E) / Integral(M,(|.g.|)|E)) = sup F * 1. by A93,A95,A94,XXREAL_3:78; then sup F * (Integral(M, (|.g.|)|E) / Integral(M, (|.g.|)|E)) = sup F by XXREAL_3:81; then A103: c <= sup F by A51,A88,A89,A90,A98,A100,XXREAL_3:79; inf F * (Integral(M,(|.g.|)|E) / Integral(M,(|.g.|)|E)) = inf F * 1. by A93,A95,A94,XXREAL_3:78; then inf F * (Integral(M, (|.g.|)|E) / Integral(M, (|.g.|)|E)) = inf F by XXREAL_3:81; then c >= inf F by A86,A79,A92,A80,A98,A102,XXREAL_3:79; hence thesis by A103,A97; end; suppose A104: Integral(M, (|.g.|)|E) = 0.; then 0. <= Integral(M, (f(#)|.g.|)|E) by A29,A7,A31,A86,A78,A79,A80, RELAT_1:68; then A105: Integral(M, (f(#)|.g.|)|E) = 0. by A29,A7,A42,A51,A87,A88,A89,A104, RELAT_1:68; consider y be object such that A106: y in F by XBOOLE_0:def 1; reconsider y as Element of ExtREAL by A106; A107: y <= sup F by A106,XXREAL_2:4; inf F <= y by A106,XXREAL_2:3; then A108: k0 <= sup F by A107,XXREAL_0:2; k0 * Integral(M, (|.g.|)|E) = 0. by A104; hence thesis by A108,A105; end; end; hence thesis by A44,A64,A74,A53,A66,MESFUNC5:102; end; begin :: Selected properties of integrals reserve E1,E2 for Element of S; reserve x,A for set; reserve a,b for Real; theorem Th18: (|.f.|)|A = |.(f|A).| proof dom((|.f.|)|A) = dom |.f.| /\ A by RELAT_1:61; then A1: dom((|.f.|)|A) = dom f /\ A by MESFUNC1:def 10; A2: dom(f|A) = dom f /\ A by RELAT_1:61; then A3: dom|.(f|A).| = dom f /\ A by MESFUNC1:def 10; now let x be Element of X; assume A4: x in dom((|.f.|)|A); then (|.(f|A).|).x = |. (f|A).x .| by A1,A3,MESFUNC1:def 10; then A5: (|.(f|A).|).x = |. f.x .| by A2,A1,A4,FUNCT_1:47; x in dom f by A1,A4,XBOOLE_0:def 4; then A6: x in dom |.f.| by MESFUNC1:def 10; ((|.f.|)|A).x = (|.f.|).x by A4,FUNCT_1:47; hence ((|.f.|)|A).x = (|.(f|A).|).x by A6,A5,MESFUNC1:def 10; end; hence thesis by A1,A3,PARTFUN1:5; end; theorem Th19: dom(|.f.|+|.g.|) = dom f /\ dom g & dom |.f+g.| c= dom |.f.| proof set F = |.f.|; set G = |.g.|; F is without-infty by MESFUNC5:12; then not -infty in rng F; then A1: F"{-infty} = {} by FUNCT_1:72; G is without-infty by MESFUNC5:12; then not -infty in rng G; then A2: G"{-infty} = {} by FUNCT_1:72; dom(|.f.|+|.g.|) = (dom F /\ dom G)\((F"{-infty} /\ G"{+infty}) \/ (F"{ +infty} /\ G"{-infty})) by MESFUNC1:def 3; then dom(|.f.|+|.g.|) = dom f /\ dom G by A1,A2,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 thesis by MESFUNC1:def 10; end; theorem Th20: (|.f.|)|(dom |.f+g.|) + (|.g.|)|(dom |.f+g.|) = (|.f.|+|.g.|)|( dom |.f+g.|) proof A1: (|.g.|)|(dom |.f+g.|) = |.(g|(dom |.f+g.|)).| by Th18; A2: dom |.f+g.| c= dom |.g.| by Th19; then A3: dom |.f+g.| c= dom g by MESFUNC1:def 10; dom(g|(dom |.f+g.|)) = dom g /\ dom |.f+g.| by RELAT_1:61; then A4: dom(g|(dom |.f+g.|)) = dom |.f+g.| by A3,XBOOLE_1:28; then A5: dom |.(g|(dom |.f+g.|)).| = dom |.f+g.| by MESFUNC1:def 10; A6: dom |.f+g.| c= dom |.f.| by Th19; then A7: dom |.f+g.| c= dom f by MESFUNC1:def 10; then dom |.f+g.| /\ dom |.f+g.| c= dom f /\ dom g by A3,XBOOLE_1:27; then A8: dom |.f+g.| c= dom(|.f.|+|.g.|) by Th19; then A9: dom((|.f.|+|.g.|)|(dom |.f+g.|)) = dom |.f+g.| by RELAT_1:62; dom(f|(dom |.f+g.|)) = dom f /\ dom |.f+g.| by RELAT_1:61; then A10: dom(f|(dom |.f+g.|)) = dom |.f+g.| by A7,XBOOLE_1:28; A11: (|.f.|)|(dom |.f+g.|) = |.(f|(dom |.f+g.|)).| by Th18; then A12: dom((|.f.|)|(dom |.f+g.|) + (|.g.|)|(dom |.f+g.|)) = dom (f|(dom |.f+g .|)) /\ dom (g|(dom |.f+g.|)) by A1,Th19 .= dom |.f+g.| by A10,A4; A13: dom |.(f|(dom |.f+g.|)).| = dom |.f+g.| by A10,MESFUNC1:def 10; now let x be Element of X; assume A14: x in dom((|.f.|+|.g.|)|(dom |.f+g.|)); then A15: ((|.f.|+|.g.|)|(dom |.f+g.|)).x = (|.f.|+|.g.|).x by FUNCT_1:47 .= (|.f.|).x + (|.g.|).x by A8,A9,A14,MESFUNC1:def 3 .= |. f.x .| + (|.g.|).x by A6,A9,A14,MESFUNC1:def 10; A16: x in dom |.f+g.| by A8,A14,RELAT_1:62; then ((|.f.|)|(dom |.f+g.|) + (|.g.|)|(dom |.f+g.|)).x = ((|.f.|)|(dom |.f +g.|)).x + ((|.g.|)|(dom |.f+g.|)).x by A12,MESFUNC1:def 3 .= |.(f|(dom |.f+g.|)).x .| + |.(g|(dom |.f+g.|)).|.x by A13,A11,A1,A16, MESFUNC1:def 10 .= |.(f|(dom |.f+g.|)).x .| + |.(g|(dom |.f+g.|)).x .| by A5,A16, MESFUNC1:def 10 .= |. f.x .| + |.(g|(dom |.f+g.|)).x .| by A16,FUNCT_1:49 .= |. f.x .| + |. g.x .| by A16,FUNCT_1:49; hence ((|.f.|+|.g.|)|(dom |.f+g.|)).x = ((|.f.|)|(dom |.f+g.|) + (|.g.|)|( dom |.f+g.|)).x by A2,A9,A14,A15,MESFUNC1:def 10; end; hence thesis by A12,A8,PARTFUN1:5,RELAT_1:62; end; theorem Th21: x in dom |.f+g.| implies (|.f+g.|).x <= (|.f.|+|.g.|).x proof A1: |. f.x + g.x .| <= |. f.x .| + |. g.x .| by EXTREAL1:24; assume A2: x in dom |.f+g.|; then x in dom (f+g) by MESFUNC1:def 10; then A3: |. (f+g).x .| <= |. f.x .| + |. g.x .| by A1,MESFUNC1:def 3; A4: dom |.f+g.| c= dom |.g.| by Th19; then A5: |. g.x .| = |.g.| .x by A2,MESFUNC1:def 10; x in dom |.g.| by A2,A4; then A6: x in dom g by MESFUNC1:def 10; A7: dom |.f+g.| c= dom |.f.| by Th19; then x in dom |.f.| by A2; then x in dom f by MESFUNC1:def 10; then x in dom f /\ dom g by A6,XBOOLE_0:def 4; then A8: x in dom(|.f.| + |.g.|) by Th19; |. f.x .| = |.f.| .x by A2,A7,MESFUNC1:def 10; then |. f.x .| + |. g.x .| = (|.f.| + |.g.|).x by A5,A8,MESFUNC1:def 3; hence thesis by A2,A3,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 that A1: f is_integrable_on M and A2: g is_integrable_on M; A3: |.g.| is_integrable_on M by A2,MESFUNC5:100; A4: f+g is_integrable_on M by A1,A2,MESFUNC5:108; A5: |.f+g.| is_integrable_on M by A4,MESFUNC5:100; for x be Element of X st x in dom |.f+g.| holds (|.f+g.|).x <= (|.f.|+ |.g.|).x by Th21; then A6: (|.f.|+|.g.|) - |.f+g.| is nonnegative by Th1; set G = |.g.|; set F = |.f.|; A7: 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; A8: |.f.| is_integrable_on M by A1,MESFUNC5:100; then |.f.|+|.g.| is_integrable_on M by A3,MESFUNC5:108; then consider E be Element of S such that A9: E = dom(|.f.|+|.g.|) /\ dom |.f+g.| and A10: Integral(M,(|.f+g.|)|E) <= Integral(M,(|.f.|+|.g.|)|E) by A5,A6,Th3; A11: G|E is_integrable_on M by A3,MESFUNC5:97; F|E is_integrable_on M by A8,MESFUNC5:97; then consider E1 be Element of S such that A12: E1 = dom (F|E) /\ dom (G|E) and A13: Integral(M,F|E+G|E) = Integral(M,(F|E)|E1) + Integral(M,(G|E)|E1) by A11,MESFUNC5:109; take E; dom(G|E) = dom G /\ E by RELAT_1:61; then A14: dom(G|E) = dom g /\ E by MESFUNC1:def 10; A15: dom (|.f.|+|.g.|) = dom f /\ dom g by Th19; then A16: E = dom |.f+g.| by A9,A7,XBOOLE_1:28,36; dom(F|E) = dom F /\ E by RELAT_1:61; then dom(F|E) = dom f /\ E by MESFUNC1:def 10; then E1 = (dom f /\ E /\ E) /\ dom g by A12,A14,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 A17: E1 = E by A9,A15,A7,XBOOLE_1:28,36; then A18: (G|E)|E1 = G|E by FUNCT_1:51; (F|E)|E1 = F|E by A17,FUNCT_1:51; hence thesis by A10,A13,A16,A18,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; A2: rng chi(A,X) c= {0,1} by FUNCT_3:39; assume A3: x in dom max+(chi(A,X)); then A4: (max+(chi(A,X))).x = max((chi(A,X)).x,0.) by MESFUNC2:def 2; (chi(A,X)).x in rng chi(A,X) by A1,A3,FUNCT_1:3; hence (max+(chi(A,X))).x = (chi(A,X)).x by A4,A2,XXREAL_0:def 10; end; hence thesis by A1,PARTFUN1:5; 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 reconsider XX = X as Element of S by MEASURE1:7; set F = XX \ E; A1: now let x be Element of X; A2: now assume x in E; then chi(E,X).x = 1 by FUNCT_3:def 3; hence max(-(chi(E,X).x),0.) = 0. by XXREAL_0:def 10; end; A3: now assume not x in E; then chi(E,X).x = 0. by FUNCT_3:def 3; then -chi(E,X).x = 0; hence max(-(chi(E,X).x),0.) = 0.; end; assume x in dom(max- chi(E,X)); hence (max-(chi(E,X))).x = 0 by A2,A3,MESFUNC2:def 3; end; A4: XX = dom chi(E,X) by FUNCT_3:def 3; then A5: XX = dom(max+(chi(E,X))) by Th23; A6: XX /\ F = F by XBOOLE_1:28; then A7: dom((max+(chi(E,X)))|F) = F by A5,RELAT_1:61; A8: now let x be Element of X; assume A9: x in dom((max+(chi(E,X)))|F); then chi(E,X).x = 0 by A7,FUNCT_3:37; then (max+(chi(E,X))).x = 0 by Th23; hence ((max+(chi(E,X)))|F).x = 0 by A9,FUNCT_1:47; end; A10: chi(E,X) is_measurable_on XX by MESFUNC2:29; then A11: max+(chi(E,X)) is_measurable_on XX by Th23; then max+(chi(E,X)) is_measurable_on F by MESFUNC1:30; then A12: integral+(M,(max+ chi(E,X))|F) = 0 by A5,A6,A7,A8,MESFUNC5:42,87; XX = dom(max- chi(E,X)) by A4,MESFUNC2:def 3; then A13: integral+(M,max- chi(E,X)) = 0 by A4,A10,A1,MESFUNC2:26,MESFUNC5:87; A14: XX /\ E = E by XBOOLE_1:28; then A15: dom((max+(chi(E,X)))|E) = E by A5,RELAT_1:61; E \/ F = XX by A14,XBOOLE_1:51; then A16: (max+ chi(E,X))|(E\/F) = max+ chi(E,X) by A5,RELAT_1:69; A17: for x be object st x in dom max+(chi(E,X)) holds 0. <= (max+(chi(E,X))).x by MESFUNC2:12; then A18: max+(chi(E,X)) is nonnegative by SUPINF_2:52; then integral+(M,(max+ chi(E,X))|(E\/F)) = integral+(M,(max+ chi(E,X))|E) + integral+(M,(max+ chi(E,X))|F) by A5,A11,MESFUNC5:81,XBOOLE_1:79; then A19: integral+(M,max+ chi(E,X)) = integral+(M,(max+ chi(E,X))|E) by A16,A12, XXREAL_3:4; A20: now let x be object; assume A21: x in dom((max+(chi(E,X)))|E); then chi(E,X).x = 1 by A15,FUNCT_3:def 3; then (max+(chi(E,X))).x = 1 by Th23; hence ((max+(chi(E,X)))|E).x = jj by A21,FUNCT_1:47; end; then (max+(chi(E,X)))|E is_simple_func_in S by A15,MESFUNC6:2; then integral+(M,max+ chi(E,X)) = integral'(M,(max+ chi(E,X))|E) by A18,A19, MESFUNC5:15,77; then A22: integral+(M,max+ chi(E,X)) = jj * M.(dom((max+(chi(E,X)))|E)) by A15,A20,MESFUNC5:104; max+(chi(E,X)) is_measurable_on E by A11,MESFUNC1:30; then (max+(chi(E,X)))|E is_measurable_on E by A5,A14,MESFUNC5:42; then A23: (chi(E,X))|E is_measurable_on E by Th23; (max+(chi(E,X)))|E is nonnegative by A17,MESFUNC5:15,SUPINF_2:52; then A24: (chi(E,X))|E is nonnegative by Th23; E = dom((chi(E,X))|E) by A15,Th23; then A25: Integral(M,(chi(E,X))|E) =integral+(M,(chi(E,X))|E) by A23,A24,MESFUNC5:88 ; assume M.E < +infty; then integral+(M,max+ chi(E,X)) < +infty by A15,A22,XXREAL_3:81; hence chi(E,X) is_integrable_on M by A4,A10,A13; Integral(M,chi(E,X)) = 1 * M.E by A15,A22,A13,XXREAL_3:15; hence Integral(M,chi(E,X)) = M.E by XXREAL_3:81; (chi(E,X))|E = (max+ chi(E,X))|E by Th23; hence thesis by A15,A19,A22,A25,XXREAL_3:81; end; theorem Th25: M.(E1/\E2) < +infty implies Integral(M,(chi(E1,X))|E2) = M.(E1/\ E2) proof reconsider XX = X as Element of S by MEASURE1:7; A1: E2 = (E1 /\ E2) \/ (E2 \ E1) by XBOOLE_1:51; set F = E2\E1; A2: dom((chi(E1,X))|(E1/\E2)) = dom(chi(E1,X)) /\ (E1/\E2) by RELAT_1:61 .= X /\ (E1/\E2) by FUNCT_3:def 3; A3: dom(chi(E1/\E2,X)|(E1/\E2)) = dom(chi(E1/\E2,X)) /\ (E1/\E2) by RELAT_1:61 .= X /\ (E1/\E2) by FUNCT_3:def 3; now let x be Element of X; assume A4: x in dom((chi(E1,X))|(E1/\E2)); then A5: (chi(E1/\E2,X)|(E1/\E2)).x = (chi(E1/\E2,X)).x by A2,A3,FUNCT_1:47; A6: x in E1 /\ E2 by A2,A4,XBOOLE_0:def 4; then A7: x in E1 by XBOOLE_0:def 4; ((chi(E1,X))|(E1/\E2)).x = (chi(E1,X)).x by A4,FUNCT_1:47 .= 1 by A7,FUNCT_3:def 3; hence ((chi(E1,X))|(E1/\E2)).x = (chi(E1/\E2,X)|(E1/\E2)).x by A6,A5, FUNCT_3:def 3; end; then A8: (chi(E1,X))|(E1/\E2) = chi(E1/\E2,X)|(E1/\E2) by A2,A3,PARTFUN1:5; assume M.(E1/\E2) < +infty; then A9: Integral(M,(chi(E1,X))|(E1/\E2)) = M.(E1/\E2) by A8,Th24; A10: XX = dom chi(E1,X) by FUNCT_3:def 3; then A11: F = dom((chi(E1,X))|(E2\E1)) by RELAT_1:62; then F = dom(chi(E1,X)) /\ F by RELAT_1:61; then A12: (chi(E1,X))|(E2\E1) is_measurable_on F by MESFUNC2:29,MESFUNC5:42; now let x be object; assume x in dom chi(E1,X); then A13: (chi(E1,X)).x in rng chi(E1,X) by FUNCT_1:3; rng chi(E1,X) c= {0,1} by FUNCT_3:39; hence 0. <= (chi(E1,X)).x by A13; end; then A14: chi(E1,X) is nonnegative by SUPINF_2:52; 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 A11,A15,FUNCT_3:37; hence 0= ((chi(E1,X))|(E2\E1)).x by A15,FUNCT_1:47; end; then integral+(M,(chi(E1,X))|(E2\E1)) = 0 by A11,A12,MESFUNC5:87; then A16: Integral(M,(chi(E1,X))|(E2\E1)) = 0. by A14,A11,A12,MESFUNC5:15,88; chi(E1,X) is_measurable_on XX by MESFUNC2:29; then Integral(M,(chi(E1,X))|E2) = Integral(M,(chi(E1,X))|(E1/\E2)) + Integral(M,(chi(E1,X))|(E2\E1)) by A10,A14,A1,MESFUNC5:91,XBOOLE_1:89; hence thesis by A9,A16,XXREAL_3:4; 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 ( a)*M.E <= Integral(M,f |E) & Integral(M,f|E) <= (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:97; 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 A6: x in dom(a1(#)(C|E)); then A7: x in dom(C|E) by MESFUNC1:def 6; then x in dom C /\ E by RELAT_1:61; then A8: x in E by XBOOLE_0:def 4; then a <= f.x by A4; then A9: a <= (f|E).x by A8,FUNCT_1:49; (a1(#)(C|E)).x = a * (C|E).x by A6,MESFUNC1:def 6 .= a * C.x by A7,FUNCT_1:47 .= a * 1. by A8,FUNCT_3:def 3; hence thesis by A9,XXREAL_3:81; end; then A10: (f|E) - (a1(#)(C|E)) is nonnegative by Th1; chi(E,X) is_integrable_on M by A3,Th24; then A11: C|E is_integrable_on M by MESFUNC5:97; then a1(#)(C|E) is_integrable_on M by MESFUNC5:110; then consider E1 be Element of S such that A12: E1 = dom(f|E) /\ dom(a1(#)(C|E)) and A13: Integral(M,(a1(#)(C|E))|E1) <= Integral(M,(f|E)|E1) by A5,A10,Th3; dom(f|E) = dom f /\ E by RELAT_1:61; then A14: dom(f|E) = E by A2,XBOOLE_1:28; dom(a1(#)(C|E)) = dom(C|E) by MESFUNC1:def 6; then dom(a1(#)(C|E)) = dom C /\ E by RELAT_1:61; then dom(a1(#)(C|E)) = X /\ E by FUNCT_3:def 3; then A15: dom(a1(#)(C|E)) = E by XBOOLE_1:28; then A16: (f|E)|E1 = f|E by A12,A14,RELAT_1:69; dom(b1(#)(C|E)) = dom(C|E) by MESFUNC1:def 6; then dom(b1(#)(C|E)) = dom C /\ E by RELAT_1:61; then dom(b1(#)(C|E)) = X /\ E by FUNCT_3:def 3; then A17: 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 A18: x in dom(f|E); then A19: x in dom(C|E) by A14,A15,MESFUNC1:def 6; then x in dom C /\ E by RELAT_1:61; then A20: x in E by XBOOLE_0:def 4; then f.x <= b by A4; then A21: (f|E).x <= b by A20,FUNCT_1:49; (b1(#)(C|E)).x = b * (C|E).x by A14,A17,A18,MESFUNC1:def 6 .= b * C.x by A19,FUNCT_1:47 .= b * 1. by A20,FUNCT_3:def 3; hence thesis by A21,XXREAL_3:81; end; then A22: (b1(#)(C|E)) - (f|E) is nonnegative by Th1; b1(#)(C|E) is_integrable_on M by A11,MESFUNC5:110; then consider E2 be Element of S such that A23: E2 = dom(f|E) /\ dom(b1(#)(C|E)) and A24: Integral(M,(f|E)|E2) <= Integral(M,(b1(#)(C|E))|E2) by A5,A22,Th3; A25: (b1(#)(C|E))|E2 = b1(#)(C|E) by A14,A17,A23,RELAT_1:69; E = E/\E; then A26: Integral(M,C|E) = M.E by A3,Th25; A27: (f|E)|E2 = f|E by A14,A17,A23,RELAT_1:69; (a1(#)(C|E))|E1 = a1(#)(C|E) by A12,A14,A15,RELAT_1:69; hence thesis by A11,A13,A24,A25,A16,A27,A26,MESFUNC5:110; end;