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 st ex E being Element of S st

( M . (E `) = 0 & E = dom f & f is E -measurable ) holds

a.e-eq-class_Lp (f,M,1) c= a.e-eq-class (f,M)

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,REAL st ex E being Element of S st

( M . (E `) = 0 & E = dom f & f is E -measurable ) holds

a.e-eq-class_Lp (f,M,1) c= a.e-eq-class (f,M)

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,REAL st ex E being Element of S st

( M . (E `) = 0 & E = dom f & f is E -measurable ) holds

a.e-eq-class_Lp (f,M,1) c= a.e-eq-class (f,M)

let f be PartFunc of X,REAL; :: thesis: ( ex E being Element of S st

( M . (E `) = 0 & E = dom f & f is E -measurable ) implies a.e-eq-class_Lp (f,M,1) c= a.e-eq-class (f,M) )

assume A1: ex E being Element of S st

( M . (E `) = 0 & E = dom f & f is E -measurable ) ; :: thesis: a.e-eq-class_Lp (f,M,1) c= a.e-eq-class (f,M)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in a.e-eq-class_Lp (f,M,1) or x in a.e-eq-class (f,M) )

assume x in a.e-eq-class_Lp (f,M,1) ; :: thesis: x in a.e-eq-class (f,M)

then consider h being PartFunc of X,REAL such that

A2: ( x = h & h in Lp_Functions (M,1) & f a.e.= h,M ) ;

A3: ex g being PartFunc of X,REAL st

( h = g & ex E being Element of S st

( M . (E `) = 0 & dom g = E & g is E -measurable & (abs g) to_power 1 is_integrable_on M ) ) by A2;

then consider Eh being Element of S such that

A4: ( M . (Eh `) = 0 & dom h = Eh & h is Eh -measurable & (abs h) to_power 1 is_integrable_on M ) ;

A5: dom ((abs h) to_power 1) = dom (abs h) by MESFUN6C:def 4;

for x being Element of X st x in dom ((abs h) to_power 1) holds

((abs h) to_power 1) . x = (abs h) . x

then A6: h is_integrable_on M by A3, MESFUNC6:94;

reconsider ND = Eh ` as Element of S by MEASURE1:34;

( M . ND = 0 & dom h = ND ` ) by A4;

then A7: h in L1_Functions M by A6;

ex E being Element of S st

( M . E = 0 & dom f = E ` & f is_integrable_on M )

hence x in a.e-eq-class (f,M) by A2, A7; :: thesis: verum

for M being sigma_Measure of S

for f being PartFunc of X,REAL st ex E being Element of S st

( M . (E `) = 0 & E = dom f & f is E -measurable ) holds

a.e-eq-class_Lp (f,M,1) c= a.e-eq-class (f,M)

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,REAL st ex E being Element of S st

( M . (E `) = 0 & E = dom f & f is E -measurable ) holds

a.e-eq-class_Lp (f,M,1) c= a.e-eq-class (f,M)

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,REAL st ex E being Element of S st

( M . (E `) = 0 & E = dom f & f is E -measurable ) holds

a.e-eq-class_Lp (f,M,1) c= a.e-eq-class (f,M)

let f be PartFunc of X,REAL; :: thesis: ( ex E being Element of S st

( M . (E `) = 0 & E = dom f & f is E -measurable ) implies a.e-eq-class_Lp (f,M,1) c= a.e-eq-class (f,M) )

assume A1: ex E being Element of S st

( M . (E `) = 0 & E = dom f & f is E -measurable ) ; :: thesis: a.e-eq-class_Lp (f,M,1) c= a.e-eq-class (f,M)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in a.e-eq-class_Lp (f,M,1) or x in a.e-eq-class (f,M) )

assume x in a.e-eq-class_Lp (f,M,1) ; :: thesis: x in a.e-eq-class (f,M)

then consider h being PartFunc of X,REAL such that

A2: ( x = h & h in Lp_Functions (M,1) & f a.e.= h,M ) ;

A3: ex g being PartFunc of X,REAL st

( h = g & ex E being Element of S st

( M . (E `) = 0 & dom g = E & g is E -measurable & (abs g) to_power 1 is_integrable_on M ) ) by A2;

