let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for k being positive Real st f in Lp_Functions (M,k) & Integral (M,((abs f) to_power k)) = 0 holds
f a.e.= X --> 0,M
let S be SigmaField of X; for M being sigma_Measure of S
for f being PartFunc of X,REAL
for k being positive Real st f in Lp_Functions (M,k) & Integral (M,((abs f) to_power k)) = 0 holds
f a.e.= X --> 0,M
let M be sigma_Measure of S; for f being PartFunc of X,REAL
for k being positive Real st f in Lp_Functions (M,k) & Integral (M,((abs f) to_power k)) = 0 holds
f a.e.= X --> 0,M
let f be PartFunc of X,REAL; for k being positive Real st f in Lp_Functions (M,k) & Integral (M,((abs f) to_power k)) = 0 holds
f a.e.= X --> 0,M
let k be positive Real; ( f in Lp_Functions (M,k) & Integral (M,((abs f) to_power k)) = 0 implies f a.e.= X --> 0,M )
assume that
A1:
f in Lp_Functions (M,k)
and
A2:
Integral (M,((abs f) to_power k)) = 0
; f a.e.= X --> 0,M
ex h being PartFunc of X,REAL st
( f = h & ex ND being Element of S st
( M . (ND `) = 0 & dom h = ND & h is ND -measurable & (abs h) to_power k is_integrable_on M ) )
by A1;
then consider NDf being Element of S such that
A3:
( M . (NDf `) = 0 & dom f = NDf & f is NDf -measurable & (abs f) to_power k is_integrable_on M )
;
reconsider t = (abs f) to_power k as PartFunc of X,REAL ;
reconsider ND = NDf ` as Element of S by MEASURE1:34;
A4:
dom t = dom (abs f)
by MESFUN6C:def 4;
then A5:
dom t = NDf
by A3, VALUED_1:def 11;
dom t = ND `
by A4, A3, VALUED_1:def 11;
then A6:
t in L1_Functions M
by A3;
abs t = t
by Th14;
then
t a.e.= X --> 0,M
by A2, A6, LPSPACE1:53;
then consider ND1 being Element of S such that
A7:
( M . ND1 = 0 & ((abs f) to_power k) | (ND1 `) = (X --> 0) | (ND1 `) )
;
set ND2 = ND \/ ND1;
( ND is measure_zero of M & ND1 is measure_zero of M )
by A3, A7, MEASURE1:def 7;
then
ND \/ ND1 is measure_zero of M
by MEASURE1:37;
then A8:
M . (ND \/ ND1) = 0
by MEASURE1:def 7;
A9:
( (ND \/ ND1) ` c= ND ` & (ND \/ ND1) ` c= ND1 ` )
by XBOOLE_1:7, XBOOLE_1:34;
dom (X --> 0) = X
by FUNCOP_1:13;
then A10:
dom ((X --> 0) | ((ND \/ ND1) `)) = (ND \/ ND1) `
by RELAT_1:62;
A11:
dom (f | ((ND \/ ND1) `)) = (ND \/ ND1) `
by A3, A9, RELAT_1:62;
for x being object st x in dom (f | ((ND \/ ND1) `)) holds
(f | ((ND \/ ND1) `)) . x = ((X --> 0) | ((ND \/ ND1) `)) . x
proof
let x be
object ;
( x in dom (f | ((ND \/ ND1) `)) implies (f | ((ND \/ ND1) `)) . x = ((X --> 0) | ((ND \/ ND1) `)) . x )
assume A12:
x in dom (f | ((ND \/ ND1) `))
;
(f | ((ND \/ ND1) `)) . x = ((X --> 0) | ((ND \/ ND1) `)) . x
A13:
now not f . x <> 0 assume
f . x <> 0
;
contradictionthen
|.(f . x).| > 0
by COMPLEX1:47;
then
|.(f . x).| to_power k <> 0
by POWER:34;
then
((abs f) . x) to_power k <> 0
by VALUED_1:18;
then A14:
((abs f) to_power k) . x <> 0
by A5, A9, A12, A11, MESFUN6C:def 4;
((X --> 0) | (ND1 `)) . x = (X --> 0) . x
by A9, A12, A11, FUNCT_1:49;
then
((X --> 0) | (ND1 `)) . x = 0
by A12, FUNCOP_1:7;
hence
contradiction
by A14, A7, A9, A12, A11, FUNCT_1:49;
verum end;
((X --> 0) | ((ND \/ ND1) `)) . x = (X --> 0) . x
by A11, A12, FUNCT_1:49;
then
((X --> 0) | ((ND \/ ND1) `)) . x = 0
by A12, FUNCOP_1:7;
hence
(f | ((ND \/ ND1) `)) . x = ((X --> 0) | ((ND \/ ND1) `)) . x
by A11, A12, A13, FUNCT_1:49;
verum
end;
then
f | ((ND \/ ND1) `) = (X --> 0) | ((ND \/ ND1) `)
by A10, A11, FUNCT_1:def 11;
hence
f a.e.= X --> 0,M
by A8; verum