let k be Real; :: 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 E -measurable holds
f to_power k is E -measurable

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 E -measurable holds
f to_power k is E -measurable

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 E -measurable holds
f to_power k is E -measurable

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 E -measurable holds
f to_power k is E -measurable

let f be PartFunc of X,REAL; :: thesis: ( f is nonnegative & 0 <= k & E c= dom f & f is E -measurable implies f to_power k is E -measurable )
reconsider k1 = k as Real ;
assume that
A1: f is nonnegative and
A2: 0 <= k and
A3: E c= dom f and
A4: f is E -measurable ; :: thesis: f to_power k is E -measurable
A5: dom (f to_power k) = dom f by Def4;
per cases ( k = 0 or k > 0 ) by A2;
suppose A6: k = 0 ; :: thesis: f to_power k is E -measurable
A7: E c= dom (f to_power k) by ;
now :: thesis: for r being Real holds E /\ (less_dom ((f to_power k),r)) in S
let r be Real; :: thesis: E /\ (less_dom ((f to_power k),b1)) in S
reconsider r1 = r as Real ;
per cases ( r <= 1 or 1 < r ) ;
suppose A8: r <= 1 ; :: thesis: E /\ (less_dom ((f to_power k),b1)) in S
now :: thesis: for x being object st x in E holds
x in great_eq_dom ((f to_power k),r1)
let x be object ; :: 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, Def4;
then r <= (f to_power k) . x by ;
hence x in great_eq_dom ((f to_power k),r1) by ; :: 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 ;
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),b1)) in S
now :: thesis: for x being object st x in E holds
x in less_dom ((f to_power k),r)
let x be object ; :: 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, Def4;
then (f to_power k) . x < r by ;
hence x in less_dom ((f to_power k),r) by ; :: 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 E -measurable by MESFUNC6:12; :: thesis: verum
end;
suppose A12: k > 0 ; :: thesis: f to_power k is E -measurable
for r being Real holds E /\ (great_eq_dom ((f to_power k),r)) in S
proof
let r be Real; :: thesis: E /\ (great_eq_dom ((f to_power k),r)) in S
reconsider r1 = r as Real ;
per cases ( r1 <= 0 or 0 < r1 ) ;
suppose A13: r1 <= 0 ; :: thesis: E /\ (great_eq_dom ((f to_power k),r)) in S
now :: thesis: for x being object st x in E holds
x in great_eq_dom ((f to_power k),r1)
let x be object ; :: 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 Def4;
0 <= (f to_power k) . x by ;
hence x in great_eq_dom ((f to_power k),r1) by ; :: 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 :: thesis: for x being object st x in great_eq_dom (f,(r1 to_power (1 / k))) holds
x in great_eq_dom ((f to_power k),r1)
set R = r to_power (jj / k);
let x be object ; :: thesis: ( x in great_eq_dom (f,(r1 to_power (1 / k))) implies x in great_eq_dom ((f to_power k),r1) )
reconsider xx = x as set by TARSKI:1;
A17: 0 < r to_power (jj / k) by ;
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 ;
(r to_power (jj / k)) to_power k = r to_power ((1 / k) * k) by ;
then A20: (r to_power (jj / k)) to_power k = r to_power 1 by ;
ex y being Real st
( y = f . x & r1 to_power (1 / k) <= y ) by ;
then r1 to_power jj <= (f . xx) to_power k1 by ;
then r <= (f . xx) to_power k by POWER:25;
then r <= (f to_power k) . xx by ;
hence x in great_eq_dom ((f to_power k),r1) by ; :: thesis: verum
end;
now :: thesis: for x being object st x in great_eq_dom ((f to_power k),r1) holds
x in great_eq_dom (f,(r1 to_power (1 / k)))
let x be object ; :: thesis: ( x in great_eq_dom ((f to_power k),r1) implies x in great_eq_dom (f,(r1 to_power (1 / k))) )
reconsider xx = x as set by TARSKI:1;
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 . xx by ;
then ((f . xx) to_power k1) to_power (1 / k1) = (f . xx) to_power ((k1 * 1) / k1) by ;
then ((f . xx) to_power k1) to_power (1 / k1) = (f . xx) to_power 1 by ;
then A23: ((f . xx) 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 ;
then r <= (f . xx) to_power k by ;
then r to_power (1 / k1) <= ((f . xx) to_power k1) to_power (1 / k1) by ;
hence x in great_eq_dom (f,(r1 to_power (1 / k))) by ; :: thesis: verum
end;
then E /\ (great_eq_dom ((f to_power k),r1)) = E /\ (great_eq_dom (f,(r1 to_power (1 / k)))) by ;
hence E /\ (great_eq_dom ((f to_power k),r)) in S by ; :: thesis: verum
end;
end;
end;
hence f to_power k is E -measurable by ; :: thesis: verum
end;
end;