then consider Eh being Element of S such that

A4: ( M . (Eh `) = 0 & dom h = Eh & h is Eh -measurable & (abs h) to_power 1 is_integrable_on M ) ;

A5: dom ((abs h) to_power 1) = dom (abs h) by MESFUN6C:def 4;

for x being Element of X st x in dom ((abs h) to_power 1) holds

((abs h) to_power 1) . x = (abs h) . x

proof

then
(abs h) to_power 1 = abs h
by A5, PARTFUN1:5;
let x be Element of X; :: thesis: ( x in dom ((abs h) to_power 1) implies ((abs h) to_power 1) . x = (abs h) . x )

assume x in dom ((abs h) to_power 1) ; :: thesis: ((abs h) to_power 1) . x = (abs h) . x

then ((abs h) to_power 1) . x = ((abs h) . x) to_power 1 by MESFUN6C:def 4;

hence ((abs h) to_power 1) . x = (abs h) . x by POWER:25; :: thesis: verum

end;assume x in dom ((abs h) to_power 1) ; :: thesis: ((abs h) to_power 1) . x = (abs h) . x

then ((abs h) to_power 1) . x = ((abs h) . x) to_power 1 by MESFUN6C:def 4;

hence ((abs h) to_power 1) . x = (abs h) . x by POWER:25; :: thesis: verum

then A6: h is_integrable_on M by A3, MESFUNC6:94;

reconsider ND = Eh ` as Element of S by MEASURE1:34;

( M . ND = 0 & dom h = ND ` ) by A4;

then A7: h in L1_Functions M by A6;

ex E being Element of S st

( M . E = 0 & dom f = E ` & f is_integrable_on M )

proof

then
f in L1_Functions M
;
consider Ef being Element of S such that

A8: ( M . (Ef `) = 0 & Ef = dom f & f is Ef -measurable ) by A1;

reconsider E = Ef ` as Element of S by MEASURE1:34;

take E ; :: thesis: ( M . E = 0 & dom f = E ` & f is_integrable_on M )

consider EE being Element of S such that

A9: ( M . EE = 0 & f | (EE `) = h | (EE `) ) by A2;

reconsider E1 = ND \/ EE as Element of S ;

( ND is measure_zero of M & EE is measure_zero of M ) by A4, A9, MEASURE1:def 7;

then E1 is measure_zero of M by MEASURE1:37;

then A10: M . E1 = 0 by MEASURE1:def 7;

EE c= E1 by XBOOLE_1:7;

then E1 ` c= EE ` by SUBSET_1:12;

then A11: ( f | (E1 `) = (f | (EE `)) | (E1 `) & h | (E1 `) = (h | (EE `)) | (E1 `) ) by FUNCT_1:51;

A12: ( dom (max+ (R_EAL f)) = Ef & dom (max- (R_EAL f)) = Ef ) by A8, MESFUNC2:def 2, MESFUNC2:def 3;

A13: ( Ef = dom (R_EAL f) & R_EAL f is Ef -measurable ) by A8;

then A14: ( max+ (R_EAL f) is Ef -measurable & max- (R_EAL f) is Ef -measurable ) by MESFUNC2:25, MESFUNC2:26;

( ( for x being Element of X holds 0. <= (max+ (R_EAL f)) . x ) & ( for x being Element of X holds 0. <= (max- (R_EAL f)) . x ) ) by MESFUNC2:12, MESFUNC2:13;

then A15: ( max+ (R_EAL f) is nonnegative & max- (R_EAL f) is nonnegative ) by SUPINF_2:39;

A16: Ef = (Ef /\ E1) \/ (Ef \ E1) by XBOOLE_1:51;

reconsider E0 = Ef /\ E1 as Element of S ;

A17: Ef \ E1 = Ef /\ (E1 `) by SUBSET_1:13;

reconsider E2 = Ef \ E1 as Element of S ;

( max+ (R_EAL f) = (max+ (R_EAL f)) | (dom (max+ (R_EAL f))) & max- (R_EAL f) = (max- (R_EAL f)) | (dom (max- (R_EAL f))) ) by RELAT_1:69;

then A18: ( integral+ (M,(max+ (R_EAL f))) = (integral+ (M,((max+ (R_EAL f)) | E0))) + (integral+ (M,((max+ (R_EAL f)) | E2))) & integral+ (M,(max- (R_EAL f))) = (integral+ (M,((max- (R_EAL f)) | E0))) + (integral+ (M,((max- (R_EAL f)) | E2))) ) by A12, A15, A16, A14, MESFUNC5:81, XBOOLE_1:89;

A19: ( integral+ (M,((max+ (R_EAL f)) | E0)) >= 0 & integral+ (M,((max- (R_EAL f)) | E0)) >= 0 ) by A15, A14, A12, MESFUNC5:80;

( integral+ (M,((max+ (R_EAL f)) | E1)) = 0 & integral+ (M,((max- (R_EAL f)) | E1)) = 0 ) by A10, A12, A15, A14, MESFUNC5:82;

then ( integral+ (M,((max+ (R_EAL f)) | E0)) = 0 & integral+ (M,((max- (R_EAL f)) | E0)) = 0 ) by A19, A12, A15, A14, MESFUNC5:83, XBOOLE_1:17;

then A20: ( integral+ (M,(max+ (R_EAL f))) = integral+ (M,((max+ (R_EAL f)) | E2)) & integral+ (M,(max- (R_EAL f))) = integral+ (M,((max- (R_EAL f)) | E2)) ) by A18, XXREAL_3:4;

A21: E2 c= E1 ` by A17, XBOOLE_1:17;

then f | E2 = (h | (E1 `)) | E2 by A9, A11, FUNCT_1:51;

then A22: (R_EAL f) | E2 = (R_EAL h) | E2 by A21, FUNCT_1:51;

A23: ( (max+ (R_EAL f)) | E2 = max+ ((R_EAL f) | E2) & (max+ (R_EAL h)) | E2 = max+ ((R_EAL h) | E2) & (max- (R_EAL f)) | E2 = max- ((R_EAL f) | E2) & (max- (R_EAL h)) | E2 = max- ((R_EAL h) | E2) ) by MESFUNC5:28;

A24: R_EAL h is_integrable_on M by A6;

then A25: ( integral+ (M,(max+ (R_EAL h))) < +infty & integral+ (M,(max- (R_EAL h))) < +infty ) ;

( integral+ (M,(max+ ((R_EAL h) | E2))) <= integral+ (M,(max+ (R_EAL h))) & integral+ (M,(max- ((R_EAL h) | E2))) <= integral+ (M,(max- (R_EAL h))) ) by A24, MESFUNC5:97;

then ( integral+ (M,(max+ (R_EAL f))) < +infty & integral+ (M,(max- (R_EAL f))) < +infty ) by A20, A25, A23, A22, XXREAL_0:2;

then R_EAL f is_integrable_on M by A13;

hence ( M . E = 0 & dom f = E ` & f is_integrable_on M ) by A8; :: thesis: verum

end;A8: ( M . (Ef `) = 0 & Ef = dom f & f is Ef -measurable ) by A1;

reconsider E = Ef ` as Element of S by MEASURE1:34;

take E ; :: thesis: ( M . E = 0 & dom f = E ` & f is_integrable_on M )

