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 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; 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; 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; ( 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 )
; a.e-eq-class_Lp (f,M,1) c= a.e-eq-class (f,M)
let x be object ; TARSKI:def 3 ( 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)
; 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
(abs h) to_power 1 = abs h
by A5, PARTFUN1:5;
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
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
;
( 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;
verum
end;
then
f in L1_Functions M
;
hence
x in a.e-eq-class (f,M)
by A2, A7; verum