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
B1: 0 <= k and
A2: ( E c= dom f & f is_measurable_on E ) ; :: thesis: f to_power k is_measurable_on E
A3: dom (f to_power k) = dom f by Def7;

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

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

A8: E c= dom (f to_power k) by A2, Def7;

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 A11: 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 A12: 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 A2, A3, Def7;
then r <= (f to_power k) . x by B11, A11, POWER:29;
hence x in great_eq_dom (f to_power k),r1 by A2, A3, A12, 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 A8, MES121;
hence E /\ (less_dom (f to_power k),r) in S ; :: thesis: verum

end;

suppose A6: 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 A7: 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 A2, A3, Def7;
then (f to_power k) . x < r by B11, A6, POWER:29;
hence x in less_dom (f to_power k),r by A2, A3, A7, 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 B12: 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 C1: 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 A2;
then C4: x in dom (f to_power k) by Def7;
0 <= (f to_power k) . x by A1, B12, MESFUNC6:51;
hence x in great_eq_dom (f to_power k),r1 by C1, C4, 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

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 )
assume A17: x in great_eq_dom f,(r1 to_power (1 / k)) ; :: thesis: x in great_eq_dom (f to_power k),r1
then A10: x in dom (f to_power k) by A3, MESFUNC6:6;
A20: ex y being Real st
( y = f . x & r1 to_power (1 / k) <= y ) by A17, MESFUNC6:6;
A24: 0 < r to_power (1 / k) by A15, POWER:39;
set R = r to_power (1 / k);
(r to_power (1 / k)) to_power k = r to_power ((1 / k) * k) by A15, POWER:38;
then (r to_power (1 / k)) to_power k = r to_power 1 by B12, XCMPLX_1:88;
then r1 to_power 1 <= (f . x) to_power k1 by B12, A20, A24, HOLDER_1:3;
then r <= (f . x) to_power k by POWER:30;
then r <= (f to_power k) . x by A10, Def7;
hence x in great_eq_dom (f to_power k),r1 by A10, 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 A26: x in great_eq_dom (f to_power k),r1 ; :: thesis: x in great_eq_dom f,(r1 to_power (1 / k))
then A27: x in dom (f to_power k) by MESFUNC6:6;
A29: 0 <= f . x by A1, MESFUNC6:51;
ex y2 being Real st
( y2 = (f to_power k) . x & r1 <= y2 ) by A26, MESFUNC6:6;
then r <= (f . x) to_power k by A27, Def7;
then A33: r to_power (1 / k1) <= ((f . x) to_power k1) to_power (1 / k1) by A15, B12, HOLDER_1:3;
((f . x) to_power k1) to_power (1 / k1) = (f . x) to_power ((k1 * 1) / k1) by B12, A29, HOLDER_1:2;
then ((f . x) to_power k1) to_power (1 / k1) = (f . x) to_power 1 by B12, XCMPLX_1:88;
then ((f . x) to_power k) to_power (1 / k) = f . x by POWER:30;
hence x in great_eq_dom f,(r1 to_power (1 / k)) by A3, A27, A33, 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:2;
hence E /\ (great_eq_dom (f to_power k),r) in S by A2, MESFUNC6:13; :: thesis: verum

end;

end;

end;

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

end;

end;