:: MESFUNC7 semantic presentation
begin
theorem Th1: :: MESFUNC7:1
for X being non empty set
for f, g being PartFunc of X,ExtREAL st ( for x being Element of X st x in dom f holds
f . x <= g . x ) holds
g - f is nonnegative
proof
let X be non empty set ; ::_thesis: for f, g being PartFunc of X,ExtREAL st ( for x being Element of X st x in dom f holds
f . x <= g . x ) holds
g - f is nonnegative
let f, g be PartFunc of X,ExtREAL; ::_thesis: ( ( for x being Element of X st x in dom f holds
f . x <= g . x ) implies g - f is nonnegative )
assume A1: for x being Element of X st x in dom f holds
f . x <= g . x ; ::_thesis: g - f is nonnegative
now__::_thesis:_for_y_being_R_eal_st_y_in_rng_(g_-_f)_holds_
0_<=_y
let y be R_eal; ::_thesis: ( y in rng (g - f) implies 0 <= y )
assume y in rng (g - f) ; ::_thesis: 0 <= y
then consider x being set such that
A2: x in dom (g - f) and
A3: y = (g - f) . x by FUNCT_1:def_3;
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; ::_thesis: verum
end;
then rng (g - f) is nonnegative by SUPINF_2:def_9;
hence g - f is nonnegative by SUPINF_2:def_16; ::_thesis: verum
end;
theorem Th2: :: MESFUNC7:2
for X being non empty set
for Y being set
for f being PartFunc of X,ExtREAL
for r being Real holds (r (#) f) | Y = r (#) (f | Y)
proof
let X be non empty set ; ::_thesis: for Y being set
for f being PartFunc of X,ExtREAL
for r being Real holds (r (#) f) | Y = r (#) (f | Y)
let Y be set ; ::_thesis: for f being PartFunc of X,ExtREAL
for r being Real holds (r (#) f) | Y = r (#) (f | Y)
let f be PartFunc of X,ExtREAL; ::_thesis: for r being Real holds (r (#) f) | Y = r (#) (f | Y)
let r be Real; ::_thesis: (r (#) f) | Y = r (#) (f | Y)
A1: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((r_(#)_f)_|_Y)_holds_
((r_(#)_f)_|_Y)_._x_=_(r_(#)_(f_|_Y))_._x
let x be Element of X; ::_thesis: ( x in dom ((r (#) f) | Y) implies ((r (#) f) | Y) . x = (r (#) (f | Y)) . x )
assume A2: x in dom ((r (#) f) | Y) ; ::_thesis: ((r (#) f) | Y) . x = (r (#) (f | Y)) . x
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_EAL r) * (f . x) by A5, MESFUNC1:def_6
.= (R_EAL r) * ((f | Y) . x) by A6, FUNCT_1:47
.= (r (#) (f | Y)) . x by A7, MESFUNC1:def_6 ; ::_thesis: verum
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 (r (#) f) | Y = r (#) (f | Y) by A1, PARTFUN1:5; ::_thesis: verum
end;
theorem Th3: :: MESFUNC7:3
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )
let f, g be PartFunc of X,ExtREAL; ::_thesis: ( f is_integrable_on M & g is_integrable_on M & g - f is nonnegative implies ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) ) )
assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M and
A3: g - f is nonnegative ; ::_thesis: ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )
set h = (- 1) (#) f;
A4: (- 1) (#) f is_integrable_on M by A1, MESFUNC5:110;
then consider E being Element of S such that
A5: E = (dom ((- 1) (#) f)) /\ (dom g) and
A6: Integral (M,(((- 1) (#) f) + g)) = (Integral (M,(((- 1) (#) f) | E))) + (Integral (M,(g | E))) by A2, MESFUNC5:109;
A7: ex E3 being Element of S st
( E3 = dom ((- 1) (#) f) & (- 1) (#) f is_measurable_on E3 ) by A4, MESFUNC5:def_17;
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 Real by A9, XXREAL_0:14;
take E ; ::_thesis: ( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )
A10: ((- 1) (#) f) | E = (- 1) (#) (f | E) by Th2;
g + (- f) is nonnegative by A3, MESFUNC2:8;
then A11: ((- 1) (#) f) + 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 Real by A13, XXREAL_0:14;
A14: (R_EAL (- 1)) * (Integral (M,(f | E))) = (- 1) * c1 by EXTREAL1:1;
ex E2 being Element of S st
( E2 = dom g & g is_measurable_on E2 ) by A2, MESFUNC5:def_17;
then ex A being Element of S st
( A = dom (((- 1) (#) f) + g) & ((- 1) (#) f) + g is_measurable_on A ) by A7, MESFUNC5:47;
then 0 <= (Integral (M,(((- 1) (#) f) | E))) + (Integral (M,(g | E))) by A6, A11, MESFUNC5:90;
then 0 <= ((R_EAL (- 1)) * (Integral (M,(f | E)))) + (Integral (M,(g | E))) by A12, A10, MESFUNC5:110;
then 0 <= (- c1) + c2 by A14, SUPINF_2:1;
then 0 + c1 <= ((- c1) + c2) + c1 by XREAL_1:6;
hence ( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) ) by A5, MESFUNC1:def_6; ::_thesis: verum
end;
begin
registration
let X be non empty set ;
cluster Relation-like X -defined ExtREAL -valued V18() extreal-yielding nonnegative for Element of K6(K7(X,ExtREAL));
existence
ex b1 being PartFunc of X,ExtREAL st b1 is nonnegative
proof
set f = the PartFunc of X,ExtREAL;
take |. the PartFunc of X,ExtREAL.| ; ::_thesis: |. the PartFunc of X,ExtREAL.| is nonnegative
now__::_thesis:_for_x_being_set_st_x_in_dom_|._the_PartFunc_of_X,ExtREAL.|_holds_
0._<=_|._the_PartFunc_of_X,ExtREAL.|_._x
let x be set ; ::_thesis: ( x in dom |. the PartFunc of X,ExtREAL.| implies 0. <= |. the PartFunc of X,ExtREAL.| . x )
assume x in dom |. the PartFunc of X,ExtREAL.| ; ::_thesis: 0. <= |. the PartFunc of X,ExtREAL.| . x
then |. the PartFunc of X,ExtREAL.| . x = |.( the PartFunc of X,ExtREAL . x).| by MESFUNC1:def_10;
hence 0. <= |. the PartFunc of X,ExtREAL.| . x by EXTREAL2:3; ::_thesis: verum
end;
hence |. the PartFunc of X,ExtREAL.| is nonnegative by SUPINF_2:52; ::_thesis: verum
end;
end;
registration
let X be non empty set ;
let f be PartFunc of X,ExtREAL;
cluster|.f.| -> nonnegative for PartFunc of X,ExtREAL;
correctness
coherence
for b1 being PartFunc of X,ExtREAL st b1 = |.f.| holds
b1 is nonnegative ;
proof
now__::_thesis:_for_x_being_set_st_x_in_dom_|.f.|_holds_
0._<=_|.f.|_._x
let x be set ; ::_thesis: ( x in dom |.f.| implies 0. <= |.f.| . x )
assume x in dom |.f.| ; ::_thesis: 0. <= |.f.| . x
then |.f.| . x = |.(f . x).| by MESFUNC1:def_10;
hence 0. <= |.f.| . x by EXTREAL2:3; ::_thesis: verum
end;
hence for b1 being PartFunc of X,ExtREAL st b1 = |.f.| holds
b1 is nonnegative by SUPINF_2:52; ::_thesis: verum
end;
end;
theorem :: MESFUNC7:4
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_integrable_on M holds
ex F being Function of NAT,S st
( ( for n being 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 being Element of NAT holds
( F . n in S & M . (F . n) < +infty ) ) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_integrable_on M holds
ex F being Function of NAT,S st
( ( for n being 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 being Element of NAT holds
( F . n in S & M . (F . n) < +infty ) ) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_integrable_on M holds
ex F being Function of NAT,S st
( ( for n being 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 being Element of NAT holds
( F . n in S & M . (F . n) < +infty ) ) )
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,ExtREAL st f is_integrable_on M holds
ex F being Function of NAT,S st
( ( for n being 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 being Element of NAT holds
( F . n in S & M . (F . n) < +infty ) ) )
let f be PartFunc of X,ExtREAL; ::_thesis: ( f is_integrable_on M implies ex F being Function of NAT,S st
( ( for n being 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 being Element of NAT holds
( F . n in S & M . (F . n) < +infty ) ) ) )
assume A1: f is_integrable_on M ; ::_thesis: ex F being Function of NAT,S st
( ( for n being 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 being Element of NAT holds
( F . n in S & M . (F . n) < +infty ) ) )
then consider E being Element of S such that
A2: E = dom f and
A3: f is_measurable_on E by MESFUNC5:def_17;
defpred S1[ Element of NAT , set ] means $2 = E /\ (great_eq_dom (|.f.|,(R_EAL (1 / ($1 + 1)))));
A4: dom |.f.| = E by A2, MESFUNC1:def_10;
now__::_thesis:_for_x_being_set_st_x_in_E_\_(eq_dom_(f,0.))_holds_
x_in_E_/\_(great_dom_(|.f.|,0.))
let x be set ; ::_thesis: ( x in E \ (eq_dom (f,0.)) implies x in E /\ (great_dom (|.f.|,0.)) )
assume A5: x in E \ (eq_dom (f,0.)) ; ::_thesis: x in E /\ (great_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 EXTREAL2:4;
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; ::_thesis: verum
end;
then A8: E \ (eq_dom (f,0.)) c= E /\ (great_dom (|.f.|,0.)) by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_E_/\_(great_dom_(|.f.|,0.))_holds_
x_in_E_\_(eq_dom_(f,0.))
let x be set ; ::_thesis: ( x in E /\ (great_dom (|.f.|,0.)) implies x in E \ (eq_dom (f,0.)) )
assume A9: x in E /\ (great_dom (|.f.|,0.)) ; ::_thesis: x in E \ (eq_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.) ; ::_thesis: contradiction
then f . z = 0. by MESFUNC1:def_15;
hence contradiction by A12, EXTREAL2:5; ::_thesis: verum
end;
hence x in E \ (eq_dom (f,0.)) by A11, XBOOLE_0:def_5; ::_thesis: verum
end;
then A13: E /\ (great_dom (|.f.|,0.)) c= E \ (eq_dom (f,0.)) by TARSKI:def_3;
A14: |.f.| is_measurable_on E by A2, A3, MESFUNC2:27;
A15: for n being Element of NAT ex Z being Element of S st S1[n,Z]
proof
let n be Element of NAT ; ::_thesis: ex Z being Element of S st S1[n,Z]
take E /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ; ::_thesis: ( E /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) is Element of S & S1[n,E /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1)))))] )
thus ( E /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) is Element of S & S1[n,E /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1)))))] ) by A14, A4, MESFUNC1:27; ::_thesis: verum
end;
consider F being Function of NAT,S such that
A16: for n being Element of NAT holds S1[n,F . n] from FUNCT_2:sch_3(A15);
A17: for n being Element of NAT holds
( F . n in S & M . (F . n) < +infty )
proof
let n be Element of NAT ; ::_thesis: ( F . n in S & M . (F . n) < +infty )
set d = R_EAL (1 / (n + 1));
set En = F . n;
set g = |.f.| | (F . n);
A18: |.f.| | (F . n) is nonnegative by MESFUNC5:15;
set z = R_EAL (1 / (n + 1));
A19: |.f.| | E = |.f.| by A4, RELAT_1:69;
A20: F . n = E /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) by A16;
then A21: dom (|.f.| | (F . n)) = F . n by A4, RELAT_1:62, XBOOLE_1:17;
(dom |.f.|) /\ (F . n) = E /\ (F . n) by A2, MESFUNC1:def_10;
then A22: (dom |.f.|) /\ (F . n) = F . n by A20, XBOOLE_1:17, XBOOLE_1:28;
|.f.| is_measurable_on F . n by A14, A20, MESFUNC1:30, XBOOLE_1:17;
then A23: |.f.| | (F . n) is_measurable_on F . n by A22, MESFUNC5:42;
then A24: integral+ (M,(|.f.| | (F . n))) = Integral (M,(|.f.| | (F . n))) by A21, MESFUNC5:15, MESFUNC5:88;
|.f.| is_integrable_on M by A1, A2, A3, MESFUNC5:100;
then A25: Integral (M,|.f.|) < +infty by MESFUNC5:96;
A26: ((R_EAL (1 / (n + 1))) * (M . (F . n))) / (R_EAL (1 / (n + 1))) = M . (F . n) by XXREAL_3:88;
F . n c= E by A20, XBOOLE_1:17;
then A27: Integral (M,(|.f.| | (F . n))) <= Integral (M,|.f.|) by A2, A3, A4, A19, MESFUNC2:27, MESFUNC5:93;
consider nf being PartFunc of X,ExtREAL such that
A28: nf is_simple_func_in S and
A29: dom nf = F . n and
A30: for x being set st x in F . n holds
nf . x = R_EAL (1 / (n + 1)) by MESFUNC5:41;
for x being set 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.|,(R_EAL (1 / (n + 1)))) by A20, XBOOLE_1:17;
A34: for x being Element of X st x in dom nf holds
nf . x <= (|.f.| | (F . n)) . x
proof
let x be Element of X; ::_thesis: ( x in dom nf implies nf . x <= (|.f.| | (F . n)) . x )
assume A35: x in dom nf ; ::_thesis: nf . x <= (|.f.| | (F . n)) . x
then A36: R_EAL (1 / (n + 1)) <= |.f.| . x by A33, A29, MESFUNC1:def_14;
(|.f.| | (F . n)) . x = |.f.| . x by A21, A29, A35, FUNCT_1:47;
hence nf . x <= (|.f.| | (F . n)) . x by A29, A30, A35, A36; ::_thesis: verum
end;
nf is_measurable_on F . n by A28, MESFUNC2:34;
then integral+ (M,nf) <= integral+ (M,(|.f.| | (F . n))) 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 / (R_EAL (1 / (n + 1))) = +infty by XXREAL_3:83;
integral+ (M,nf) = Integral (M,nf) by A28, A31, MESFUNC5:89;
then integral+ (M,nf) = (R_EAL (1 / (n + 1))) * (M . (F . n)) by A29, A30, A32, MESFUNC5:104;
then (R_EAL (1 / (n + 1))) * (M . (F . n)) < +infty by A25, A37, XXREAL_0:2;
hence ( F . n in S & M . (F . n) < +infty ) by A26, A38, XXREAL_3:80; ::_thesis: verum
end;
take F ; ::_thesis: ( ( for n being 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 being Element of NAT holds
( F . n in S & M . (F . n) < +infty ) ) )
for n being Element of NAT holds F . n = E /\ (great_eq_dom (|.f.|,(R_EAL (0 + (1 / (n + 1)))))) by A16;
then E /\ (great_dom (|.f.|,(R_EAL 0))) = union (rng F) by MESFUNC1:22;
hence ( ( for n being 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 being Element of NAT holds
( F . n in S & M . (F . n) < +infty ) ) ) by A2, A16, A13, A8, A17, XBOOLE_0:def_10; ::_thesis: verum
end;
begin
notation
let F be Relation;
synonym extreal-yielding F for ext-real-valued ;
end;
registration
cluster Relation-like NAT -defined V18() V34() FinSequence-like FinSubsequence-like extreal-yielding for set ;
existence
ex b1 being FinSequence st b1 is extreal-yielding
proof
set f = the FinSequence of ExtREAL ;
the FinSequence of ExtREAL is extreal-yielding ;
hence ex b1 being FinSequence st b1 is extreal-yielding ; ::_thesis: verum
end;
end;
definition
func multextreal -> BinOp of ExtREAL means :Def1: :: MESFUNC7:def 1
for x, y being Element of ExtREAL holds it . (x,y) = x * y;
existence
ex b1 being BinOp of ExtREAL st
for x, y being Element of ExtREAL holds b1 . (x,y) = x * y from BINOP_1:sch_4();
uniqueness
for b1, b2 being BinOp of ExtREAL st ( for x, y being Element of ExtREAL holds b1 . (x,y) = x * y ) & ( for x, y being Element of ExtREAL holds b2 . (x,y) = x * y ) holds
b1 = b2 from BINOP_2:sch_2();
end;
:: deftheorem Def1 defines multextreal MESFUNC7:def_1_:_
for b1 being BinOp of ExtREAL holds
( b1 = multextreal iff for x, y being Element of ExtREAL holds b1 . (x,y) = x * y );
registration
cluster multextreal -> commutative associative ;
coherence
( multextreal is commutative & multextreal is associative )
proof
A1: for a, b, c being Element of ExtREAL holds multextreal . (a,(multextreal . (b,c))) = multextreal . ((multextreal . (a,b)),c)
proof
let a, b, c be Element of ExtREAL ; ::_thesis: multextreal . (a,(multextreal . (b,c))) = multextreal . ((multextreal . (a,b)),c)
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 multextreal . (a,(multextreal . (b,c))) = multextreal . ((multextreal . (a,b)),c) by Def1; ::_thesis: verum
end;
for a, b being Element of ExtREAL holds multextreal . (a,b) = multextreal . (b,a)
proof
let a, b be Element of ExtREAL ; ::_thesis: multextreal . (a,b) = multextreal . (b,a)
multextreal . (a,b) = a * b by Def1;
hence multextreal . (a,b) = multextreal . (b,a) by Def1; ::_thesis: verum
end;
hence ( multextreal is commutative & multextreal is associative ) by A1, BINOP_1:def_2, BINOP_1:def_3; ::_thesis: verum
end;
end;
Lm1: 1. is_a_unity_wrt multextreal
proof
for r being Element of ExtREAL holds multextreal . (r,1.) = r
proof
let r be Element of ExtREAL ; ::_thesis: multextreal . (r,1.) = r
multextreal . (r,1.) = r * 1. by Def1;
hence multextreal . (r,1.) = r by XXREAL_3:81; ::_thesis: verum
end;
then A1: 1. is_a_right_unity_wrt multextreal by BINOP_1:def_6;
for r being Element of ExtREAL holds multextreal . (1.,r) = r
proof
let r be Element of ExtREAL ; ::_thesis: multextreal . (1.,r) = r
multextreal . (1.,r) = 1. * r by Def1;
hence multextreal . (1.,r) = r by XXREAL_3:81; ::_thesis: verum
end;
then 1. is_a_left_unity_wrt multextreal by BINOP_1:def_5;
hence 1. is_a_unity_wrt multextreal by A1, BINOP_1:def_7; ::_thesis: verum
end;
theorem Th5: :: MESFUNC7:5
the_unity_wrt multextreal = 1 by Lm1, BINOP_1:def_8;
registration
cluster multextreal -> having_a_unity ;
coherence
multextreal is having_a_unity by Lm1, Th5, SETWISEO:14;
end;
definition
let F be extreal-yielding FinSequence;
func Product F -> Element of ExtREAL means :Def2: :: MESFUNC7:def 2
ex f being FinSequence of ExtREAL st
( f = F & it = multextreal $$ f );
existence
ex b1 being Element of ExtREAL ex f being FinSequence of ExtREAL st
( f = F & b1 = multextreal $$ f )
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 ; ::_thesis: ex f being FinSequence of ExtREAL st
( f = F & multextreal $$ f = multextreal $$ f )
thus ex f being FinSequence of ExtREAL st
( f = F & multextreal $$ f = multextreal $$ f ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of ExtREAL st ex f being FinSequence of ExtREAL st
( f = F & b1 = multextreal $$ f ) & ex f being FinSequence of ExtREAL st
( f = F & b2 = multextreal $$ f ) holds
b1 = b2 ;
end;
:: deftheorem Def2 defines Product MESFUNC7:def_2_:_
for F being extreal-yielding FinSequence
for b2 being Element of ExtREAL holds
( b2 = Product F iff ex f being FinSequence of ExtREAL st
( f = F & b2 = multextreal $$ f ) );
registration
let x be Element of ExtREAL ;
let n be Nat;
clustern |-> x -> extreal-yielding ;
coherence
n |-> x is extreal-yielding ;
end;
definition
let x be Element of ExtREAL ;
let k be Nat;
funcx |^ k -> set equals :: MESFUNC7:def 3
Product (k |-> x);
coherence
Product (k |-> x) is set ;
end;
:: deftheorem defines |^ MESFUNC7:def_3_:_
for x being Element of ExtREAL
for k being Nat holds x |^ k = Product (k |-> x);
definition
let x be Element of ExtREAL ;
let k be Nat;
:: original: |^
redefine funcx |^ k -> R_eal;
coherence
x |^ k is R_eal ;
end;
registration
cluster <*> ExtREAL -> extreal-yielding ;
coherence
<*> ExtREAL is extreal-yielding ;
end;
registration
let r be Element of ExtREAL ;
cluster<*r*> -> extreal-yielding ;
coherence
<*r*> is extreal-yielding ;
end;
theorem Th6: :: MESFUNC7:6
Product (<*> ExtREAL) = 1
proof
Product (<*> ExtREAL) = multextreal $$ (<*> ExtREAL) by Def2;
hence Product (<*> ExtREAL) = 1 by Th5, FINSOP_1:10; ::_thesis: verum
end;
theorem Th7: :: MESFUNC7:7
for r being Element of ExtREAL holds Product <*r*> = r
proof
let r be Element of ExtREAL ; ::_thesis: Product <*r*> = r
reconsider r9 = r as Element of ExtREAL ;
reconsider F = <*r9*> as FinSequence of ExtREAL ;
multextreal $$ F = r by FINSOP_1:11;
hence Product <*r*> = r by Def2; ::_thesis: verum
end;
registration
let f, g be extreal-yielding FinSequence;
clusterf ^ g -> extreal-yielding ;
coherence
f ^ g is extreal-yielding
proof
A1: rng (f ^ g) = (rng f) \/ (rng g) by FINSEQ_1:31;
A2: rng g c= ExtREAL by VALUED_0:def_2;
rng f c= ExtREAL by VALUED_0:def_2;
then rng (f ^ g) c= ExtREAL by A2, A1, XBOOLE_1:8;
hence f ^ g is extreal-yielding by VALUED_0:def_2; ::_thesis: verum
end;
end;
theorem Th8: :: MESFUNC7:8
for F being extreal-yielding FinSequence
for r being Element of ExtREAL holds Product (F ^ <*r*>) = (Product F) * r
proof
let F be extreal-yielding FinSequence; ::_thesis: for r being Element of ExtREAL holds Product (F ^ <*r*>) = (Product F) * r
let r be Element of ExtREAL ; ::_thesis: Product (F ^ <*r*>) = (Product F) * r
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 Product (F ^ <*r*>) = (Product F) * r by Def1; ::_thesis: verum
end;
theorem Th9: :: MESFUNC7:9
for x being Element of ExtREAL holds x |^ 1 = x
proof
let x be Element of ExtREAL ; ::_thesis: x |^ 1 = x
Product (1 |-> x) = Product <*x*> by FINSEQ_2:59;
hence x |^ 1 = x by Th7; ::_thesis: verum
end;
theorem Th10: :: MESFUNC7:10
for x being Element of ExtREAL
for k being Nat holds x |^ (k + 1) = (x |^ k) * x
proof
let x be Element of ExtREAL ; ::_thesis: for k being Nat holds x |^ (k + 1) = (x |^ k) * x
defpred S1[ Nat] means x |^ ($1 + 1) = (x |^ $1) * x;
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume x |^ (k + 1) = (x |^ k) * x ; ::_thesis: S1[k + 1]
reconsider k1 = k + 1 as Element of NAT ;
Product ((k1 + 1) |-> x) = Product ((k1 |-> x) ^ <*x*>) by FINSEQ_2:60;
hence S1[k + 1] by Th8; ::_thesis: verum
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: S1[ 0 ] by Th6, FINSEQ_2:58;
for k being Nat holds S1[k] from NAT_1:sch_2(A2, A1);
hence for k being Nat holds x |^ (k + 1) = (x |^ k) * x ; ::_thesis: verum
end;
definition
let k be Nat;
let X be non empty set ;
let f be PartFunc of X,ExtREAL;
funcf |^ k -> PartFunc of X,ExtREAL means :Def4: :: MESFUNC7:def 4
( dom it = dom f & ( for x being Element of X st x in dom it holds
it . x = (f . x) |^ k ) );
existence
ex b1 being PartFunc of X,ExtREAL st
( dom b1 = dom f & ( for x being Element of X st x in dom b1 holds
b1 . x = (f . x) |^ k ) )
proof
deffunc H1( set ) -> R_eal = (f . $1) |^ k;
defpred S1[ set ] means $1 in dom f;
consider f3 being PartFunc of X,ExtREAL such that
A1: for d being Element of X holds
( d in dom f3 iff S1[d] ) and
A2: for d being Element of X st d in dom f3 holds
f3 /. d = H1(d) from PARTFUN2:sch_2();
take f3 ; ::_thesis: ( dom f3 = dom f & ( for x being Element of X st x in dom f3 holds
f3 . x = (f . x) |^ k ) )
for x being set st x in dom f holds
x in dom f3 by A1;
then A3: dom f c= dom f3 by TARSKI:def_3;
for x being set st x in dom f3 holds
x in dom f by A1;
then dom f3 c= dom f by TARSKI:def_3;
hence dom f3 = dom f by A3, XBOOLE_0:def_10; ::_thesis: for x being Element of X st x in dom f3 holds
f3 . x = (f . x) |^ k
let d be Element of X; ::_thesis: ( d in dom f3 implies f3 . d = (f . d) |^ k )
assume A4: d in dom f3 ; ::_thesis: f3 . d = (f . d) |^ k
then f3 /. d = (f . d) |^ k by A2;
hence f3 . d = (f . d) |^ k by A4, PARTFUN1:def_6; ::_thesis: verum
end;
uniqueness
for b1, b2 being PartFunc of X,ExtREAL st dom b1 = dom f & ( for x being Element of X st x in dom b1 holds
b1 . x = (f . x) |^ k ) & dom b2 = dom f & ( for x being Element of X st x in dom b2 holds
b2 . x = (f . x) |^ k ) holds
b1 = b2
proof
let f1, f2 be PartFunc of X,ExtREAL; ::_thesis: ( dom f1 = dom f & ( for x being Element of X st x in dom f1 holds
f1 . x = (f . x) |^ k ) & dom f2 = dom f & ( for x being Element of X st x in dom f2 holds
f2 . x = (f . x) |^ k ) implies f1 = f2 )
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 ; ::_thesis: f1 = f2
for d being Element of X st d in dom f holds
f1 . d = f2 . d
proof
let d be Element of X; ::_thesis: ( d in dom f implies f1 . d = f2 . d )
assume A9: d in dom f ; ::_thesis: f1 . d = f2 . d
then f1 . d = (f . d) |^ k by A5, A6;
hence f1 . d = f2 . d by A7, A8, A9; ::_thesis: verum
end;
hence f1 = f2 by A5, A7, PARTFUN1:5; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines |^ MESFUNC7:def_4_:_
for k being Nat
for X being non empty set
for f, b4 being PartFunc of X,ExtREAL holds
( b4 = f |^ k iff ( dom b4 = dom f & ( for x being Element of X st x in dom b4 holds
b4 . x = (f . x) |^ k ) ) );
theorem Th11: :: MESFUNC7:11
for x being Element of ExtREAL
for y being real number
for k being Nat st x = y holds
x |^ k = y |^ k
proof
let x be Element of ExtREAL ; ::_thesis: for y being real number
for k being Nat st x = y holds
x |^ k = y |^ k
let y be real number ; ::_thesis: for k being Nat st x = y holds
x |^ k = y |^ k
let k be Nat; ::_thesis: ( x = y implies x |^ k = y |^ k )
defpred S1[ Nat] means x |^ $1 = y |^ $1;
assume A1: x = y ; ::_thesis: x |^ k = y |^ k
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
reconsider y1 = y as Element of REAL by XREAL_0:def_1;
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; ::_thesis: S1[k + 1]
then (x |^ k) * x = (y1 |^ k) * y1 by A1, EXTREAL1:1;
then (x |^ k) * x = y |^ (k + 1) by NEWTON:6;
hence S1[k + 1] by Th10; ::_thesis: verum
end;
x |^ 0 = 1. by Th6, FINSEQ_2:58;
then A3: S1[ 0 ] by NEWTON:4;
for k being Nat holds S1[k] from NAT_1:sch_2(A3, A2);
hence x |^ k = y |^ k ; ::_thesis: verum
end;
theorem Th12: :: MESFUNC7:12
for x being Element of ExtREAL
for k being Nat st 0 <= x holds
0 <= x |^ k
proof
let x be Element of ExtREAL ; ::_thesis: for k being Nat st 0 <= x holds
0 <= x |^ k
let k be Nat; ::_thesis: ( 0 <= x implies 0 <= x |^ k )
defpred S1[ Nat] means 0 <= x |^ $1;
assume A1: 0 <= x ; ::_thesis: 0 <= x |^ k
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
x |^ (k + 1) = (x |^ k) * x by Th10;
hence S1[k + 1] by A1, A3; ::_thesis: verum
end;
A4: S1[ 0 ] by Th6, FINSEQ_2:58;
for k being Nat holds S1[k] from NAT_1:sch_2(A4, A2);
hence 0 <= x |^ k ; ::_thesis: verum
end;
theorem Th13: :: MESFUNC7:13
for k being Nat st 1 <= k holds
+infty |^ k = +infty
proof
defpred S1[ Nat] means +infty |^ $1 = +infty ;
A1: for k being non empty Nat st S1[k] holds
S1[k + 1]
proof
let k be non empty Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
+infty |^ (k + 1) = (+infty |^ k) * +infty by Th10;
hence S1[k + 1] by A2, XXREAL_3:def_5; ::_thesis: verum
end;
A3: S1[1] by Th9;
for k being non empty Nat holds S1[k] from NAT_1:sch_10(A3, A1);
hence for k being Nat st 1 <= k holds
+infty |^ k = +infty ; ::_thesis: verum
end;
theorem Th14: :: MESFUNC7:14
for k being Nat
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for E being Element of S st E c= dom f & f is_measurable_on E holds
|.f.| |^ k is_measurable_on E
proof
let k be Nat; ::_thesis: for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for E being Element of S st E c= dom f & f is_measurable_on E holds
|.f.| |^ k is_measurable_on E
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for E being Element of S st E c= dom f & f is_measurable_on E holds
|.f.| |^ k is_measurable_on E
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,ExtREAL
for E being Element of S st E c= dom f & f is_measurable_on E holds
|.f.| |^ k is_measurable_on E
let f be PartFunc of X,ExtREAL; ::_thesis: for E being Element of S st E c= dom f & f is_measurable_on E holds
|.f.| |^ k is_measurable_on E
let E be Element of S; ::_thesis: ( E c= dom f & f is_measurable_on E implies |.f.| |^ k is_measurable_on E )
reconsider k1 = k as Element of NAT by ORDINAL1:def_12;
assume that
A1: E c= dom f and
A2: f is_measurable_on E ; ::_thesis: |.f.| |^ k is_measurable_on E
A3: dom (|.f.| |^ k) = dom |.f.| by Def4;
then A4: dom (|.f.| |^ k) = dom f by MESFUNC1:def_10;
percases ( k = 0 or k <> 0 ) ;
supposeA5: k = 0 ; ::_thesis: |.f.| |^ k is_measurable_on E
A6: for r being real number st 1 < r holds
E /\ (less_dom ((|.f.| |^ k),(R_EAL r))) in S
proof
let r be real number ; ::_thesis: ( 1 < r implies E /\ (less_dom ((|.f.| |^ k),(R_EAL r))) in S )
assume A7: 1 < r ; ::_thesis: E /\ (less_dom ((|.f.| |^ k),(R_EAL r))) in S
E c= less_dom ((|.f.| |^ k),(R_EAL r))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in E or x in less_dom ((|.f.| |^ k),(R_EAL r)) )
assume A8: x in E ; ::_thesis: x in less_dom ((|.f.| |^ k),(R_EAL r))
then (|.f.| |^ k) . x = (|.f.| . x) |^ k by A1, A4, Def4;
then (|.f.| |^ k) . x < r by A5, A7, Th6, FINSEQ_2:58;
hence x in less_dom ((|.f.| |^ k),(R_EAL r)) by A1, A4, A8, MESFUNC1:def_11; ::_thesis: verum
end;
then E /\ (less_dom ((|.f.| |^ k),(R_EAL r))) = E by XBOOLE_1:28;
hence E /\ (less_dom ((|.f.| |^ k),(R_EAL r))) in S ; ::_thesis: verum
end;
A9: E c= dom (|.f.| |^ k) by A1, A3, MESFUNC1:def_10;
for r being real number holds E /\ (less_dom ((|.f.| |^ k),(R_EAL r))) in S
proof
let r be real number ; ::_thesis: E /\ (less_dom ((|.f.| |^ k),(R_EAL r))) in S
now__::_thesis:_(_r_<=_1_implies_E_/\_(less_dom_((|.f.|_|^_k),(R_EAL_r)))_in_S_)
assume A10: r <= 1 ; ::_thesis: E /\ (less_dom ((|.f.| |^ k),(R_EAL r))) in S
E c= great_eq_dom ((|.f.| |^ k),(R_EAL r))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in E or x in great_eq_dom ((|.f.| |^ k),(R_EAL r)) )
assume A11: x in E ; ::_thesis: x in great_eq_dom ((|.f.| |^ k),(R_EAL r))
then (|.f.| |^ k) . x = (|.f.| . x) |^ k by A1, A4, Def4;
then r <= (|.f.| |^ k) . x by A5, A10, Th6, FINSEQ_2:58;
hence x in great_eq_dom ((|.f.| |^ k),(R_EAL r)) by A1, A4, A11, MESFUNC1:def_14; ::_thesis: verum
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 A9, MESFUNC1:17;
hence E /\ (less_dom ((|.f.| |^ k),(R_EAL r))) in S ; ::_thesis: verum
end;
hence E /\ (less_dom ((|.f.| |^ k),(R_EAL r))) in S by A6; ::_thesis: verum
end;
hence |.f.| |^ k is_measurable_on E by MESFUNC1:def_16; ::_thesis: verum
end;
supposeA12: k <> 0 ; ::_thesis: |.f.| |^ k is_measurable_on E
then A13: (1 / k) * k = 1 by XCMPLX_1:87;
A14: for r being 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 ; ::_thesis: ( 0 < r implies great_eq_dom ((|.f.| |^ k),(R_EAL r)) = great_eq_dom (|.f.|,(R_EAL (r to_power (1 / k)))) )
assume A15: 0 < r ; ::_thesis: great_eq_dom ((|.f.| |^ k),(R_EAL r)) = great_eq_dom (|.f.|,(R_EAL (r to_power (1 / k))))
A16: 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 ; :: according to TARSKI:def_3 ::_thesis: ( not x in great_eq_dom ((|.f.| |^ k),(R_EAL r)) or x in great_eq_dom (|.f.|,(R_EAL (r to_power (1 / k)))) )
assume A17: x in great_eq_dom ((|.f.| |^ k),(R_EAL r)) ; ::_thesis: x in great_eq_dom (|.f.|,(R_EAL (r to_power (1 / k))))
then A18: x in dom (|.f.| |^ k) by MESFUNC1:def_14;
then A19: |.f.| . x = |.(f . x).| by A3, MESFUNC1:def_10;
then A20: 0 <= |.f.| . x by EXTREAL2:3;
percases ( |.f.| . x = +infty or |.f.| . x <> +infty ) ;
suppose |.f.| . x = +infty ; ::_thesis: x in great_eq_dom (|.f.|,(R_EAL (r to_power (1 / k))))
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 A3, A18, MESFUNC1:def_14; ::_thesis: verum
end;
suppose |.f.| . x <> +infty ; ::_thesis: x in great_eq_dom (|.f.|,(R_EAL (r to_power (1 / k))))
then reconsider fx = |.f.| . x as Element of REAL by A20, XXREAL_0:14;
A21: r <= (|.f.| |^ k) . x by A17, MESFUNC1:def_14;
(|.f.| |^ k) . x = (|.f.| . x) |^ k by A18, Def4;
then A22: r <= fx to_power k1 by A21, Th11;
(fx to_power k) to_power (1 / k) = fx to_power ((k * 1) / k) by A12, A19, EXTREAL2:3, HOLDER_1:2;
then A23: (fx to_power k) to_power (1 / k) = fx by A13, POWER:25;
r is Real by XREAL_0:def_1;
then r to_power (1 / k) <= (fx to_power k) to_power (1 / k) by A12, A15, A22, HOLDER_1:3;
hence x in great_eq_dom (|.f.|,(R_EAL (r to_power (1 / k)))) by A3, A18, A23, MESFUNC1:def_14; ::_thesis: verum
end;
end;
end;
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 ; :: according to TARSKI:def_3 ::_thesis: ( not x in great_eq_dom (|.f.|,(R_EAL (r to_power (1 / k)))) or x in great_eq_dom ((|.f.| |^ k),(R_EAL r)) )
assume A24: x in great_eq_dom (|.f.|,(R_EAL (r to_power (1 / k)))) ; ::_thesis: x in great_eq_dom ((|.f.| |^ k),(R_EAL r))
then A25: x in dom |.f.| by MESFUNC1:def_14;
then A26: (|.f.| |^ k) . x = (|.f.| . x) |^ k by A3, Def4;
|.f.| . x = |.(f . x).| by A25, MESFUNC1:def_10;
then A27: 0 <= |.f.| . x by EXTREAL2:3;
A28: now__::_thesis:_(_|.f.|_._x_<>_+infty_implies_r_<=_(|.f.|_|^_k)_._x_)
assume |.f.| . x <> +infty ; ::_thesis: r <= (|.f.| |^ k) . x
then reconsider fx = |.f.| . x as Element of REAL by A27, XXREAL_0:14;
reconsider R = r to_power (1 / k) as Real by XREAL_0:def_1;
A29: 0 < r to_power (1 / k) by A15, POWER:34;
A30: R to_power k1 = r to_power ((1 / k) * k) by A15, POWER:33;
A31: (|.f.| |^ k) . x = fx |^ k by A26, Th11;
R_EAL (r to_power (1 / k)) <= |.f.| . x by A24, MESFUNC1:def_14;
then r to_power 1 <= fx to_power k by A12, A13, A29, A30, HOLDER_1:3;
hence r <= (|.f.| |^ k) . x by A31, POWER:25; ::_thesis: verum
end;
now__::_thesis:_(_|.f.|_._x_=_+infty_implies_r_<=_(|.f.|_|^_k)_._x_)
assume |.f.| . x = +infty ; ::_thesis: r <= (|.f.| |^ k) . x
then (|.f.| . x) |^ k = +infty by A12, Th13, NAT_1:14;
hence r <= (|.f.| |^ k) . x by A26, XXREAL_0:3; ::_thesis: verum
end;
hence x in great_eq_dom ((|.f.| |^ k),(R_EAL r)) by A3, A25, A28, MESFUNC1:def_14; ::_thesis: verum
end;
hence great_eq_dom ((|.f.| |^ k),(R_EAL r)) = great_eq_dom (|.f.|,(R_EAL (r to_power (1 / k)))) by A16, XBOOLE_0:def_10; ::_thesis: verum
end;
A32: |.f.| is_measurable_on E by A1, A2, MESFUNC2:27;
for r being real number holds E /\ (great_eq_dom ((|.f.| |^ k),(R_EAL r))) in S
proof
let r be real number ; ::_thesis: E /\ (great_eq_dom ((|.f.| |^ k),(R_EAL r))) in S
percases ( r <= 0 or 0 < r ) ;
supposeA33: r <= 0 ; ::_thesis: E /\ (great_eq_dom ((|.f.| |^ k),(R_EAL r))) in S
E c= great_eq_dom ((|.f.| |^ k),(R_EAL r))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in E or x in great_eq_dom ((|.f.| |^ k),(R_EAL r)) )
assume A34: x in E ; ::_thesis: x in great_eq_dom ((|.f.| |^ k),(R_EAL r))
then A35: |.f.| . x = |.(f . x).| by A1, A3, A4, MESFUNC1:def_10;
(|.f.| |^ k) . x = (|.f.| . x) |^ k by A1, A4, A34, Def4;
then r <= (|.f.| |^ k) . x by A33, A35, Th12, EXTREAL2:3;
hence x in great_eq_dom ((|.f.| |^ k),(R_EAL r)) by A1, A4, A34, MESFUNC1:def_14; ::_thesis: verum
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))) in S ; ::_thesis: verum
end;
suppose 0 < r ; ::_thesis: E /\ (great_eq_dom ((|.f.| |^ k),(R_EAL r))) in S
then E /\ (great_eq_dom ((|.f.| |^ k),(R_EAL r))) = E /\ (great_eq_dom (|.f.|,(R_EAL (r to_power (1 / k))))) by A14;
hence E /\ (great_eq_dom ((|.f.| |^ k),(R_EAL r))) in S by A1, A3, A4, A32, MESFUNC1:27; ::_thesis: verum
end;
end;
end;
hence |.f.| |^ k is_measurable_on E by A1, A4, MESFUNC1:27; ::_thesis: verum
end;
end;
end;
theorem Th15: :: MESFUNC7:15
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,ExtREAL
for E being Element of S st (dom f) /\ (dom g) = E & f is V67() & g is V67() & f is_measurable_on E & g is_measurable_on E holds
f (#) g is_measurable_on E
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f, g being PartFunc of X,ExtREAL
for E being Element of S st (dom f) /\ (dom g) = E & f is V67() & g is V67() & f is_measurable_on E & g is_measurable_on E holds
f (#) g is_measurable_on E
let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,ExtREAL
for E being Element of S st (dom f) /\ (dom g) = E & f is V67() & g is V67() & f is_measurable_on E & g is_measurable_on E holds
f (#) g is_measurable_on E
let f, g be PartFunc of X,ExtREAL; ::_thesis: for E being Element of S st (dom f) /\ (dom g) = E & f is V67() & g is V67() & f is_measurable_on E & g is_measurable_on E holds
f (#) g is_measurable_on E
let E be Element of S; ::_thesis: ( (dom f) /\ (dom g) = E & f is V67() & g is V67() & f is_measurable_on E & g is_measurable_on E implies f (#) g is_measurable_on E )
assume that
A1: (dom f) /\ (dom g) = E and
A2: f is V67() and
A3: g is V67() and
A4: f is_measurable_on E and
A5: g is_measurable_on E ; ::_thesis: f (#) g is_measurable_on E
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 being Element of X st x in dom (|.(f + g).| |^ 2) holds
|.((|.(f + g).| |^ 2) . x).| < +infty
proof
let x be Element of X; ::_thesis: ( x in dom (|.(f + g).| |^ 2) implies |.((|.(f + g).| |^ 2) . x).| < +infty )
assume A18: x in dom (|.(f + g).| |^ 2) ; ::_thesis: |.((|.(f + g).| |^ 2) . x).| < +infty
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 Real by A19, EXTREAL2:30;
(f . x) + (g . x) = c1 + c2 by SUPINF_2:1;
then |.((f . x) + (g . x)).| = abs (c1 + c2) by EXTREAL2:1;
then A20: |.((f . x) + (g . x)).| * |.((f . x) + (g . x)).| = (abs (c1 + c2)) * (abs (c1 + c2)) 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 EXTREAL2:8
.= |.(((f . x) + (g . x)) * ((f . x) + (g . x))).|
.= |.((f . x) + (g . x)).| * |.((f . x) + (g . x)).| by EXTREAL2:8 ;
hence |.((|.(f + g).| |^ 2) . x).| < +infty by A20, XXREAL_0:9; ::_thesis: verum
end;
then |.(f + g).| |^ 2 is V67() by MESFUNC2:def_1;
then A23: (1 / 4) (#) (|.(f + g).| |^ 2) is V67() 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 being 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; ::_thesis: ( x in dom (f (#) g) implies (f (#) g) . x = (((1 / 4) (#) (|.(f + g).| |^ 2)) - ((1 / 4) (#) (|.(f - g).| |^ 2))) . x )
assume A25: x in dom (f (#) g) ; ::_thesis: (f (#) g) . x = (((1 / 4) (#) (|.(f + g).| |^ 2)) - ((1 / 4) (#) (|.(f - g).| |^ 2))) . x
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 Real by A26, EXTREAL2:30;
(f . x) + (g . x) = c1 + c2 by SUPINF_2:1;
then |.((f . x) + (g . x)).| = abs (c1 + c2) by EXTREAL2:1;
then A27: |.((f . x) + (g . x)).| * |.((f . x) + (g . x)).| = (abs (c1 + c2)) * (abs (c1 + c2)) by EXTREAL1:1;
((1 / 4) (#) (|.(f + g).| |^ 2)) . x = (R_EAL (1 / 4)) * ((|.(f + g).| |^ 2) . x) by A15, A6, A7, A25, MESFUNC1:def_6;
then ((1 / 4) (#) (|.(f + g).| |^ 2)) . x = (R_EAL (1 / 4)) * ((|.(f + g).| . x) |^ (1 + 1)) by A15, A6, A25, Def4;
then A28: ((1 / 4) (#) (|.(f + g).| |^ 2)) . x = (R_EAL (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 = (R_EAL (1 / 4)) * (|.((f . x) + (g . x)).| * |.((f . x) + (g . x)).|) by A29, A28, Th9;
then A30: ((1 / 4) (#) (|.(f + g).| |^ 2)) . x = (1 / 4) * ((abs (c1 + c2)) * (abs (c1 + c2))) by A27, EXTREAL1:1;
(abs (c1 - c2)) * (abs (c1 - c2)) = (abs (c1 - c2)) ^2 ;
then A31: (abs (c1 - c2)) * (abs (c1 - c2)) = (c1 - c2) ^2 by COMPLEX1:75;
((1 / 4) (#) (|.(f - g).| |^ 2)) . x = (R_EAL (1 / 4)) * ((|.(f - g).| |^ 2) . x) by A10, A6, A12, A25, MESFUNC1:def_6;
then ((1 / 4) (#) (|.(f - g).| |^ 2)) . x = (R_EAL (1 / 4)) * ((|.(f - g).| . x) |^ (1 + 1)) by A10, A6, A25, Def4;
then A32: ((1 / 4) (#) (|.(f - g).| |^ 2)) . x = (R_EAL (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)).| = abs (c1 - c2) by EXTREAL2:1;
then A33: |.((f . x) - (g . x)).| * |.((f . x) - (g . x)).| = (abs (c1 - c2)) * (abs (c1 - c2)) 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 = (R_EAL (1 / 4)) * (|.((f . x) - (g . x)).| * |.((f . x) - (g . x)).|) by A34, A32, Th9;
then A35: ((1 / 4) (#) (|.(f - g).| |^ 2)) . x = (1 / 4) * ((abs (c1 - c2)) * (abs (c1 - c2))) by A33, EXTREAL1:1;
(abs (c1 + c2)) * (abs (c1 + c2)) = (abs (c1 + c2)) ^2 ;
then (abs (c1 + c2)) * (abs (c1 + c2)) = (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 (f (#) g) . x = (((1 / 4) (#) (|.(f + g).| |^ 2)) - ((1 / 4) (#) (|.(f - g).| |^ 2))) . x by A15, A10, A6, A7, A12, A24, A25, MESFUNC1:def_4; ::_thesis: verum
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 being Element of X st x in dom (|.(f - g).| |^ 2) holds
|.((|.(f - g).| |^ 2) . x).| < +infty
proof
let x be Element of X; ::_thesis: ( x in dom (|.(f - g).| |^ 2) implies |.((|.(f - g).| |^ 2) . x).| < +infty )
assume A38: x in dom (|.(f - g).| |^ 2) ; ::_thesis: |.((|.(f - g).| |^ 2) . x).| < +infty
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 Real by A39, EXTREAL2:30;
(f . x) - (g . x) = c1 - c2 by SUPINF_2:3;
then |.((f . x) - (g . x)).| = abs (c1 - c2) by EXTREAL2:1;
then A40: |.((f . x) - (g . x)).| * |.((f . x) - (g . x)).| = (abs (c1 - c2)) * (abs (c1 - c2)) 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 EXTREAL2:8
.= |.(((f . x) - (g . x)) * ((f . x) - (g . x))).|
.= |.((f . x) - (g . x)).| * |.((f . x) - (g . x)).| by EXTREAL2:8 ;
hence |.((|.(f - g).| |^ 2) . x).| < +infty by A40, XXREAL_0:9; ::_thesis: verum
end;
then |.(f - g).| |^ 2 is V67() by MESFUNC2:def_1;
then A42: (1 / 4) (#) (|.(f - g).| |^ 2) is V67() by MESFUNC2:10;
f + g is_measurable_on E by A2, A3, A4, A5, MESFUNC2:7;
then |.(f + g).| |^ 2 is_measurable_on E by A1, A14, A15, Th14;
then A43: (1 / 4) (#) (|.(f + g).| |^ 2) is_measurable_on E by A1, A15, MESFUNC5:49;
f - g is_measurable_on E by A1, A2, A3, A4, A5, MESFUNC2:11, XBOOLE_1:17;
then |.(f - g).| |^ 2 is_measurable_on E by A1, A9, A10, Th14;
then (1 / 4) (#) (|.(f - g).| |^ 2) is_measurable_on E by A1, A10, MESFUNC5:49;
hence f (#) g is_measurable_on E by A1, A10, A12, A23, A42, A36, A43, MESFUNC2:11; ::_thesis: verum
end;
theorem Th16: :: MESFUNC7:16
for X being non empty set
for f being PartFunc of X,ExtREAL st rng f is real-bounded holds
f is V67()
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,ExtREAL st rng f is real-bounded holds
f is V67()
let f be PartFunc of X,ExtREAL; ::_thesis: ( rng f is real-bounded implies f is V67() )
assume A1: rng f is real-bounded ; ::_thesis: f is V67()
then rng f is bounded_above by XXREAL_2:def_11;
then consider UB being real number 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 number such that
A4: LB is LowerBound of rng f by XXREAL_2:def_9;
A5: LB in REAL by XREAL_0:def_1;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_f_holds_
|.(f_._x).|_<_+infty
let x be Element of X; ::_thesis: ( x in dom f implies |.(f . x).| < +infty )
assume x in dom f ; ::_thesis: |.(f . x).| < +infty
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, XXREAL_0: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, XXREAL_0:9;
hence |.(f . x).| < +infty by A7, EXTREAL2:11; ::_thesis: verum
end;
hence f is V67() by MESFUNC2:def_1; ::_thesis: verum
end;
theorem :: MESFUNC7:17
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL
for E being Element of S
for F being non empty Subset of ExtREAL st (dom f) /\ (dom g) = E & rng f = F & g is V67() & f is_measurable_on E & rng f is real-bounded & g is_integrable_on M holds
( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) ) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL
for E being Element of S
for F being non empty Subset of ExtREAL st (dom f) /\ (dom g) = E & rng f = F & g is V67() & f is_measurable_on E & rng f is real-bounded & g is_integrable_on M holds
( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) ) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL
for E being Element of S
for F being non empty Subset of ExtREAL st (dom f) /\ (dom g) = E & rng f = F & g is V67() & f is_measurable_on E & rng f is real-bounded & g is_integrable_on M holds
( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) ) )
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,ExtREAL
for E being Element of S
for F being non empty Subset of ExtREAL st (dom f) /\ (dom g) = E & rng f = F & g is V67() & f is_measurable_on E & rng f is real-bounded & g is_integrable_on M holds
( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) ) )
let f, g be PartFunc of X,ExtREAL; ::_thesis: for E being Element of S
for F being non empty Subset of ExtREAL st (dom f) /\ (dom g) = E & rng f = F & g is V67() & f is_measurable_on E & rng f is real-bounded & g is_integrable_on M holds
( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) ) )
let E be Element of S; ::_thesis: for F being non empty Subset of ExtREAL st (dom f) /\ (dom g) = E & rng f = F & g is V67() & f is_measurable_on E & rng f is real-bounded & g is_integrable_on M holds
( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) ) )
let F be non empty Subset of ExtREAL; ::_thesis: ( (dom f) /\ (dom g) = E & rng f = F & g is V67() & f is_measurable_on E & rng f is real-bounded & g is_integrable_on M implies ( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) ) ) )
assume that
A1: (dom f) /\ (dom g) = E and
A2: rng f = F and
A3: g is V67() and
A4: f is_measurable_on E and
A5: rng f is real-bounded and
A6: g is_integrable_on M ; ::_thesis: ( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) ) )
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 Real by A2, A10, A9, A11, XXREAL_2:57, XXREAL_2:58;
A12: |.(sup F).| = abs l0 by EXTREAL2:1;
|.(inf F).| = abs k0 by EXTREAL2:1;
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 being Element of X st x in dom |.g.| holds
|.(|.g.| . x).| < +infty
proof
let x be Element of X; ::_thesis: ( x in dom |.g.| implies |.(|.g.| . x).| < +infty )
assume A18: x in dom |.g.| ; ::_thesis: |.(|.g.| . x).| < +infty
then |.(|.g.| . x).| = |.|.(g . x).|.| by MESFUNC1:def_10;
then |.(|.g.| . x).| = |.(g . x).| ;
hence |.(|.g.| . x).| < +infty by A3, A17, A18, MESFUNC2:def_1; ::_thesis: verum
end;
then A19: |.g.| is V67() by MESFUNC2:def_1;
A20: f is V67() by A5, Th16;
consider E1 being Element of S such that
A21: E1 = dom g and
A22: g is_measurable_on E1 by A6, MESFUNC5:def_17;
A23: E1 = dom |.g.| by A21, MESFUNC1:def_10;
|.g.| is_measurable_on E1 by A21, A22, MESFUNC2:27;
then A24: |.g.| is_measurable_on E by A1, A21, MESFUNC1:30, XBOOLE_1:17;
(dom f) /\ (dom |.g.|) = E by A1, MESFUNC1:def_10;
then A25: f (#) |.g.| is_measurable_on E by A4, A24, A20, A19, Th15;
A26: |.g.| is_integrable_on M by A6, A21, A22, 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 being 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; ::_thesis: ( x in E implies ( (inf F) * |.(g . x).| <= (f . x) * |.(g . x).| & (f . x) * |.(g . x).| <= (sup F) * |.(g . x).| ) )
A34: 0 <= |.(g . x).| by EXTREAL2:3;
assume A35: x in E ; ::_thesis: ( (inf F) * |.(g . x).| <= (f . x) * |.(g . x).| & (f . x) * |.(g . x).| <= (sup F) * |.(g . x).| )
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 ( (inf F) * |.(g . x).| <= (f . x) * |.(g . x).| & (f . x) * |.(g . x).| <= (sup F) * |.(g . x).| ) by A36, A34, XXREAL_3:71; ::_thesis: verum
end;
for x being 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; ::_thesis: ( x in dom ((k0 (#) |.g.|) | E) implies ((k0 (#) |.g.|) | E) . x <= ((f (#) |.g.|) | E) . x )
assume A37: x in dom ((k0 (#) |.g.|) | E) ; ::_thesis: ((k0 (#) |.g.|) | E) . x <= ((f (#) |.g.|) | E) . x
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 = (R_EAL k0) * (|.g.| . x) by A16, A30, A31, A37, MESFUNC1:def_6;
then (k0 (#) |.g.|) . x = (R_EAL k0) * |.(g . x).| by A16, A31, A37, MESFUNC1:def_10;
then (k0 (#) |.g.|) . x <= (f (#) |.g.|) . x by A33, A31, A37, A39;
hence ((k0 (#) |.g.|) | E) . x <= ((f (#) |.g.|) | E) . x by A29, A7, A31, A37, A38, FUNCT_1:47; ::_thesis: verum
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 being 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; ::_thesis: ( x in dom ((f (#) |.g.|) | E) implies |.(((f (#) |.g.|) | E) . x).| <= |.((f (#) g) | E).| . x )
assume A47: x in dom ((f (#) |.g.|) | E) ; ::_thesis: |.(((f (#) |.g.|) | E) . x).| <= |.((f (#) g) | E).| . x
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 EXTREAL2:8
.= |.(f . x).| * |.(g . x).| ;
then A49: |.((f (#) |.g.|) . x).| = |.((f . x) * (g . x)).| by EXTREAL2:8;
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 |.(((f (#) |.g.|) | E) . x).| <= |.((f (#) g) | E).| . x by A43, A29, A7, A47, A49, A50, A48, MESFUNC1:def_5; ::_thesis: verum
end;
Integral (M,((l0 (#) |.g.|) | E)) = Integral (M,(l0 (#) (|.g.| | E))) by Th2;
then A51: Integral (M,((l0 (#) |.g.|) | E)) = (R_EAL l0) * (Integral (M,(|.g.| | E))) by A27, MESFUNC5:110;
A52: (dom (f (#) g)) /\ E = E by A43;
g is_measurable_on E by A1, A21, A22, MESFUNC1:30, XBOOLE_1:17;
then f (#) g is_measurable_on E by A1, A3, A4, A20, Th15;
then A53: (f (#) g) | E is_measurable_on E by A52, MESFUNC5:42;
A54: for x being Element of X st x in E holds
|.(f . x).| <= |.(inf F).| + |.(sup F).|
proof
0 <= abs k0 by COMPLEX1:46;
then A55: l0 + 0 <= l0 + (abs k0) by XREAL_1:6;
l0 <= abs l0 by COMPLEX1:76;
then l0 + (abs k0) <= (abs l0) + (abs k0) by XREAL_1:6;
then A56: l0 <= (abs l0) + (abs k0) by A55, XXREAL_0:2;
0 <= abs l0 by COMPLEX1:46;
then A57: (- (abs k0)) - (abs l0) <= (- (abs k0)) - 0 by XREAL_1:10;
- (abs k0) <= k0 by COMPLEX1:76;
then A58: (- (abs k0)) - (abs l0) <= k0 by A57, XXREAL_0:2;
let x be Element of X; ::_thesis: ( x in E implies |.(f . x).| <= |.(inf F).| + |.(sup F).| )
A59: abs k0 = |.(inf F).| by EXTREAL2:1;
assume A60: x in E ; ::_thesis: |.(f . x).| <= |.(inf F).| + |.(sup F).|
then f . x in rng f by A13, FUNCT_1:3;
then reconsider fx = f . x as Real by A8;
A61: abs l0 = |.(sup F).| by EXTREAL2:1;
fx <= l0 by A13, A14, A60, FUNCT_1:3, XXREAL_2:def_1;
then A62: fx <= (abs k0) + (abs l0) by A56, XXREAL_0:2;
k0 <= fx by A13, A32, A60, FUNCT_1:3, XXREAL_2:def_2;
then - ((abs k0) + (abs l0)) <= fx by A58, XXREAL_0:2;
then A63: abs fx <= (abs k0) + (abs l0) by A62, ABSVALUE:5;
abs fx = |.(f . x).| by EXTREAL2:1;
hence |.(f . x).| <= |.(inf F).| + |.(sup F).| by A63, A59, A61, SUPINF_2:1; ::_thesis: verum
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 being 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; ::_thesis: ( x in dom ((f (#) g) | E) implies |.(((f (#) g) | E) . x).| <= (((k1 + l1) (#) |.g.|) | E) . x )
assume A67: x in dom ((f (#) g) | E) ; ::_thesis: |.(((f (#) g) | E) . x).| <= (((k1 + l1) (#) |.g.|) | E) . x
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 EXTREAL2:3;
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, EXTREAL2:8;
((k1 + l1) (#) |.g.|) . x = (R_EAL (k1 + l1)) * (|.g.| . x) by A16, A44, A65, A67, MESFUNC1:def_6;
then (((k1 + l1) (#) |.g.|) | E) . x = (R_EAL (k1 + l1)) * |.((g | E) . x).| by A16, A44, A67, A70, A72, MESFUNC1:def_10;
hence |.(((f (#) g) | E) . x).| <= (((k1 + l1) (#) |.g.|) | E) . x by A71, A73, SUPINF_2:1; ::_thesis: verum
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 A44, A53, MESFUNC5:100;
(dom (f (#) |.g.|)) /\ E = E by A29;
then (f (#) |.g.|) | E is_measurable_on E by A25, MESFUNC5:42;
then A76: (f (#) |.g.|) | E is_integrable_on M by A45, A29, A7, A75, A46, MESFUNC5:102;
then A77: -infty < Integral (M,((f (#) |.g.|) | E)) by MESFUNC5:96;
k0 (#) |.g.| is_integrable_on M by A26, MESFUNC5:110;
then (k0 (#) |.g.|) | E is_integrable_on M by MESFUNC5:97;
then consider V1 being 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 being 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; ::_thesis: ( x in dom ((f (#) |.g.|) | E) implies ((f (#) |.g.|) | E) . x <= ((l0 (#) |.g.|) | E) . x )
assume A82: x in dom ((f (#) |.g.|) | E) ; ::_thesis: ((f (#) |.g.|) | E) . x <= ((l0 (#) |.g.|) | E) . x
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 = (R_EAL l0) * (|.g.| . x) by A29, A7, A81, A82, MESFUNC1:def_6;
then (l0 (#) |.g.|) . x = (R_EAL 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 ((f (#) |.g.|) | E) . x <= ((l0 (#) |.g.|) | E) . x by A29, A7, A42, A82, A83, FUNCT_1:47; ::_thesis: verum
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)) = (R_EAL 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 being 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 being Element of REAL st
( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) )
proof
percases ( Integral (M,(|.g.| | E)) <> 0. or Integral (M,(|.g.| | E)) = 0. ) ;
supposeA93: Integral (M,(|.g.| | E)) <> 0. ; ::_thesis: ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) )
reconsider c3 = Integral (M,((f (#) |.g.|) | E)) as 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 Real by A94, XXREAL_0:14;
(Integral (M,((f (#) |.g.|) | E))) / (Integral (M,(|.g.| | E))) = c3 / c1 by EXTREAL1:2;
then reconsider c = (Integral (M,((f (#) |.g.|) | E))) / (Integral (M,(|.g.| | E))) as Element of REAL ;
A96: (Integral (M,(|.g.| | E))) / (Integral (M,(|.g.| | E))) = c1 / c1 by EXTREAL1:2;
(Integral (M,(|.g.| | E))) / (Integral (M,(|.g.| | E))) = c1 / c1 by EXTREAL1:2;
then A97: c3 * (c1 / c1) = (Integral (M,((f (#) |.g.|) | E))) * ((Integral (M,(|.g.| | E))) / (Integral (M,(|.g.| | E)))) by EXTREAL1:1;
(Integral (M,((f (#) |.g.|) | E))) / (Integral (M,(|.g.| | E))) = c3 / c1 by EXTREAL1:2;
then (Integral (M,(|.g.| | E))) * ((Integral (M,((f (#) |.g.|) | E))) / (Integral (M,(|.g.| | E)))) = c1 * (c3 / c1) by EXTREAL1:1;
then A98: (R_EAL c) * (Integral (M,(|.g.| | E))) = Integral (M,((f (#) |.g.|) | E)) by A93, A97, XXREAL_3:88;
A99: Integral (M,(|.g.| | E)) > 0. by A21, A22, A23, A93, MESFUNC2:27, MESFUNC5:92;
(sup F) * (Integral (M,(|.g.| | E))) = l0 * c1 by EXTREAL1:1;
then A100: ((sup F) * (Integral (M,(|.g.| | E)))) / (Integral (M,(|.g.| | E))) = (l0 * c1) / c1 by EXTREAL1:2;
(l0 * c1) / c1 = l0 * (c1 / c1) ;
then A101: ((sup F) * (Integral (M,(|.g.| | E)))) / (Integral (M,(|.g.| | E))) = (sup F) * ((Integral (M,(|.g.| | E))) / (Integral (M,(|.g.| | E)))) by A96, A100, EXTREAL1:1;
(inf F) * (Integral (M,(|.g.| | E))) = k0 * c1 by EXTREAL1:1;
then A102: ((inf F) * (Integral (M,(|.g.| | E)))) / (Integral (M,(|.g.| | E))) = (k0 * c1) / c1 by EXTREAL1:2;
(k0 * c1) / c1 = k0 * (c1 / c1) ;
then A103: ((inf F) * (Integral (M,(|.g.| | E)))) / (Integral (M,(|.g.| | E))) = (inf F) * ((Integral (M,(|.g.| | E))) / (Integral (M,(|.g.| | E)))) by A96, A102, EXTREAL1:1;
(sup F) * ((Integral (M,(|.g.| | E))) / (Integral (M,(|.g.| | E)))) = (sup F) * 1. by A93, A95, A94, XXREAL_3:78;
then (sup F) * ((Integral (M,(|.g.| | E))) / (Integral (M,(|.g.| | E)))) = sup F by XXREAL_3:81;
then A104: c <= sup F by A51, A88, A89, A90, A99, A101, 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, A99, A103, XXREAL_3:79;
hence ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) ) by A104, A98; ::_thesis: verum
end;
supposeA105: Integral (M,(|.g.| | E)) = 0. ; ::_thesis: ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) )
then 0. <= Integral (M,((f (#) |.g.|) | E)) by A29, A7, A31, A86, A78, A79, A80, RELAT_1:68;
then A106: Integral (M,((f (#) |.g.|) | E)) = 0. by A29, A7, A42, A51, A87, A88, A89, A105, RELAT_1:68;
consider y being set such that
A107: y in F by XBOOLE_0:def_1;
reconsider y = y as Element of ExtREAL by A107;
A108: y <= sup F by A107, XXREAL_2:4;
inf F <= y by A107, XXREAL_2:3;
then A109: k0 <= sup F by A108, XXREAL_0:2;
(R_EAL k0) * (Integral (M,(|.g.| | E))) = 0. by A105;
hence ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) ) by A109, A106; ::_thesis: verum
end;
end;
end;
hence ( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) ) ) by A44, A64, A74, A53, A66, MESFUNC5:102; ::_thesis: verum
end;
begin
theorem Th18: :: MESFUNC7:18
for X being non empty set
for f being PartFunc of X,ExtREAL
for A being set holds |.f.| | A = |.(f | A).|
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,ExtREAL
for A being set holds |.f.| | A = |.(f | A).|
let f be PartFunc of X,ExtREAL; ::_thesis: for A being set holds |.f.| | A = |.(f | A).|
let A be set ; ::_thesis: |.f.| | A = |.(f | A).|
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__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(|.f.|_|_A)_holds_
(|.f.|_|_A)_._x_=_|.(f_|_A).|_._x
let x be Element of X; ::_thesis: ( x in dom (|.f.| | A) implies (|.f.| | A) . x = |.(f | A).| . x )
assume A4: x in dom (|.f.| | A) ; ::_thesis: (|.f.| | A) . x = |.(f | A).| . x
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; ::_thesis: verum
end;
hence |.f.| | A = |.(f | A).| by A1, A3, PARTFUN1:5; ::_thesis: verum
end;
theorem Th19: :: MESFUNC7:19
for X being non empty set
for f, g being PartFunc of X,ExtREAL holds
( dom (|.f.| + |.g.|) = (dom f) /\ (dom g) & dom |.(f + g).| c= dom |.f.| )
proof
let X be non empty set ; ::_thesis: for f, g being PartFunc of X,ExtREAL holds
( dom (|.f.| + |.g.|) = (dom f) /\ (dom g) & dom |.(f + g).| c= dom |.f.| )
let f, g be PartFunc of X,ExtREAL; ::_thesis: ( dom (|.f.| + |.g.|) = (dom f) /\ (dom g) & dom |.(f + g).| c= dom |.f.| )
set F = |.f.|;
set G = |.g.|;
|.f.| is V120() by MESFUNC5:12;
then not -infty in rng |.f.| by MESFUNC5:def_3;
then A1: |.f.| " {-infty} = {} by FUNCT_1:72;
|.g.| is V120() by MESFUNC5:12;
then not -infty in rng |.g.| by MESFUNC5:def_3;
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; ::_thesis: dom |.(f + g).| c= dom |.f.|
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; ::_thesis: verum
end;
theorem Th20: :: MESFUNC7:20
for X being non empty set
for f, g being PartFunc of X,ExtREAL holds (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|)
proof
let X be non empty set ; ::_thesis: for f, g being PartFunc of X,ExtREAL holds (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|)
let f, g be PartFunc of X,ExtREAL; ::_thesis: (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|)
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__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((|.f.|_+_|.g.|)_|_(dom_|.(f_+_g).|))_holds_
((|.f.|_+_|.g.|)_|_(dom_|.(f_+_g).|))_._x_=_((|.f.|_|_(dom_|.(f_+_g).|))_+_(|.g.|_|_(dom_|.(f_+_g).|)))_._x
let x be Element of X; ::_thesis: ( x in dom ((|.f.| + |.g.|) | (dom |.(f + g).|)) implies ((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x )
assume A14: x in dom ((|.f.| + |.g.|) | (dom |.(f + g).|)) ; ::_thesis: ((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x
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; ::_thesis: verum
end;
hence (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|) by A12, A8, PARTFUN1:5, RELAT_1:62; ::_thesis: verum
end;
theorem Th21: :: MESFUNC7:21
for X being non empty set
for f, g being PartFunc of X,ExtREAL
for x being set st x in dom |.(f + g).| holds
|.(f + g).| . x <= (|.f.| + |.g.|) . x
proof
let X be non empty set ; ::_thesis: for f, g being PartFunc of X,ExtREAL
for x being set st x in dom |.(f + g).| holds
|.(f + g).| . x <= (|.f.| + |.g.|) . x
let f, g be PartFunc of X,ExtREAL; ::_thesis: for x being set st x in dom |.(f + g).| holds
|.(f + g).| . x <= (|.f.| + |.g.|) . x
let x be set ; ::_thesis: ( x in dom |.(f + g).| implies |.(f + g).| . x <= (|.f.| + |.g.|) . x )
A1: |.((f . x) + (g . x)).| <= |.(f . x).| + |.(g . x).| by EXTREAL2:13;
assume A2: x in dom |.(f + g).| ; ::_thesis: |.(f + g).| . x <= (|.f.| + |.g.|) . x
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 |.(f + g).| . x <= (|.f.| + |.g.|) . x by A2, A3, MESFUNC1:def_10; ::_thesis: verum
end;
theorem :: MESFUNC7:22
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) )
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) )
let f, g be PartFunc of X,ExtREAL; ::_thesis: ( f is_integrable_on M & g is_integrable_on M implies ex E being Element of S st
( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) ) )
assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M ; ::_thesis: ex E being Element of S st
( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) )
ex A being Element of S st
( A = dom g & g is_measurable_on A ) by A2, MESFUNC5:def_17;
then A3: |.g.| is_integrable_on M by A2, MESFUNC5:100;
A4: f + g is_integrable_on M by A1, A2, MESFUNC5:108;
then ex A being 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:100;
for x being 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 ;
ex A being Element of S st
( A = dom f & f is_measurable_on A ) by A1, MESFUNC5:def_17;
then A8: |.f.| is_integrable_on M by A1, MESFUNC5:100;
then |.f.| + |.g.| is_integrable_on M by A3, MESFUNC5:108;
then consider E being 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 being 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 ; ::_thesis: ( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | 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, XBOOLE_1: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, XBOOLE_1:36;
then A18: (|.g.| | E) | E1 = |.g.| | E by FUNCT_1:51;
(|.f.| | E) | E1 = |.f.| | E by A17, FUNCT_1:51;
hence ( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) ) by A10, A13, A16, A18, Th20, MESFUNC1:def_10; ::_thesis: verum
end;
theorem Th23: :: MESFUNC7:23
for X being non empty set
for A being set holds max+ (chi (A,X)) = chi (A,X)
proof
let X be non empty set ; ::_thesis: for A being set holds max+ (chi (A,X)) = chi (A,X)
let A be set ; ::_thesis: max+ (chi (A,X)) = chi (A,X)
A1: dom (max+ (chi (A,X))) = dom (chi (A,X)) by MESFUNC2:def_2;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(max+_(chi_(A,X)))_holds_
(max+_(chi_(A,X)))_._x_=_(chi_(A,X))_._x
let x be Element of X; ::_thesis: ( x in dom (max+ (chi (A,X))) implies (max+ (chi (A,X))) . x = (chi (A,X)) . x )
A2: rng (chi (A,X)) c= {0,1} by FUNCT_3:39;
assume A3: x in dom (max+ (chi (A,X))) ; ::_thesis: (max+ (chi (A,X))) . x = (chi (A,X)) . 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; ::_thesis: verum
end;
hence max+ (chi (A,X)) = chi (A,X) by A1, PARTFUN1:5; ::_thesis: verum
end;
theorem Th24: :: MESFUNC7:24
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S st M . E < +infty holds
( chi (E,X) is_integrable_on M & Integral (M,(chi (E,X))) = M . E & Integral (M,((chi (E,X)) | E)) = M . E )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S st M . E < +infty holds
( chi (E,X) is_integrable_on M & Integral (M,(chi (E,X))) = M . E & Integral (M,((chi (E,X)) | E)) = M . E )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for E being Element of S st M . E < +infty holds
( chi (E,X) is_integrable_on M & Integral (M,(chi (E,X))) = M . E & Integral (M,((chi (E,X)) | E)) = M . E )
let M be sigma_Measure of S; ::_thesis: for E being Element of S st M . E < +infty holds
( chi (E,X) is_integrable_on M & Integral (M,(chi (E,X))) = M . E & Integral (M,((chi (E,X)) | E)) = M . E )
let E be Element of S; ::_thesis: ( 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 ) )
reconsider XX = X as Element of S by MEASURE1:7;
set F = XX \ E;
A1: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(max-_(chi_(E,X)))_holds_
(max-_(chi_(E,X)))_._x_=_0
let x be Element of X; ::_thesis: ( x in dom (max- (chi (E,X))) implies (max- (chi (E,X))) . x = 0 )
A2: now__::_thesis:_(_x_in_E_implies_max_((-_((chi_(E,X))_._x)),0.)_=_0._)
assume x in E ; ::_thesis: max ((- ((chi (E,X)) . x)),0.) = 0.
then (chi (E,X)) . x = 1 by FUNCT_3:def_3;
hence max ((- ((chi (E,X)) . x)),0.) = 0. by XXREAL_0:def_10; ::_thesis: verum
end;
A3: now__::_thesis:_(_not_x_in_E_implies_max_((-_((chi_(E,X))_._x)),0.)_=_0._)
assume not x in E ; ::_thesis: max ((- ((chi (E,X)) . x)),0.) = 0.
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. ; ::_thesis: verum
end;
assume x in dom (max- (chi (E,X))) ; ::_thesis: (max- (chi (E,X))) . x = 0
hence (max- (chi (E,X))) . x = 0 by A2, A3, MESFUNC2:def_3; ::_thesis: verum
end;
A4: XX = dom (chi (E,X)) by FUNCT_3:def_3;
then A5: XX = dom (max+ (chi (E,X))) by Th23;
A6: XX /\ (XX \ E) = XX \ E by XBOOLE_1:28;
then A7: dom ((max+ (chi (E,X))) | (XX \ E)) = XX \ E by A5, RELAT_1:61;
A8: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((max+_(chi_(E,X)))_|_(XX_\_E))_holds_
((max+_(chi_(E,X)))_|_(XX_\_E))_._x_=_0
let x be Element of X; ::_thesis: ( x in dom ((max+ (chi (E,X))) | (XX \ E)) implies ((max+ (chi (E,X))) | (XX \ E)) . x = 0 )
assume A9: x in dom ((max+ (chi (E,X))) | (XX \ E)) ; ::_thesis: ((max+ (chi (E,X))) | (XX \ E)) . x = 0
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))) | (XX \ E)) . x = 0 by A9, FUNCT_1:47; ::_thesis: verum
end;
A10: chi (E,X) is_measurable_on XX by MESFUNC2:29;
then A11: max+ (chi (E,X)) is_measurable_on XX by Th23;
then max+ (chi (E,X)) is_measurable_on XX \ E by MESFUNC1:30;
then A12: integral+ (M,((max+ (chi (E,X))) | (XX \ E))) = 0 by A5, A6, A7, A8, MESFUNC5:42, MESFUNC5: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 \/ (XX \ E) = XX by A14, XBOOLE_1:51;
then A16: (max+ (chi (E,X))) | (E \/ (XX \ E)) = max+ (chi (E,X)) by A5, RELAT_1:69;
A17: for x being set 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 \/ (XX \ E)))) = (integral+ (M,((max+ (chi (E,X))) | E))) + (integral+ (M,((max+ (chi (E,X))) | (XX \ E)))) 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__::_thesis:_for_x_being_set_st_x_in_dom_((max+_(chi_(E,X)))_|_E)_holds_
((max+_(chi_(E,X)))_|_E)_._x_=_1
let x be set ; ::_thesis: ( x in dom ((max+ (chi (E,X))) | E) implies ((max+ (chi (E,X))) | E) . x = 1 )
assume A21: x in dom ((max+ (chi (E,X))) | E) ; ::_thesis: ((max+ (chi (E,X))) | E) . x = 1
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 = 1 by A21, FUNCT_1:47; ::_thesis: verum
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, MESFUNC5:77;
then A22: integral+ (M,(max+ (chi (E,X)))) = (R_EAL 1) * (M . (dom ((max+ (chi (E,X))) | E))) by A15, A20, MESFUNC5:104;
max+ (chi (E,X)) is_measurable_on E by A11, MESFUNC1:30;
then (max+ (chi (E,X))) | E is_measurable_on E by A5, A14, MESFUNC5:42;
then A23: (chi (E,X)) | E is_measurable_on E by Th23;
(max+ (chi (E,X))) | E is nonnegative by A17, MESFUNC5:15, SUPINF_2:52;
then A24: (chi (E,X)) | E is nonnegative by Th23;
E = dom ((chi (E,X)) | E) by A15, Th23;
then A25: Integral (M,((chi (E,X)) | E)) = integral+ (M,((chi (E,X)) | E)) by A23, A24, MESFUNC5:88;
assume M . E < +infty ; ::_thesis: ( chi (E,X) is_integrable_on M & Integral (M,(chi (E,X))) = M . E & Integral (M,((chi (E,X)) | E)) = M . E )
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, MESFUNC5:def_17; ::_thesis: ( Integral (M,(chi (E,X))) = M . E & Integral (M,((chi (E,X)) | E)) = M . E )
Integral (M,(chi (E,X))) = (R_EAL 1) * (M . E) by A15, A22, A13, XXREAL_3:15;
hence Integral (M,(chi (E,X))) = M . E by XXREAL_3:81; ::_thesis: Integral (M,((chi (E,X)) | E)) = M . E
(chi (E,X)) | E = (max+ (chi (E,X))) | E by Th23;
hence Integral (M,((chi (E,X)) | E)) = M . E by A15, A19, A22, A25, XXREAL_3:81; ::_thesis: verum
end;
theorem Th25: :: MESFUNC7:25
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E1, E2 being Element of S st M . (E1 /\ E2) < +infty holds
Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2)
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for E1, E2 being Element of S st M . (E1 /\ E2) < +infty holds
Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2)
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for E1, E2 being Element of S st M . (E1 /\ E2) < +infty holds
Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2)
let M be sigma_Measure of S; ::_thesis: for E1, E2 being Element of S st M . (E1 /\ E2) < +infty holds
Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2)
let E1, E2 be Element of S; ::_thesis: ( M . (E1 /\ E2) < +infty implies Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2) )
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__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((chi_(E1,X))_|_(E1_/\_E2))_holds_
((chi_(E1,X))_|_(E1_/\_E2))_._x_=_((chi_((E1_/\_E2),X))_|_(E1_/\_E2))_._x
let x be Element of X; ::_thesis: ( x in dom ((chi (E1,X)) | (E1 /\ E2)) implies ((chi (E1,X)) | (E1 /\ E2)) . x = ((chi ((E1 /\ E2),X)) | (E1 /\ E2)) . x )
assume A4: x in dom ((chi (E1,X)) | (E1 /\ E2)) ; ::_thesis: ((chi (E1,X)) | (E1 /\ E2)) . x = ((chi ((E1 /\ E2),X)) | (E1 /\ E2)) . x
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; ::_thesis: verum
end;
then A8: (chi (E1,X)) | (E1 /\ E2) = (chi ((E1 /\ E2),X)) | (E1 /\ E2) by A2, A3, PARTFUN1:5;
assume M . (E1 /\ E2) < +infty ; ::_thesis: Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2)
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: E2 \ E1 = dom ((chi (E1,X)) | (E2 \ E1)) by RELAT_1:62;
then E2 \ E1 = (dom (chi (E1,X))) /\ (E2 \ E1) by RELAT_1:61;
then A12: (chi (E1,X)) | (E2 \ E1) is_measurable_on E2 \ E1 by MESFUNC2:29, MESFUNC5:42;
now__::_thesis:_for_x_being_set_st_x_in_dom_(chi_(E1,X))_holds_
0._<=_(chi_(E1,X))_._x
let x be set ; ::_thesis: ( x in dom (chi (E1,X)) implies 0. <= (chi (E1,X)) . x )
assume x in dom (chi (E1,X)) ; ::_thesis: 0. <= (chi (E1,X)) . 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; ::_thesis: verum
end;
then A14: chi (E1,X) is nonnegative by SUPINF_2:52;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((chi_(E1,X))_|_(E2_\_E1))_holds_
0_=_((chi_(E1,X))_|_(E2_\_E1))_._x
let x be Element of X; ::_thesis: ( x in dom ((chi (E1,X)) | (E2 \ E1)) implies 0 = ((chi (E1,X)) | (E2 \ E1)) . x )
assume A15: x in dom ((chi (E1,X)) | (E2 \ E1)) ; ::_thesis: 0 = ((chi (E1,X)) | (E2 \ E1)) . x
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; ::_thesis: verum
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, MESFUNC5:88;
chi (E1,X) is_measurable_on XX by MESFUNC2:29;
then Integral (M,((chi (E1,X)) | E2)) = (Integral (M,((chi (E1,X)) | (E1 /\ E2)))) + (Integral (M,((chi (E1,X)) | (E2 \ E1)))) by A10, A14, A1, MESFUNC5:91, XBOOLE_1:89;
hence Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2) by A9, A16, XXREAL_3:4; ::_thesis: verum
end;
theorem :: MESFUNC7:26
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for E being Element of S
for a, b being real number st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds
( a <= f . x & f . x <= b ) ) holds
( (R_EAL a) * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= (R_EAL b) * (M . E) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for E being Element of S
for a, b being real number st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds
( a <= f . x & f . x <= b ) ) holds
( (R_EAL a) * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= (R_EAL b) * (M . E) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for E being Element of S
for a, b being real number st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds
( a <= f . x & f . x <= b ) ) holds
( (R_EAL a) * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= (R_EAL b) * (M . E) )
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,ExtREAL
for E being Element of S
for a, b being real number st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds
( a <= f . x & f . x <= b ) ) holds
( (R_EAL a) * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= (R_EAL b) * (M . E) )
let f be PartFunc of X,ExtREAL; ::_thesis: for E being Element of S
for a, b being real number st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds
( a <= f . x & f . x <= b ) ) holds
( (R_EAL a) * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= (R_EAL b) * (M . E) )
let E be Element of S; ::_thesis: for a, b being real number st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds
( a <= f . x & f . x <= b ) ) holds
( (R_EAL a) * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= (R_EAL b) * (M . E) )
let a, b be real number ; ::_thesis: ( f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being 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) ) )
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 being Element of X st x in E holds
( a <= f . x & f . x <= b ) ; ::_thesis: ( (R_EAL a) * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= (R_EAL b) * (M . E) )
set C = chi (E,X);
A5: f | E is_integrable_on M by A1, MESFUNC5:97;
for x being Element of X st x in dom (a1 (#) ((chi (E,X)) | E)) holds
(a1 (#) ((chi (E,X)) | E)) . x <= (f | E) . x
proof
let x be Element of X; ::_thesis: ( x in dom (a1 (#) ((chi (E,X)) | E)) implies (a1 (#) ((chi (E,X)) | E)) . x <= (f | E) . x )
assume A6: x in dom (a1 (#) ((chi (E,X)) | E)) ; ::_thesis: (a1 (#) ((chi (E,X)) | E)) . x <= (f | E) . x
then A7: x in dom ((chi (E,X)) | E) by MESFUNC1:def_6;
then x in (dom (chi (E,X))) /\ 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 (#) ((chi (E,X)) | E)) . x = (R_EAL a) * (((chi (E,X)) | E) . x) by A6, MESFUNC1:def_6
.= (R_EAL a) * ((chi (E,X)) . x) by A7, FUNCT_1:47
.= (R_EAL a) * 1. by A8, FUNCT_3:def_3 ;
hence (a1 (#) ((chi (E,X)) | E)) . x <= (f | E) . x by A9, XXREAL_3:81; ::_thesis: verum
end;
then A10: (f | E) - (a1 (#) ((chi (E,X)) | E)) is nonnegative by Th1;
chi (E,X) is_integrable_on M by A3, Th24;
then A11: (chi (E,X)) | E is_integrable_on M by MESFUNC5:97;
then a1 (#) ((chi (E,X)) | E) is_integrable_on M by MESFUNC5:110;
then consider E1 being Element of S such that
A12: E1 = (dom (f | E)) /\ (dom (a1 (#) ((chi (E,X)) | E))) and
A13: Integral (M,((a1 (#) ((chi (E,X)) | 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 (#) ((chi (E,X)) | E)) = dom ((chi (E,X)) | E) by MESFUNC1:def_6;
then dom (a1 (#) ((chi (E,X)) | E)) = (dom (chi (E,X))) /\ E by RELAT_1:61;
then dom (a1 (#) ((chi (E,X)) | E)) = X /\ E by FUNCT_3:def_3;
then A15: dom (a1 (#) ((chi (E,X)) | E)) = E by XBOOLE_1:28;
then A16: (f | E) | E1 = f | E by A12, A14, RELAT_1:69;
dom (b1 (#) ((chi (E,X)) | E)) = dom ((chi (E,X)) | E) by MESFUNC1:def_6;
then dom (b1 (#) ((chi (E,X)) | E)) = (dom (chi (E,X))) /\ E by RELAT_1:61;
then dom (b1 (#) ((chi (E,X)) | E)) = X /\ E by FUNCT_3:def_3;
then A17: dom (b1 (#) ((chi (E,X)) | E)) = E by XBOOLE_1:28;
for x being Element of X st x in dom (f | E) holds
(f | E) . x <= (b1 (#) ((chi (E,X)) | E)) . x
proof
let x be Element of X; ::_thesis: ( x in dom (f | E) implies (f | E) . x <= (b1 (#) ((chi (E,X)) | E)) . x )
assume A18: x in dom (f | E) ; ::_thesis: (f | E) . x <= (b1 (#) ((chi (E,X)) | E)) . x
then A19: x in dom ((chi (E,X)) | E) by A14, A15, MESFUNC1:def_6;
then x in (dom (chi (E,X))) /\ 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 (#) ((chi (E,X)) | E)) . x = (R_EAL b) * (((chi (E,X)) | E) . x) by A14, A17, A18, MESFUNC1:def_6
.= (R_EAL b) * ((chi (E,X)) . x) by A19, FUNCT_1:47
.= (R_EAL b) * 1. by A20, FUNCT_3:def_3 ;
hence (f | E) . x <= (b1 (#) ((chi (E,X)) | E)) . x by A21, XXREAL_3:81; ::_thesis: verum
end;
then A22: (b1 (#) ((chi (E,X)) | E)) - (f | E) is nonnegative by Th1;
b1 (#) ((chi (E,X)) | E) is_integrable_on M by A11, MESFUNC5:110;
then consider E2 being Element of S such that
A23: E2 = (dom (f | E)) /\ (dom (b1 (#) ((chi (E,X)) | E))) and
A24: Integral (M,((f | E) | E2)) <= Integral (M,((b1 (#) ((chi (E,X)) | E)) | E2)) by A5, A22, Th3;
A25: (b1 (#) ((chi (E,X)) | E)) | E2 = b1 (#) ((chi (E,X)) | E) by A14, A17, A23, RELAT_1:69;
E = E /\ E ;
then A26: Integral (M,((chi (E,X)) | E)) = M . E by A3, Th25;
A27: (f | E) | E2 = f | E by A14, A17, A23, RELAT_1:69;
(a1 (#) ((chi (E,X)) | E)) | E1 = a1 (#) ((chi (E,X)) | E) by A12, A14, A15, RELAT_1:69;
hence ( (R_EAL a) * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= (R_EAL b) * (M . E) ) by A11, A13, A24, A25, A16, A27, A26, MESFUNC5:110; ::_thesis: verum
end;