let k be real number ; :: thesis: for X being non empty set
for S being SigmaField of X
for E being Element of S
for f being PartFunc of X,REAL st f is nonnegative & 0 <= k & E c= dom f & f is_measurable_on E holds
f to_power k is_measurable_on E
let X be non empty set ; :: thesis: for S being SigmaField of X
for E being Element of S
for f being PartFunc of X,REAL st f is nonnegative & 0 <= k & E c= dom f & f is_measurable_on E holds
f to_power k is_measurable_on E
let S be SigmaField of X; :: thesis: for E being Element of S
for f being PartFunc of X,REAL st f is nonnegative & 0 <= k & E c= dom f & f is_measurable_on E holds
f to_power k is_measurable_on E
let E be Element of S; :: thesis: for f being PartFunc of X,REAL st f is nonnegative & 0 <= k & E c= dom f & f is_measurable_on E holds
f to_power k is_measurable_on E
let f be PartFunc of X,REAL; :: thesis: ( f is nonnegative & 0 <= k & E c= dom f & f is_measurable_on E implies f to_power k is_measurable_on E )
reconsider k1 = k as Real by XREAL_0:def 1;
assume that
A1: f is nonnegative and
A2: 0 <= k and
A3: E c= dom f and
A4: f is_measurable_on E ; :: thesis: f to_power k is_measurable_on E
A5: dom (f to_power k) = dom f by Def6;

per cases ( k = 0 or k > 0 ) by A2;

suppose A6: k = 0 ; :: thesis: f to_power k is_measurable_on E

A7: E c= dom (f to_power k) by A3, Def6;

now

let r be real number ; :: thesis: E /\ (less_dom ((f to_power k),b₁)) in S
reconsider r1 = r as Real by XREAL_0:def 1;

per cases ( r <= 1 or 1 < r ) ;

suppose A8: r <= 1 ; :: thesis: E /\ (less_dom ((f to_power k),b₁)) in S

now

let x be set ; :: thesis: ( x in E implies x in great_eq_dom ((f to_power k),r1) )
assume A9: x in E ; :: thesis: x in great_eq_dom ((f to_power k),r1)
then (f to_power k) . x = (f . x) to_power k by A3, A5, Def6;
then r <= (f to_power k) . x by A6, A8, POWER:24;
hence x in great_eq_dom ((f to_power k),r1) by A3, A5, A9, MESFUNC6:6; :: thesis: verum

end;

then E c= great_eq_dom ((f to_power k),r) by TARSKI:def 3;
then E /\ (great_eq_dom ((f to_power k),r)) = E by XBOOLE_1:28;
then E /\ (less_dom ((f to_power k),r1)) = E \ E by A7, Th28;
hence E /\ (less_dom ((f to_power k),r)) in S ; :: thesis: verum

end;

suppose A10: 1 < r ; :: thesis: E /\ (less_dom ((f to_power k),b₁)) in S

now

let x be set ; :: thesis: ( x in E implies x in less_dom ((f to_power k),r) )
assume A11: x in E ; :: thesis: x in less_dom ((f to_power k),r)
then (f to_power k) . x = (f . x) to_power k by A3, A5, Def6;
then (f to_power k) . x < r by A6, A10, POWER:24;
hence x in less_dom ((f to_power k),r) by A3, A5, A11, MESFUNC6:3; :: thesis: verum

end;

then E c= less_dom ((f to_power k),r) by TARSKI:def 3;
then E /\ (less_dom ((f to_power k),r)) = E by XBOOLE_1:28;
hence E /\ (less_dom ((f to_power k),r)) in S ; :: thesis: verum

end;

end;

end;

hence f to_power k is_measurable_on E by MESFUNC6:12; :: thesis: verum

end;

suppose A12: k > 0 ; :: thesis: f to_power k is_measurable_on E

for r being real number holds E /\ (great_eq_dom ((f to_power k),r)) in S

proof

let r be real number ; :: thesis: E /\ (great_eq_dom ((f to_power k),r)) in S
reconsider r1 = r as Real by XREAL_0:def 1;

