let X be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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

hence f a.e.= X --> 0,M by A8; :: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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

then
f | ((ND \/ ND1) `) = (X --> 0) | ((ND \/ ND1) `)
by A10, A11, FUNCT_1:def 11;
let x be object ; :: thesis: ( x in dom (f | ((ND \/ ND1) `)) implies (f | ((ND \/ ND1) `)) . x = ((X --> 0) | ((ND \/ ND1) `)) . x )

assume A12: x in dom (f | ((ND \/ ND1) `)) ; :: thesis: (f | ((ND \/ ND1) `)) . x = ((X --> 0) | ((ND \/ ND1) `)) . x

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; :: thesis: verum

end;assume A12: x in dom (f | ((ND \/ ND1) `)) ; :: thesis: (f | ((ND \/ ND1) `)) . x = ((X --> 0) | ((ND \/ ND1) `)) . x

A13: now :: thesis: not f . x <> 0

((X --> 0) | ((ND \/ ND1) `)) . x = (X --> 0) . x
by A11, A12, FUNCT_1:49;assume
f . x <> 0
; :: thesis: contradiction

then |.(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; :: thesis: verum

end;then |.(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; :: thesis: verum

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; :: thesis: verum

hence f a.e.= X --> 0,M by A8; :: thesis: verum