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