per cases ( r1 <= 0 or 0 < r1 ) ;

suppose A13: r1 <= 0 ; :: thesis: E /\ (great_eq_dom ((f to_power k),r)) in S

now

let x be set ; :: thesis: ( x in E implies x in great_eq_dom ((f to_power k),r1) )
assume x in E ; :: thesis: x in great_eq_dom ((f to_power k),r1)
then x in dom f by A3;
then A14: x in dom (f to_power k) by Def6;
0 <= (f to_power k) . x by A1, A12, MESFUNC6:51;
hence x in great_eq_dom ((f to_power k),r1) by A13, A14, MESFUNC6:6; :: thesis: verum

end;

then E c= great_eq_dom ((f to_power k),r) by TARSKI:def 3;
then E /\ (great_eq_dom ((f to_power k),r)) = E by XBOOLE_1:28;
hence E /\ (great_eq_dom ((f to_power k),r)) in S ; :: thesis: verum

end;

suppose A15: 0 < r1 ; :: thesis: E /\ (great_eq_dom ((f to_power k),r)) in S

A16: now

set R = r to_power (1 / k);
let x be set ; :: thesis: ( x in great_eq_dom (f,(r1 to_power (1 / k))) implies x in great_eq_dom ((f to_power k),r1) )
A17: 0 < r to_power (1 / k) by A15, POWER:34;
assume A18: x in great_eq_dom (f,(r1 to_power (1 / k))) ; :: thesis: x in great_eq_dom ((f to_power k),r1)
then A19: x in dom (f to_power k) by A5, MESFUNC6:6;
(r to_power (1 / k)) to_power k = r to_power ((1 / k) * k) by A15, POWER:33;
then A20: (r to_power (1 / k)) to_power k = r to_power 1 by A12, XCMPLX_1:87;
ex y being Real st
( y = f . x & r1 to_power (1 / k) <= y ) by A18, MESFUNC6:6;
then r1 to_power 1 <= (f . x) to_power k1 by A12, A17, A20, HOLDER_1:3;
then r <= (f . x) to_power k by POWER:25;
then r <= (f to_power k) . x by A19, Def6;
hence x in great_eq_dom ((f to_power k),r1) by A19, MESFUNC6:6; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in great_eq_dom ((f to_power k),r1) implies x in great_eq_dom (f,(r1 to_power (1 / k))) )
assume A21: x in great_eq_dom ((f to_power k),r1) ; :: thesis: x in great_eq_dom (f,(r1 to_power (1 / k)))
then A22: x in dom (f to_power k) by MESFUNC6:6;
0 <= f . x by A1, MESFUNC6:51;
then ((f . x) to_power k1) to_power (1 / k1) = (f . x) to_power ((k1 * 1) / k1) by A12, HOLDER_1:2;
then ((f . x) to_power k1) to_power (1 / k1) = (f . x) to_power 1 by A12, XCMPLX_1:87;
then A23: ((f . x) to_power k) to_power (1 / k) = f . x by POWER:25;
ex y2 being Real st
( y2 = (f to_power k) . x & r1 <= y2 ) by A21, MESFUNC6:6;
then r <= (f . x) to_power k by A22, Def6;
then r to_power (1 / k1) <= ((f . x) to_power k1) to_power (1 / k1) by A12, A15, HOLDER_1:3;
hence x in great_eq_dom (f,(r1 to_power (1 / k))) by A5, A22, A23, MESFUNC6:6; :: thesis: verum

end;

then E /\ (great_eq_dom ((f to_power k),r1)) = E /\ (great_eq_dom (f,(r1 to_power (1 / k)))) by A16, TARSKI:1;
hence E /\ (great_eq_dom ((f to_power k),r)) in S by A3, A4, MESFUNC6:13; :: thesis: verum

end;

end;

end;

hence f to_power k is_measurable_on E by A3, A5, MESFUNC6:13; :: thesis: verum

end;

end;