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 E -measurable holds
|.f.| |^ k is E -measurable
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 E -measurable holds
|.f.| |^ k is E -measurable
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 E -measurable holds
|.f.| |^ k is E -measurable
let f be PartFunc of X,ExtREAL; :: thesis: for E being Element of S st E c= dom f & f is E -measurable holds
|.f.| |^ k is E -measurable
let E be Element of S; :: thesis: ( E c= dom f & f is E -measurable implies |.f.| |^ k is E -measurable )
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
assume that
A1: E c= dom f and
A2: f is E -measurable ; :: thesis: |.f.| |^ k is E -measurable
A3: dom (|.f.| |^ k) = dom |.f.| by Def4;
then A4: dom (|.f.| |^ k) = dom f by MESFUNC1:def 10;
per cases ( k = 0 or k <> 0 ) ;
suppose A5: k = 0 ; :: thesis: |.f.| |^ k is E -measurable
A6: for r being Real st 1 < r holds
E /\ (less_dom ((|.f.| |^ k),r)) in S
proof
let r be Real; :: thesis: ( 1 < r implies E /\ (less_dom ((|.f.| |^ k),r)) in S )
assume A7: 1 < r ; :: thesis: E /\ (less_dom ((|.f.| |^ k),r)) in S
E c= less_dom ((|.f.| |^ k),r)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in E or x in less_dom ((|.f.| |^ k),r) )
reconsider xx = x as set by TARSKI:1;
assume A8: x in E ; :: thesis: x in less_dom ((|.f.| |^ k),r)
then (|.f.| |^ k) . xx = (|.f.| . xx) |^ k by A1, A4, Def4;
then (|.f.| |^ k) . xx < r by A5, A7, Th6, FINSEQ_2:58;
hence x in less_dom ((|.f.| |^ k),r) by A1, A4, A8, MESFUNC1:def 11; :: thesis: verum
end;
then E /\ (less_dom ((|.f.| |^ k),r)) = E by XBOOLE_1:28;
hence E /\ (less_dom ((|.f.| |^ k),r)) in S ; :: thesis: verum
end;
A9: E c= dom (|.f.| |^ k) by A1, A3, MESFUNC1:def 10;
for r being Real holds E /\ (less_dom ((|.f.| |^ k),r)) in S
proof
let r be Real; :: thesis: E /\ (less_dom ((|.f.| |^ k),r)) in S
now :: thesis: ( r <= 1 implies E /\ (less_dom ((|.f.| |^ k),r)) in S )
assume A10: r <= 1 ; :: thesis: E /\ (less_dom ((|.f.| |^ k),r)) in S
E c= great_eq_dom ((|.f.| |^ k),r)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in E or x in great_eq_dom ((|.f.| |^ k),r) )
reconsider xx = x as set by TARSKI:1;
assume A11: x in E ; :: thesis: x in great_eq_dom ((|.f.| |^ k),r)
then (|.f.| |^ k) . xx = (|.f.| . xx) |^ k by A1, A4, Def4;
then r <= (|.f.| |^ k) . xx by A5, A10, Th6, FINSEQ_2:58;
hence x in great_eq_dom ((|.f.| |^ k),r) by A1, A4, A11, MESFUNC1:def 14; :: thesis: verum
end;
then E /\ (great_eq_dom ((|.f.| |^ k),r)) = E by XBOOLE_1:28;
then E /\ (less_dom ((|.f.| |^ k),r)) = E \ E by A9, MESFUNC1:17;
hence E /\ (less_dom ((|.f.| |^ k),r)) in S ; :: thesis: verum
end;
hence E /\ (less_dom ((|.f.| |^ k),r)) in S by A6; :: thesis: verum
end;
hence |.f.| |^ k is E -measurable ; :: thesis: verum
end;
suppose A12: k <> 0 ; :: thesis: |.f.| |^ k is E -measurable
then A13: (jj / k) * k = 1 by XCMPLX_1:87;
A14: for r being Real st 0 < r holds
great_eq_dom ((|.f.| |^ k),r) = great_eq_dom (|.f.|,(r to_power (1 / k)))
proof
let r be Real; :: thesis: ( 0 < r implies great_eq_dom ((|.f.| |^ k),r) = great_eq_dom (|.f.|,(r to_power (1 / k))) )
assume A15: 0 < r ; :: thesis: great_eq_dom ((|.f.| |^ k),r) = great_eq_dom (|.f.|,(r to_power (1 / k)))
A16: great_eq_dom ((|.f.| |^ k),r) c= great_eq_dom (|.f.|,(r to_power (1 / k)))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in great_eq_dom ((|.f.| |^ k),r) or x in great_eq_dom (|.f.|,(r to_power (1 / k))) )
reconsider xx = x as set by TARSKI:1;
assume A17: x in great_eq_dom ((|.f.| |^ k),r) ; :: thesis: x in great_eq_dom (|.f.|,(r to_power (1 / k)))
then A18: x in dom (|.f.| |^ k) by MESFUNC1:def 14;
then A19: |.f.| . xx = |.(f . xx).| by A3, MESFUNC1:def 10;
then A20: 0 <= |.f.| . xx by EXTREAL1:14;
per cases ( |.f.| . xx = +infty or |.f.| . xx <> +infty ) ;
suppose |.f.| . xx <> +infty ; :: thesis: x in great_eq_dom (|.f.|,(r to_power (1 / k)))
then reconsider fx = |.f.| . xx as Element of REAL by A20, XXREAL_0:14;
A21: r <= (|.f.| |^ k) . xx by A17, MESFUNC1:def 14;
(|.f.| |^ k) . xx = (|.f.| . xx) |^ k by A18, Def4;
then A22: r <= fx to_power k1 by A21, Th11;
(fx to_power k) to_power (jj / k) = fx to_power ((k * jj) / k) by A12, A19, EXTREAL1:14, HOLDER_1:2;
then A23: (fx to_power k) to_power (1 / k) = fx by A13, POWER:25;
r to_power (jj / k) <= (fx to_power k) to_power (jj / k) by A15, A22, HOLDER_1:3;
hence x in great_eq_dom (|.f.|,(r to_power (1 / k))) by A3, A18, A23, MESFUNC1:def 14; :: thesis: verum
end;
end;
end;
great_eq_dom (|.f.|,(r to_power (1 / k))) c= great_eq_dom ((|.f.| |^ k),r)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in great_eq_dom (|.f.|,(r to_power (1 / k))) or x in great_eq_dom ((|.f.| |^ k),r) )
reconsider xx = x as set by TARSKI:1;
assume A24: x in great_eq_dom (|.f.|,(r to_power (1 / k))) ; :: thesis: x in great_eq_dom ((|.f.| |^ k),r)
then A25: x in dom |.f.| by MESFUNC1:def 14;
then A26: (|.f.| |^ k) . xx = (|.f.| . xx) |^ k by A3, Def4;
|.f.| . xx = |.(f . xx).| by A25, MESFUNC1:def 10;
then A27: 0 <= |.f.| . xx by EXTREAL1:14;
A28: now :: thesis: ( |.f.| . xx <> +infty implies r <= (|.f.| |^ k) . xx )
assume |.f.| . xx <> +infty ; :: thesis: r <= (|.f.| |^ k) . xx
then reconsider fx = |.f.| . xx as Element of REAL by A27, XXREAL_0:14;
reconsider R = r to_power (1 / k) as Real ;
A29: 0 < r to_power (1 / k) by A15, POWER:34;
A30: R to_power k1 = r to_power ((jj / k) * k) by A15, POWER:33;
A31: (|.f.| |^ k) . xx = fx |^ k by A26, Th11;
r to_power (1 / k) <= |.f.| . xx by A24, MESFUNC1:def 14;
then r to_power 1 <= fx to_power k by A13, A29, A30, HOLDER_1:3;
hence r <= (|.f.| |^ k) . xx by A31; :: thesis: verum
end;
now :: thesis: ( |.f.| . xx = +infty implies r <= (|.f.| |^ k) . xx )
assume |.f.| . xx = +infty ; :: thesis: r <= (|.f.| |^ k) . xx
then (|.f.| . xx) |^ k = +infty by A12, Th13, NAT_1:14;
hence r <= (|.f.| |^ k) . xx by A26, XXREAL_0:3; :: thesis: verum
end;
hence x in great_eq_dom ((|.f.| |^ k),r) by A3, A25, A28, MESFUNC1:def 14; :: thesis: verum
end;
hence great_eq_dom ((|.f.| |^ k),r) = great_eq_dom (|.f.|,(r to_power (1 / k))) by A16, XBOOLE_0:def 10; :: thesis: verum
end;
A32: |.f.| is E -measurable by A1, A2, MESFUNC2:27;
for r being Real holds E /\ (great_eq_dom ((|.f.| |^ k),r)) in S
proof
let r be Real; :: thesis: E /\ (great_eq_dom ((|.f.| |^ k),r)) in S
per cases ( r <= 0 or 0 < r ) ;
suppose A33: r <= 0 ; :: thesis: E /\ (great_eq_dom ((|.f.| |^ k),r)) in S
E c= great_eq_dom ((|.f.| |^ k),r)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in E or x in great_eq_dom ((|.f.| |^ k),r) )
reconsider xx = x as set by TARSKI:1;
assume A34: x in E ; :: thesis: x in great_eq_dom ((|.f.| |^ k),r)
then A35: |.f.| . xx = |.(f . xx).| by A1, A3, A4, MESFUNC1:def 10;
(|.f.| |^ k) . xx = (|.f.| . xx) |^ k by A1, A4, A34, Def4;
then r <= (|.f.| |^ k) . xx by A33, A35, Th12, EXTREAL1:14;
hence x in great_eq_dom ((|.f.| |^ k),r) by A1, A4, A34, MESFUNC1:def 14; :: thesis: verum
end;
then E /\ (great_eq_dom ((|.f.| |^ k),r)) = E by XBOOLE_1:28;
hence E /\ (great_eq_dom ((|.f.| |^ k),r)) in S ; :: thesis: verum
end;
suppose 0 < r ; :: thesis: E /\ (great_eq_dom ((|.f.| |^ k),r)) in S
then E /\ (great_eq_dom ((|.f.| |^ k),r)) = E /\ (great_eq_dom (|.f.|,(r to_power (1 / k)))) by A14;
hence E /\ (great_eq_dom ((|.f.| |^ k),r)) in S by A1, A3, A4, A32, MESFUNC1:27; :: thesis: verum
end;
end;
end;
hence |.f.| |^ k is E -measurable by A1, A4, MESFUNC1:27; :: thesis: verum
end;
end;