let k be 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 E -measurable holds
|.f.| |^ k is E -measurable
let X be 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 S be 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 f be 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 E be Element of S; ( 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
; |.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
;
|.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;
( 1 < r implies E /\ (less_dom ((|.f.| |^ k),r)) in S )
assume A7:
1
< r
;
E /\ (less_dom ((|.f.| |^ k),r)) in S
E c= less_dom (
(|.f.| |^ k),
r)
proof
let x be
object ;
TARSKI:def 3 ( 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
;
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;
verum
end;
then
E /\ (less_dom ((|.f.| |^ k),r)) = E
by XBOOLE_1:28;
hence
E /\ (less_dom ((|.f.| |^ k),r)) in S
;
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;
E /\ (less_dom ((|.f.| |^ k),r)) in S
now ( r <= 1 implies E /\ (less_dom ((|.f.| |^ k),r)) in S )assume A10:
r <= 1
;
E /\ (less_dom ((|.f.| |^ k),r)) in S
E c= great_eq_dom (
(|.f.| |^ k),
r)
proof
let x be
object ;
TARSKI:def 3 ( 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
;
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;
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
;
verum end;
hence
E /\ (less_dom ((|.f.| |^ k),r)) in S
by A6;
verum
end; hence
|.f.| |^ k is
E -measurable
;
verum end; suppose A12:
k <> 0
;
|.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;
( 0 < r implies great_eq_dom ((|.f.| |^ k),r) = great_eq_dom (|.f.|,(r to_power (1 / k))) )
assume A15:
0 < r
;
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 ;
TARSKI:def 3 ( 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)
;
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
;
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;
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 ;
TARSKI:def 3 ( 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)))
;
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;
hence
x in great_eq_dom (
(|.f.| |^ k),
r)
by A3, A25, A28, MESFUNC1:def 14;
verum
end;
hence
great_eq_dom (
(|.f.| |^ k),
r)
= great_eq_dom (
|.f.|,
(r to_power (1 / k)))
by A16, XBOOLE_0:def 10;
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;
E /\ (great_eq_dom ((|.f.| |^ k),r)) in S
per cases
( r <= 0 or 0 < r )
;
suppose A33:
r <= 0
;
E /\ (great_eq_dom ((|.f.| |^ k),r)) in S
E c= great_eq_dom (
(|.f.| |^ k),
r)
proof
let x be
object ;
TARSKI:def 3 ( 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
;
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;
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
;
verum end; end;
end; hence
|.f.| |^ k is
E -measurable
by A1, A4, MESFUNC1:27;
verum end; end;