let k be natural number ; :: 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_measurable_on E holds
|.f.| |^ k is_measurable_on E
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_measurable_on E holds
|.f.| |^ k is_measurable_on E
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_measurable_on E holds
|.f.| |^ k is_measurable_on E
let f be PartFunc of X,ExtREAL ; :: thesis: for E being Element of S st E c= dom f & f is_measurable_on E holds
|.f.| |^ k is_measurable_on E
let E be Element of S; :: thesis: ( E c= dom f & f is_measurable_on E implies |.f.| |^ k is_measurable_on E )
reconsider k1 = k as Element of NAT by ORDINAL1:def 13;
assume A1:
( E c= dom f & f is_measurable_on E )
; :: thesis: |.f.| |^ k is_measurable_on E
A2:
dom (|.f.| |^ k) = dom |.f.|
by Def5;
then A3:
dom (|.f.| |^ k) = dom f
by MESFUNC1:def 10;
per cases
( k = 0 or k <> 0 )
;
suppose A4:
k = 0
;
:: thesis: |.f.| |^ k is_measurable_on EA5:
for
r being
real number st 1
< r holds
E /\ (less_dom (|.f.| |^ k),(R_EAL r)) in S
proof
let r be
real number ;
:: thesis: ( 1 < r implies E /\ (less_dom (|.f.| |^ k),(R_EAL r)) in S )
assume A6:
1
< r
;
:: thesis: E /\ (less_dom (|.f.| |^ k),(R_EAL r)) in S
E c= less_dom (|.f.| |^ k),
(R_EAL r)
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in E or x in less_dom (|.f.| |^ k),(R_EAL r) )
assume A7:
x in E
;
:: thesis: x in less_dom (|.f.| |^ k),(R_EAL r)
then
(|.f.| |^ k) . x = (|.f.| . x) |^ k
by A1, A3, Def5;
then
(|.f.| |^ k) . x < r
by A4, A6, Th6, FINSEQ_2:72;
hence
x in less_dom (|.f.| |^ k),
(R_EAL r)
by A1, A3, A7, MESFUNC1:def 12;
:: thesis: verum
end;
then
E /\ (less_dom (|.f.| |^ k),(R_EAL r)) = E
by XBOOLE_1:28;
hence
E /\ (less_dom (|.f.| |^ k),(R_EAL r)) in S
;
:: thesis: verum
end; A8:
E c= dom (|.f.| |^ k)
by A1, A2, MESFUNC1:def 10;
for
r being
real number holds
E /\ (less_dom (|.f.| |^ k),(R_EAL r)) in S
proof
let r be
real number ;
:: thesis: E /\ (less_dom (|.f.| |^ k),(R_EAL r)) in S
now assume A9:
r <= 1
;
:: thesis: E /\ (less_dom (|.f.| |^ k),(R_EAL r)) in S
E c= great_eq_dom (|.f.| |^ k),
(R_EAL r)
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in E or x in great_eq_dom (|.f.| |^ k),(R_EAL r) )
assume A10:
x in E
;
:: thesis: x in great_eq_dom (|.f.| |^ k),(R_EAL r)
then
(|.f.| |^ k) . x = (|.f.| . x) |^ k
by A1, A3, Def5;
then
r <= (|.f.| |^ k) . x
by A4, A9, Th6, FINSEQ_2:72;
hence
x in great_eq_dom (|.f.| |^ k),
(R_EAL r)
by A1, A3, A10, MESFUNC1:def 15;
:: thesis: verum
end; then
E /\ (great_eq_dom (|.f.| |^ k),(R_EAL r)) = E
by XBOOLE_1:28;
then
E /\ (less_dom (|.f.| |^ k),(R_EAL r)) = E \ E
by A8, MESFUNC1:21;
hence
E /\ (less_dom (|.f.| |^ k),(R_EAL r)) in S
;
:: thesis: verum end;
hence
E /\ (less_dom (|.f.| |^ k),(R_EAL r)) in S
by A5;
:: thesis: verum
end; hence
|.f.| |^ k is_measurable_on E
by MESFUNC1:def 17;
:: thesis: verum end; suppose A11:
k <> 0
;
:: thesis: |.f.| |^ k is_measurable_on Ethen A12:
1
<= k
by NAT_1:14;
A13:
(1 / k) * k = 1
by A11, XCMPLX_1:88;
A14:
for
r being
real number st
0 < r holds
great_eq_dom (|.f.| |^ k),
(R_EAL r) = great_eq_dom |.f.|,
(R_EAL (r to_power (1 / k)))
proof
let r be
real number ;
:: thesis: ( 0 < r implies great_eq_dom (|.f.| |^ k),(R_EAL r) = great_eq_dom |.f.|,(R_EAL (r to_power (1 / k))) )
assume A15:
0 < r
;
:: thesis: great_eq_dom (|.f.| |^ k),(R_EAL r) = great_eq_dom |.f.|,(R_EAL (r to_power (1 / k)))
A16:
great_eq_dom |.f.|,
(R_EAL (r to_power (1 / k))) c= great_eq_dom (|.f.| |^ k),
(R_EAL r)
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in great_eq_dom |.f.|,(R_EAL (r to_power (1 / k))) or x in great_eq_dom (|.f.| |^ k),(R_EAL r) )
assume A17:
x in great_eq_dom |.f.|,
(R_EAL (r to_power (1 / k)))
;
:: thesis: x in great_eq_dom (|.f.| |^ k),(R_EAL r)
then A18:
x in dom |.f.|
by MESFUNC1:def 15;
then
|.f.| . x = |.(f . x).|
by MESFUNC1:def 10;
then A19:
0 <= |.f.| . x
by EXTREAL2:51;
A20:
(|.f.| |^ k) . x = (|.f.| . x) |^ k
by A2, A18, Def5;
now assume
|.f.| . x <> +infty
;
:: thesis: r <= (|.f.| |^ k) . xthen reconsider fx =
|.f.| . x as
Element of
REAL by A19, XXREAL_0:14;
A22:
(|.f.| |^ k) . x = fx |^ k
by A20, Th11;
A23:
R_EAL (r to_power (1 / k)) <= |.f.| . x
by A17, MESFUNC1:def 15;
A24:
0 < r to_power (1 / k)
by A15, POWER:39;
reconsider R =
r to_power (1 / k) as
Real by XREAL_0:def 1;
R to_power k1 = r to_power ((1 / k) * k)
by A15, POWER:38;
then A25:
r to_power 1
<= fx to_power k
by A12, A13, A23, A24, HOLDER_1:3;
thus
r <= (|.f.| |^ k) . x
by A22, A25, POWER:30;
:: thesis: verum end;
hence
x in great_eq_dom (|.f.| |^ k),
(R_EAL r)
by A2, A18, A21, MESFUNC1:def 15;
:: thesis: verum
end;
great_eq_dom (|.f.| |^ k),
(R_EAL r) c= great_eq_dom |.f.|,
(R_EAL (r to_power (1 / k)))
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in great_eq_dom (|.f.| |^ k),(R_EAL r) or x in great_eq_dom |.f.|,(R_EAL (r to_power (1 / k))) )
assume A26:
x in great_eq_dom (|.f.| |^ k),
(R_EAL r)
;
:: thesis: x in great_eq_dom |.f.|,(R_EAL (r to_power (1 / k)))
then A27:
x in dom (|.f.| |^ k)
by MESFUNC1:def 15;
then A28:
|.f.| . x = |.(f . x).|
by A2, MESFUNC1:def 10;
then A29:
0 <= |.f.| . x
by EXTREAL2:51;
per cases
( |.f.| . x = +infty or |.f.| . x <> +infty )
;
suppose
|.f.| . x <> +infty
;
:: thesis: x in great_eq_dom |.f.|,(R_EAL (r to_power (1 / k)))then reconsider fx =
|.f.| . x as
Element of
REAL by A29, XXREAL_0:14;
A30:
0 < 1
/ k
by A12;
A31:
r <= (|.f.| |^ k) . x
by A26, MESFUNC1:def 15;
(|.f.| |^ k) . x = (|.f.| . x) |^ k
by A27, Def5;
then
(|.f.| |^ k) . x = fx |^ k
by Th11;
then A32:
r <= fx to_power k1
by A31;
r is
Real
by XREAL_0:def 1;
then A33:
r to_power (1 / k) <= (fx to_power k) to_power (1 / k)
by A15, A30, A32, HOLDER_1:3;
0 < k
by A11;
then
(fx to_power k) to_power (1 / k) = fx to_power ((k * 1) / k)
by A28, EXTREAL2:51, HOLDER_1:2;
then
(fx to_power k) to_power (1 / k) = fx
by A13, POWER:30;
hence
x in great_eq_dom |.f.|,
(R_EAL (r to_power (1 / k)))
by A2, A27, A33, MESFUNC1:def 15;
:: thesis: verum end;
end;
hence
great_eq_dom (|.f.| |^ k),
(R_EAL r) = great_eq_dom |.f.|,
(R_EAL (r to_power (1 / k)))
by A16, XBOOLE_0:def 10;
:: thesis: verum
end; A34:
|.f.| is_measurable_on E
by A1, MESFUNC2:29;
for
r being
real number holds
E /\ (great_eq_dom (|.f.| |^ k),(R_EAL r)) in S
proof
let r be
real number ;
:: thesis: E /\ (great_eq_dom (|.f.| |^ k),(R_EAL r)) in S
per cases
( r <= 0 or 0 < r )
;
suppose A35:
r <= 0
;
:: thesis: E /\ (great_eq_dom (|.f.| |^ k),(R_EAL r)) in S
E c= great_eq_dom (|.f.| |^ k),
(R_EAL r)
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in E or x in great_eq_dom (|.f.| |^ k),(R_EAL r) )
assume A36:
x in E
;
:: thesis: x in great_eq_dom (|.f.| |^ k),(R_EAL r)
then A37:
(|.f.| |^ k) . x = (|.f.| . x) |^ k
by A1, A3, Def5;
|.f.| . x = |.(f . x).|
by A1, A2, A3, A36, MESFUNC1:def 10;
then
r <= (|.f.| |^ k) . x
by A35, A37, Th12, EXTREAL2:51;
hence
x in great_eq_dom (|.f.| |^ k),
(R_EAL r)
by A1, A3, A36, MESFUNC1:def 15;
:: thesis: verum
end; then
E /\ (great_eq_dom (|.f.| |^ k),(R_EAL r)) = E
by XBOOLE_1:28;
hence
E /\ (great_eq_dom (|.f.| |^ k),(R_EAL r)) in S
;
:: thesis: verum end;
end; hence
|.f.| |^ k is_measurable_on E
by A1, A3, MESFUNC1:31;
:: thesis: verum end;