consider EE being Element of S such that

A9: ( M . EE = 0 & f | (EE `) = h | (EE `) ) by A2;

reconsider E1 = ND \/ EE as Element of S ;

( ND is measure_zero of M & EE is measure_zero of M ) by A4, A9, MEASURE1:def 7;

then E1 is measure_zero of M by MEASURE1:37;

then A10: M . E1 = 0 by MEASURE1:def 7;

EE c= E1 by XBOOLE_1:7;

then E1 ` c= EE ` by SUBSET_1:12;

then A11: ( f | (E1 `) = (f | (EE `)) | (E1 `) & h | (E1 `) = (h | (EE `)) | (E1 `) ) by FUNCT_1:51;

A12: ( dom (max+ (R_EAL f)) = Ef & dom (max- (R_EAL f)) = Ef ) by A8, MESFUNC2:def 2, MESFUNC2:def 3;

A13: ( Ef = dom (R_EAL f) & R_EAL f is Ef -measurable ) by A8;

then A14: ( max+ (R_EAL f) is Ef -measurable & max- (R_EAL f) is Ef -measurable ) by MESFUNC2:25, MESFUNC2:26;

( ( for x being Element of X holds 0. <= (max+ (R_EAL f)) . x ) & ( for x being Element of X holds 0. <= (max- (R_EAL f)) . x ) ) by MESFUNC2:12, MESFUNC2:13;

