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_measurable_on E ) 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_measurable_on E ) 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_measurable_on E ) 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_measurable_on E ) implies a.e-eq-class_Lp (f,M,1) c= a.e-eq-class (f,M) )
assume A2:
ex E being Element of S st
( M . (E `) = 0 & E = dom f & f is_measurable_on E )
; a.e-eq-class_Lp (f,M,1) c= a.e-eq-class (f,M)
now let x be
set ;
( x in a.e-eq-class_Lp (f,M,1) implies 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 A3:
(
x = h &
h in Lp_Functions (
M,1) &
f a.e.= h,
M )
;
A4:
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_measurable_on E &
(abs g) to_power 1
is_integrable_on M ) )
by A3;
then consider Eh being
Element of
S such that A5:
(
M . (Eh `) = 0 &
dom h = Eh &
h is_measurable_on Eh &
(abs h) to_power 1
is_integrable_on M )
;
A6:
dom ((abs h) to_power 1) = dom (abs h)
by MESFUN6C:def 6;
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 A6, PARTFUN1:34;
then A7:
h is_integrable_on M
by A4, MESFUNC6:94;
reconsider ND =
Eh ` as
Element of
S by MEASURE1:66;
(
M . ND = 0 &
dom h = ND ` )
by A5;
then A8:
h in L1_Functions M
by A7;
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 B1:
(
M . (Ef `) = 0 &
Ef = dom f &
f is_measurable_on Ef )
by A2;
reconsider E =
Ef ` as
Element of
S by MEASURE1:66;
take
E
;
( M . E = 0 & dom f = E ` & f is_integrable_on M )
consider EE being
Element of
S such that B3:
(
M . EE = 0 &
f | (EE `) = h | (EE `) )
by A3, LPSPACE1:def 10;
reconsider E1 =
ND \/ EE as
Element of
S ;
(
ND is
measure_zero of
M &
EE is
measure_zero of
M )
by A5, B3, MEASURE1:def 13;
then
E1 is
measure_zero of
M
by MEASURE1:70;
then E2:
M . E1 = 0
by MEASURE1:def 13;
EE c= E1
by XBOOLE_1:7;
then
E1 ` c= EE `
by SUBSET_1:31;
then E3:
(
f | (E1 `) = (f | (EE `)) | (E1 `) &
h | (E1 `) = (h | (EE `)) | (E1 `) )
by FUNCT_1:82;
C3:
(
dom (max+ (R_EAL f)) = Ef &
dom (max- (R_EAL f)) = Ef )
by B1, MESFUNC2:def 2, MESFUNC2:def 3;
C1:
(
Ef = dom (R_EAL f) &
R_EAL f is_measurable_on Ef )
by B1, MESFUNC6:def 6;
then D1:
(
max+ (R_EAL f) is_measurable_on Ef &
max- (R_EAL f) is_measurable_on Ef )
by MESFUNC2:27, MESFUNC2:28;
( ( 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:14, MESFUNC2:15;
then C4:
(
max+ (R_EAL f) is
nonnegative &
max- (R_EAL f) is
nonnegative )
by SUPINF_2:58;
C5:
Ef = (Ef /\ E1) \/ (Ef \ E1)
by XBOOLE_1:51;
reconsider E0 =
Ef /\ E1 as
Element of
S ;
D6:
Ef \ E1 = Ef /\ (E1 `)
by SUBSET_1:32;
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:98;
then D5:
(
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 C3, C4, C5, D1, MESFUNC5:87, XBOOLE_1:89;
D2:
(
integral+ (
M,
((max+ (R_EAL f)) | E0))
>= 0 &
integral+ (
M,
((max- (R_EAL f)) | E0))
>= 0 )
by C4, D1, C3, MESFUNC5:86;
(
integral+ (
M,
((max+ (R_EAL f)) | E1))
= 0 &
integral+ (
M,
((max- (R_EAL f)) | E1))
= 0 )
by E2, C3, C4, D1, MESFUNC5:88;
then
(
integral+ (
M,
((max+ (R_EAL f)) | E0))
= 0 &
integral+ (
M,
((max- (R_EAL f)) | E0))
= 0 )
by D2, C3, C4, D1, MESFUNC5:89, XBOOLE_1:17;
then G1:
(
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 D5, XXREAL_3:4;
D7:
E2 c= E1 `
by D6, XBOOLE_1:17;
then
f | E2 = (h | (E1 `)) | E2
by B3, E3, FUNCT_1:82;
then D8:
(R_EAL f) | E2 = (R_EAL h) | E2
by D7, FUNCT_1:82;
F3:
(
(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:34;
F1:
R_EAL h is_integrable_on M
by A7, MESFUNC6:def 9;
then F2:
(
integral+ (
M,
(max+ (R_EAL h)))
< +infty &
integral+ (
M,
(max- (R_EAL h)))
< +infty )
by MESFUNC5:def 17;
(
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 F1, MESFUNC5:103;
then
(
integral+ (
M,
(max+ (R_EAL f)))
< +infty &
integral+ (
M,
(max- (R_EAL f)))
< +infty )
by G1, F2, F3, D8, XXREAL_0:2;
then
R_EAL f is_integrable_on M
by C1, MESFUNC5:def 17;
hence
(
M . E = 0 &
dom f = E ` &
f is_integrable_on M )
by B1, MESFUNC6:def 9;
verum
end; then
f in L1_Functions M
;
hence
x in a.e-eq-class (
f,
M)
by A3, A8;
verum end;
hence
a.e-eq-class_Lp (f,M,1) c= a.e-eq-class (f,M)
by TARSKI:def 3; verum