:: The First Mean Value Theorem for Integrals
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received October 30, 2007
:: Copyright (c) 2007-2026 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, VALUED_0, POWER, XXREAL_3,
SQUARE_1, NEWTON, CARD_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
equalities MESFUNC5, XCMPLX_0, SQUARE_1, SUPINF_2, XXREAL_3;
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 E3-measurable 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 E2-measurable by A2;
then ex A be Element of S st A = dom(h+g) & (h+g) is A-measurable 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 E-measurable;
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 E-measurable 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 En-measurable by A14,A20,MESFUNC1:30,XBOOLE_1:17;
then
A23: g is En-measurable 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
;
d is R_eal by XXREAL_0:def 1; then
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 En-measurable 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; :: redefines |^ (MESFUNC7, definition)
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;
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 E-measurable holds (|.f.|) |^ k is E-measurable
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 E-measurable;
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 E-measurable 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 <r;
then E /\ great_eq_dom((|.f.|)|^k,r) = E /\ great_eq_dom(|.f.|,
r to_power (1/k)) by A14;
hence thesis by A1,A3,A4,A32,MESFUNC1:27;
end;
end;
hence thesis by A1,A4,MESFUNC1:27;
end;
end;
theorem Th15:
dom f /\ dom g = E & f is real-valued & g is real-valued & f
is E-measurable & g is E-measurable implies f(#)g is E-measurable
proof
assume that
A1: dom f /\ dom g = E and
A2: f is real-valued and
A3: g is real-valued and
A4: f is E-measurable and
A5: g is E-measurable;
A6: dom (f(#)g) = dom f /\ dom g by MESFUNC1:def 5;
A7: dom ((1/4)(#)(|.f+g.|)|^2) = dom ((|.f+g.|)|^2) by MESFUNC1:def 6;
A8: dom ((|.f-g.|)|^2) = dom |.f-g.| by Def4;
then
A9: dom ((|.f-g.|)|^2) = dom (f-g) by MESFUNC1:def 10;
then
A10: dom ((|.f-g.|)|^2) = dom f /\ dom g by A2,MESFUNC2:2;
then
A11: dom ((|.f-g.|)|^2) c= dom g by XBOOLE_1:17;
A12: dom ((1/4)(#)(|.f-g.|)|^2) = dom ((|.f-g.|)|^2) by MESFUNC1:def 6;
A13: dom ((|.f+g.|)|^2) = dom |.f+g.| by Def4;
then
A14: dom ((|.f+g.|)|^2) = dom (f+g) by MESFUNC1:def 10;
then
A15: dom ((|.f+g.|)|^2) = dom f /\ dom g by A2,MESFUNC2:2;
then
A16: dom ((|.f+g.|)|^2) c= dom g by XBOOLE_1:17;
A17: dom ((|.f+g.|)|^2) c= dom f by A15,XBOOLE_1:17;
for x be Element of X st x in dom ((|.f+g.|)|^2)
holds |. ((|.f+g.|)|^2).x .| < +infty
proof
let x be Element of X;
assume
A18: x in dom ((|. f+g .|)|^2);
then
A19: |.g.x.| < +infty by A3,A16,MESFUNC2:def 1;
|.f.x.| < +infty by A2,A17,A18,MESFUNC2:def 1;
then reconsider c1 = f.x, c2 = g.x as Element of REAL by A19,EXTREAL1:41;
f.x + g.x = c1 + c2 by SUPINF_2:1;
then |. f.x + g.x .| = |.c1+c2 qua Complex.| by EXTREAL1:12;
then
A20: |. f.x + g.x .| * |. f.x + g.x .|
= |.c1+c2 qua Complex.|*|.c1+c2 qua Complex.| by EXTREAL1:1;
((|.f+g.|)|^2).x = ((|.f+g.|).x)|^(1+1) by A18,Def4;
then
A21: ((|.f+g.|)|^2).x = (|.f+g.| .x)|^1 * (|.f+g.| .x) by Th10;
A22: |.(f+g).x.| = |. f.x+g.x .| by A14,A18,MESFUNC1:def 3;
|.f+g.| .x = |.(f+g).x.| by A13,A18,MESFUNC1:def 10;
then
|.((|.f+g.|)|^2).x.| = |. |. f.x + g.x .| * |. f.x + g.x .| .| by A21,A22
,Th9
.= |. |.(f.x + g.x) * (f.x + g.x).| .| by EXTREAL1:19
.= |.(f.x + g.x) * (f.x + g.x).|
.= |. f.x + g.x .| * |. f.x + g.x .| by EXTREAL1:19;
hence thesis by A20,XXREAL_0:9, XREAL_0:def 1;
end;
then (|.f+g.|)|^2 is real-valued by MESFUNC2:def 1;
then
A23: (1/4)(#)(|.f+g.|)|^2 is real-valued by MESFUNC2:10;
then
A24: dom ((1/4)(#)(|.f+g.|)|^2 - (1/4)(#)(|.f-g.|)|^2) = dom((1/4)(#)(|.f+g
.|)|^2) /\ dom((1/4)(#)(|.f-g.|)|^2) by MESFUNC2:2;
for x be Element of X st x in dom (f(#)g) holds (f(#)g).x = ((1/4)(#)(
|.f+g.|) |^ 2 - (1/4)(#)(|.f-g.|) |^ 2).x
proof
let x be Element of X;
assume
A25: x in dom (f(#)g);
then
A26: |.g.x.| <+infty by A3,A15,A16,A6,MESFUNC2:def 1;
|.f.x.| <+infty by A2,A15,A17,A6,A25,MESFUNC2:def 1;
then reconsider c1 = f.x, c2 = g.x as Element of REAL by A26,EXTREAL1:41;
f.x + g.x = c1 + c2 by SUPINF_2:1;
then |. f.x+g.x .| = |.c1+c2 qua Complex.| by EXTREAL1:12;
then
A27: |. f.x+g.x .| * |. f.x+g.x .|
= |.c1+c2 qua Complex.|*|.c1+c2 qua Complex.| by EXTREAL1:1;
((1/4)(#)(|.f+g.|)|^2).x = (1/4) * ((|.f+g.|)|^2).x by A15,A6,A7,A25,
MESFUNC1:def 6;
then ((1/4)(#)(|.f+g.|)|^2).x = (1/4) * (|.f+g.| .x)|^(1+1) by A15,A6
,A25,Def4;
then
A28: ((1/4)(#)(|.f+g.|)|^2).x = (1/4) * ((|.f+g.| .x)|^1 * (|.f+g.| .
x) ) by Th10;
A29: |.f+g.| .x = |.(f+g).x.| by A13,A15,A6,A25,MESFUNC1:def 10;
|.(f+g).x.| = |. f.x+g.x .| by A14,A15,A6,A25,MESFUNC1:def 3;
then ((1/4)(#)(|.f+g.|)|^2).x = (1/4) * (|. f.x+g.x .| * |. f. x+g.x
.| ) by A29,A28,Th9;
then
A30: ((1/4)(#)(|.f+g.|)|^2).x
=(1/4)*(|.c1+c2 qua Complex.|*|.c1+c2 qua Complex.|) by A27,EXTREAL1:1;
(|.c1-c2 qua Complex.|*|.c1-c2 qua Complex.|) = (|.c1-c2 qua Complex.|)^2;
then
A31: (|.c1-c2 qua Complex.|*|.c1-c2 qua Complex.|) = (c1-c2)^2 by COMPLEX1:75;
((1/4)(#)(|.f-g.|)|^2).x = (1/4) * ((|.f-g.|)|^2).x by A10,A6,A12,A25,
MESFUNC1:def 6;
then ((1/4)(#)(|.f-g.|)|^2).x = (1/4) * (|.f-g.| .x)|^(1+1) by A10,A6
,A25,Def4;
then
A32: ((1/4)(#)(|.f-g.|)|^2).x = (1/4) * ((|.f-g.| .x)|^1 * (|.f-g.| .
x) ) by Th10;
f.x - g.x = c1 - c2 by SUPINF_2:3;
then |. f.x-g.x .| = |.c1-c2 qua Complex.| by EXTREAL1:12;
then
A33: |. f.x-g.x .| * |. f.x-g.x .|
= |.c1-c2 qua Complex.|*|.c1-c2 qua Complex.| by EXTREAL1:1;
A34: |.f-g.| .x = |.(f-g).x.| by A8,A10,A6,A25,MESFUNC1:def 10;
|.(f-g).x.| = |. f.x-g.x .| by A9,A10,A6,A25,MESFUNC1:def 4;
then ((1/4)(#)(|.f-g.|)|^2).x = (1/4) * (|. f.x-g.x .| * |. f.x-g.x
.|) by A34,A32,Th9;
then
A35: ((1/4)(#)(|.f-g.|)|^2).x
=(1/4)*(|.c1-c2 qua Complex.|*|.c1-c2 qua Complex.|) by A33,EXTREAL1:1;
(|.c1+c2 qua Complex.|*|.c1+c2 qua Complex.|) = (|.c1+c2 qua Complex.|)^2;
then (|.c1+c2 qua Complex.|*|.c1+c2 qua Complex.|) = (c1+c2)^2
by COMPLEX1:75;
then
((1/4)(#)(|.f+g.|)|^2).x -((1/4)(#)(|.f-g.|)|^2).x =(1/4)*(c1^2+2*c1*
c2+c2^2) - (1/4)*(c1^2-2*c1*c2+c2^2) by A30,A35,A31,SUPINF_2:3
.= c1*c2
.= (f.x)*(g.x) by EXTREAL1:1
.= (f(#)g).x by A25,MESFUNC1:def 5;
hence thesis by A15,A10,A6,A7,A12,A24,A25,MESFUNC1:def 4;
end;
then
A36: f(#)g = (1/4)(#)(|.f+g.|)|^2 - (1/4)(#)(|.f-g.|)|^2 by A15,A10,A6,A7,A12
,A24,PARTFUN1:5;
A37: dom ((|.f-g.|)|^2) c= dom f by A10,XBOOLE_1:17;
for x be Element of X st x in dom ((|.f-g.|)|^2) holds |.((|.f-g.|)|^2)
.x .| < +infty
proof
let x be Element of X;
assume
A38: x in dom ((|.f-g.|)|^2);
then
A39: |.g.x.| < +infty by A3,A11,MESFUNC2:def 1;
|.f.x.| < +infty by A2,A37,A38,MESFUNC2:def 1;
then reconsider c1 = f.x, c2 = g.x as Element of REAL by A39,EXTREAL1:41;
f.x - g.x = c1 - c2 by SUPINF_2:3;
then |. f.x-g.x.| = |.c1-c2 qua Complex.| by EXTREAL1:12;
then
A40: |. f.x-g.x .| * |. f.x-g.x .|
= |.c1-c2 qua Complex.|*|.c1-c2 qua Complex.| by EXTREAL1:1;
((|.f-g.|)|^2).x = ((|.f-g.|).x)|^(1+1) by A38,Def4;
then
A41: ((|.f-g.|)|^2).x = ((|.f-g.|).x)|^1 * (|.f-g.|).x by Th10;
((|.f-g.|).x) = |.(f-g).x.| by A8,A38,MESFUNC1:def 10;
then ((|.f-g.|).x) = |. f.x-g.x .| by A9,A38,MESFUNC1:def 4;
then
|.((|.f-g.|)|^2).x.| = |. |. f.x - g.x .| * |. f.x - g.x .| .| by A41,Th9
.= |. |.(f.x - g.x) * (f.x - g.x).| .| by EXTREAL1:19
.= |.(f.x - g.x) * (f.x - g.x).|
.= |. f.x - g.x .| * |. f.x - g.x .| by EXTREAL1:19;
hence thesis by A40,XXREAL_0:9,XREAL_0:def 1;
end;
then (|.f-g.|)|^2 is real-valued by MESFUNC2:def 1;
then
A42: (1/4)(#)(|.f-g.|)|^2 is real-valued by MESFUNC2:10;
f+g is E-measurable by A2,A3,A4,A5,MESFUNC2:7;
then (|.f+g.|)|^2 is E-measurable by A1,A14,A15,Th14;
then
A43: (jj/4)(#)(|.f+g.|)|^2 is E-measurable by A1,A15,MESFUNC5:49;
f-g is E-measurable by A1,A2,A3,A4,A5,MESFUNC2:11,XBOOLE_1:17;
then (|.f-g.|)|^2 is E-measurable by A1,A9,A10,Th14;
then (jj/4)(#)(|.f-g.|)|^2 is E-measurable by A1,A10,MESFUNC5:49;
hence thesis by A1,A10,A12,A23,A42,A36,A43,MESFUNC2:11;
end;
theorem Th16:
rng f is real-bounded implies f is real-valued
proof
assume
A1: rng f is real-bounded;
then rng f is bounded_above by XXREAL_2:def 11;
then consider UB being Real such that
A2: UB is UpperBound of rng f by XXREAL_2:def 10;
A3: UB in REAL by XREAL_0:def 1;
rng f is bounded_below by A1,XXREAL_2:def 11;
then consider LB being Real such that
A4: LB is LowerBound of rng f by XXREAL_2:def 9;
A5: LB in REAL by XREAL_0:def 1;
now
let x be Element of X;
assume x in dom f;
then
A6: f.x in rng f by FUNCT_1:3;
then LB <= f.x by A4,XXREAL_2:def 2;
then -infty < f.x by A5,XXREAL_0:2,12;
then
A7: -(+infty) < f.x by XXREAL_3:23;
f.x <= UB by A2,A6,XXREAL_2:def 1;
then f.x < +infty by A3,XXREAL_0:2,9;
hence |. f.x .| < +infty by A7,EXTREAL1:22;
end;
hence thesis by MESFUNC2:def 1;
end;
::$N Mean value theorem for integrals (first)
theorem
for 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 st dom f /\ dom g = E & rng f =
F & g is real-valued & f is E-measurable & rng f is real-bounded & g
is_integrable_on M holds (f(#)g)|E is_integrable_on M & ex c be Element of REAL
st c >= 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 E-measurable 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 E1-measurable by A6;
A23: E1 = dom |.g.| by A21,MESFUNC1:def 10;
|.g.| is E1-measurable by A21,A22,MESFUNC2:27;
then
A24: |.g.| is E-measurable by A1,A21,MESFUNC1:30,XBOOLE_1:17;
dom f /\ dom |.g.| = E by A1,MESFUNC1:def 10;
then
A25: f(#)|.g.| is E-measurable 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 E-measurable by A1,A21,A22,MESFUNC1:30,XBOOLE_1:17;
then f(#)g is E-measurable by A1,A3,A4,A20,Th15;
then
A53: (f(#)g)|E is E-measurable 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 E-measurable 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
by EXTREAL1:2;
then reconsider c = c2 as Element of REAL;
A96: c3 qua ExtReal * (c1 qua ExtReal / c1) =
Integral(M, (f(#)|.g.|)|E) * ( Integral(M, (|.g.|
)|E) / Integral(M, (|.g.|)|E) );
Integral(M,(|.g.|)|E) * ( Integral(M,(f(#)|.g.|)|E) / Integral(M,(
|.g .|)|E) ) = c1 qua ExtReal * (c3 qua ExtReal / c1);
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;
A99: (sup F * Integral(M, (|.g.|)|E)) / Integral(M, (|.g.|)|E) =
l0 qua ExtReal*c1 qua ExtReal/c1;
l0 qua ExtReal*(c1 qua ExtReal)/c1=l0 qua ExtReal*(c1 qua ExtReal/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;
k0 qua ExtReal*c1 qua ExtReal/c1=k0 qua ExtReal*(c1 qua ExtReal/c1);
then
A102: inf F * Integral(M, (|.g.|)|E) / Integral(M, (|.g.|)|E) =
inf F qua ExtReal*(Integral(M, (|.g.|)|E) qua ExtReal
/ Integral(M, (|.g.|)|E));
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 XX-measurable by MESFUNC2:29;
then
A11: max+(chi(E,X)) is XX-measurable by Th23;
then max+(chi(E,X)) is F-measurable 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 E-measurable by A11,MESFUNC1:30;
then (max+(chi(E,X)))|E is E-measurable by A5,A14,MESFUNC5:42;
then
A23: (chi(E,X))|E is E-measurable 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 F-measurable 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 XX-measurable 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;