then A15: ( max+ (R_EAL f) is nonnegative & max- (R_EAL f) is nonnegative ) by SUPINF_2:39;

A16: Ef = (Ef /\ E1) \/ (Ef \ E1) by XBOOLE_1:51;

reconsider E0 = Ef /\ E1 as Element of S ;

A17: Ef \ E1 = Ef /\ (E1 `) by SUBSET_1:13;

reconsider E2 = Ef \ E1 as Element of S ;

( max+ (R_EAL f) = (max+ (R_EAL f)) | (dom (max+ (R_EAL f))) & max- (R_EAL f) = (max- (R_EAL f)) | (dom (max- (R_EAL f))) ) by RELAT_1:69;

then A18: ( integral+ (M,(max+ (R_EAL f))) = (integral+ (M,((max+ (R_EAL f)) | E0))) + (integral+ (M,((max+ (R_EAL f)) | E2))) & integral+ (M,(max- (R_EAL f))) = (integral+ (M,((max- (R_EAL f)) | E0))) + (integral+ (M,((max- (R_EAL f)) | E2))) ) by A12, A15, A16, A14, MESFUNC5:81, XBOOLE_1:89;

A19: ( integral+ (M,((max+ (R_EAL f)) | E0)) >= 0 & integral+ (M,((max- (R_EAL f)) | E0)) >= 0 ) by A15, A14, A12, MESFUNC5:80;

( integral+ (M,((max+ (R_EAL f)) | E1)) = 0 & integral+ (M,((max- (R_EAL f)) | E1)) = 0 ) by A10, A12, A15, A14, MESFUNC5:82;

then ( integral+ (M,((max+ (R_EAL f)) | E0)) = 0 & integral+ (M,((max- (R_EAL f)) | E0)) = 0 ) by A19, A12, A15, A14, MESFUNC5:83, XBOOLE_1:17;

then A20: ( integral+ (M,(max+ (R_EAL f))) = integral+ (M,((max+ (R_EAL f)) | E2)) & integral+ (M,(max- (R_EAL f))) = integral+ (M,((max- (R_EAL f)) | E2)) ) by A18, XXREAL_3:4;

A21: E2 c= E1 ` by A17, XBOOLE_1:17;

then f | E2 = (h | (E1 `)) | E2 by A9, A11, FUNCT_1:51;

then A22: (R_EAL f) | E2 = (R_EAL h) | E2 by A21, FUNCT_1:51;

A23: ( (max+ (R_EAL f)) | E2 = max+ ((R_EAL f) | E2) & (max+ (R_EAL h)) | E2 = max+ ((R_EAL h) | E2) & (max- (R_EAL f)) | E2 = max- ((R_EAL f) | E2) & (max- (R_EAL h)) | E2 = max- ((R_EAL h) | E2) ) by MESFUNC5:28;

A24: R_EAL h is_integrable_on M by A6;

then A25: ( integral+ (M,(max+ (R_EAL h))) < +infty & integral+ (M,(max- (R_EAL h))) < +infty ) ;

( integral+ (M,(max+ ((R_EAL h) | E2))) <= integral+ (M,(max+ (R_EAL h))) & integral+ (M,(max- ((R_EAL h) | E2))) <= integral+ (M,(max- (R_EAL h))) ) by A24, MESFUNC5:97;

then ( integral+ (M,(max+ (R_EAL f))) < +infty & integral+ (M,(max- (R_EAL f))) < +infty ) by A20, A25, A23, A22, XXREAL_0:2;

then R_EAL f is_integrable_on M by A13;

hence ( M . E = 0 & dom f = E ` & f is_integrable_on M ) by A8; :: thesis: verum

hence x in a.e-eq-class (f,M) by A2, A7; :: thesis: verum