let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for k being positive Real st ex E being Element of S st
( M . (E ` ) = 0 & E = dom f & f is_measurable_on E ) & g in a.e-eq-class_Lp f,M,k holds
( g a.e.= f,M & f in Lp_Functions M,k )
let S be SigmaField of X; for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for k being positive Real st ex E being Element of S st
( M . (E ` ) = 0 & E = dom f & f is_measurable_on E ) & g in a.e-eq-class_Lp f,M,k holds
( g a.e.= f,M & f in Lp_Functions M,k )
let M be sigma_Measure of S; for f, g being PartFunc of X,REAL
for k being positive Real st ex E being Element of S st
( M . (E ` ) = 0 & E = dom f & f is_measurable_on E ) & g in a.e-eq-class_Lp f,M,k holds
( g a.e.= f,M & f in Lp_Functions M,k )
let f, g be PartFunc of X,REAL ; for k being positive Real st ex E being Element of S st
( M . (E ` ) = 0 & E = dom f & f is_measurable_on E ) & g in a.e-eq-class_Lp f,M,k holds
( g a.e.= f,M & f in Lp_Functions M,k )
let k be positive Real; ( ex E being Element of S st
( M . (E ` ) = 0 & E = dom f & f is_measurable_on E ) & g in a.e-eq-class_Lp f,M,k implies ( g a.e.= f,M & f in Lp_Functions M,k ) )
assume that
A1:
ex E being Element of S st
( M . (E ` ) = 0 & E = dom f & f is_measurable_on E )
and
A2:
g in a.e-eq-class_Lp f,M,k
; ( g a.e.= f,M & f in Lp_Functions M,k )
A3:
ex r being PartFunc of X,REAL st
( g = r & r in Lp_Functions M,k & f a.e.= r,M )
by A2;
hence
g a.e.= f,M
by LPSPACE1:29; f in Lp_Functions M,k
g in Lp_Functions M,k
by A2;
then consider g1 being PartFunc of X,REAL such that
A4:
( g = g1 & ex E being Element of S st
( M . (E ` ) = 0 & dom g1 = E & g1 is_measurable_on E & (abs g1) to_power k is_integrable_on M ) )
;
consider Eh being Element of S such that
A5:
( M . (Eh ` ) = 0 & dom g = Eh & g is_measurable_on Eh & (abs g) to_power k is_integrable_on M )
by A4;
reconsider ND = Eh ` as Element of S by MEASURE1:66;
ex E being Element of S st
( M . (E ` ) = 0 & dom f = E & f is_measurable_on E & (abs f) to_power k is_integrable_on M )
proof
set AFK =
(abs f) to_power k;
set AGK =
(abs g) to_power k;
consider Ef being
Element of
S such that B1:
(
M . (Ef ` ) = 0 &
Ef = dom f &
f is_measurable_on Ef )
by A1;
take
Ef
;
( M . (Ef ` ) = 0 & dom f = Ef & f is_measurable_on Ef & (abs f) to_power k is_integrable_on M )
consider EE being
Element of
S such that B2:
(
M . EE = 0 &
g | (EE ` ) = f | (EE ` ) )
by A3, LPSPACE1:def 10;
reconsider E1 =
ND \/ EE as
Element of
S ;
EE c= E1
by XBOOLE_1:7;
then
E1 ` c= EE `
by SUBSET_1:31;
then B3:
(
f | (E1 ` ) = (f | (EE ` )) | (E1 ` ) &
g | (E1 ` ) = (g | (EE ` )) | (E1 ` ) )
by FUNCT_1:82;
B4:
dom (abs f) = Ef
by B1, VALUED_1:def 11;
then
dom ((abs f) to_power k) = Ef
by MESFUN6C:def 6;
then B5:
(
dom (max+ (R_EAL ((abs f) to_power k))) = Ef &
dom (max- (R_EAL ((abs f) to_power k))) = Ef )
by MESFUNC2:def 2, MESFUNC2:def 3;
abs f is_measurable_on Ef
by B1, MESFUNC6:48;
then
(abs f) to_power k is_measurable_on Ef
by B4, MESFUN6C:29;
then B6:
(
Ef = dom (R_EAL ((abs f) to_power k)) &
R_EAL ((abs f) to_power k) is_measurable_on Ef )
by B4, MESFUN6C:def 6, MESFUNC6:def 6;
then B7:
(
max+ (R_EAL ((abs f) to_power k)) is_measurable_on Ef &
max- (R_EAL ((abs f) to_power k)) is_measurable_on Ef )
by MESFUNC2:27, MESFUNC2:28;
( ( for
x being
Element of
X holds
0. <= (max+ (R_EAL ((abs f) to_power k))) . x ) & ( for
x being
Element of
X holds
0. <= (max- (R_EAL ((abs f) to_power k))) . x ) )
by MESFUNC2:14, MESFUNC2:15;
then B8:
(
max+ (R_EAL ((abs f) to_power k)) is
nonnegative &
max- (R_EAL ((abs f) to_power k)) is
nonnegative )
by SUPINF_2:58;
B9:
Ef = (Ef /\ E1) \/ (Ef \ E1)
by XBOOLE_1:51;
reconsider E0 =
Ef /\ E1 as
Element of
S ;
reconsider E2 =
Ef \ E1 as
Element of
S ;
(
max+ (R_EAL ((abs f) to_power k)) = (max+ (R_EAL ((abs f) to_power k))) | (dom (max+ (R_EAL ((abs f) to_power k)))) &
max- (R_EAL ((abs f) to_power k)) = (max- (R_EAL ((abs f) to_power k))) | (dom (max- (R_EAL ((abs f) to_power k)))) )
by RELAT_1:98;
then B10:
(
integral+ M,
(max+ (R_EAL ((abs f) to_power k))) = (integral+ M,((max+ (R_EAL ((abs f) to_power k))) | E0)) + (integral+ M,((max+ (R_EAL ((abs f) to_power k))) | E2)) &
integral+ M,
(max- (R_EAL ((abs f) to_power k))) = (integral+ M,((max- (R_EAL ((abs f) to_power k))) | E0)) + (integral+ M,((max- (R_EAL ((abs f) to_power k))) | E2)) )
by B5, B7, B8, B9, MESFUNC5:87, XBOOLE_1:89;
B11:
(
integral+ M,
((max+ (R_EAL ((abs f) to_power k))) | E0) >= 0 &
integral+ M,
((max- (R_EAL ((abs f) to_power k))) | E0) >= 0 )
by B7, B8, B5, MESFUNC5:86;
(
ND is
measure_zero of
M &
EE is
measure_zero of
M )
by A5, B2, MEASURE1:def 13;
then
E1 is
measure_zero of
M
by MEASURE1:70;
then
M . E1 = 0
by MEASURE1:def 13;
then
(
integral+ M,
((max+ (R_EAL ((abs f) to_power k))) | E1) = 0 &
integral+ M,
((max- (R_EAL ((abs f) to_power k))) | E1) = 0 )
by B5, B7, B8, MESFUNC5:88;
then
(
integral+ M,
((max+ (R_EAL ((abs f) to_power k))) | E0) = 0 &
integral+ M,
((max- (R_EAL ((abs f) to_power k))) | E0) = 0 )
by B5, B7, B8, B11, MESFUNC5:89, XBOOLE_1:17;
then B12:
(
integral+ M,
(max+ (R_EAL ((abs f) to_power k))) = integral+ M,
((max+ (R_EAL ((abs f) to_power k))) | E2) &
integral+ M,
(max- (R_EAL ((abs f) to_power k))) = integral+ M,
((max- (R_EAL ((abs f) to_power k))) | E2) )
by B10, XXREAL_3:4;
Ef \ E1 = Ef /\ (E1 ` )
by SUBSET_1:32;
then B13:
E2 c= E1 `
by XBOOLE_1:17;
then
f | E2 = (g | (E1 ` )) | E2
by B2, B3, FUNCT_1:82;
then B14:
f | E2 = g | E2
by B13, FUNCT_1:82;
B15:
(
(abs f) | E2 = abs (f | E2) &
(abs g) | E2 = abs (g | E2) )
by RFUNCT_1:62;
B16:
(
((abs f) | E2) to_power k = ((abs f) to_power k) | E2 &
((abs g) | E2) to_power k = ((abs g) to_power k) | E2 )
by Lm001g;
B17:
(
(max+ (R_EAL ((abs f) to_power k))) | E2 = max+ ((R_EAL ((abs f) to_power k)) | E2) &
(max+ (R_EAL ((abs g) to_power k))) | E2 = max+ ((R_EAL ((abs g) to_power k)) | E2) &
(max- (R_EAL ((abs f) to_power k))) | E2 = max- ((R_EAL ((abs f) to_power k)) | E2) &
(max- (R_EAL ((abs g) to_power k))) | E2 = max- ((R_EAL ((abs g) to_power k)) | E2) )
by MESFUNC5:34;
B18:
R_EAL ((abs g) to_power k) is_integrable_on M
by A5, MESFUNC6:def 9;
then B19:
(
integral+ M,
(max+ (R_EAL ((abs g) to_power k))) < +infty &
integral+ M,
(max- (R_EAL ((abs g) to_power k))) < +infty )
by MESFUNC5:def 17;
(
integral+ M,
(max+ ((R_EAL ((abs g) to_power k)) | E2)) <= integral+ M,
(max+ (R_EAL ((abs g) to_power k))) &
integral+ M,
(max- ((R_EAL ((abs g) to_power k)) | E2)) <= integral+ M,
(max- (R_EAL ((abs g) to_power k))) )
by B18, MESFUNC5:103;
then
(
integral+ M,
(max+ (R_EAL ((abs f) to_power k))) < +infty &
integral+ M,
(max- (R_EAL ((abs f) to_power k))) < +infty )
by B12, B14, B15, B16, B17, B19, XXREAL_0:2;
then
R_EAL ((abs f) to_power k) is_integrable_on M
by B6, MESFUNC5:def 17;
hence
(
M . (Ef ` ) = 0 &
dom f = Ef &
f is_measurable_on Ef &
(abs f) to_power k is_integrable_on M )
by B1, MESFUNC6:def 9;
verum
end;
hence
f in Lp_Functions M,k
; verum