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 E -measurable ) & 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 E -measurable ) & 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 E -measurable ) & 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 E -measurable ) & 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 E -measurable ) & 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 E -measurable )
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
; 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 E -measurable & (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 Eh -measurable & (abs g) to_power k is_integrable_on M )
by A4;
reconsider ND = Eh ` as Element of S by MEASURE1:34;
ex E being Element of S st
( M . (E `) = 0 & dom f = E & f is E -measurable & (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 A6:
(
M . (Ef `) = 0 &
Ef = dom f &
f is
Ef -measurable )
by A1;
take
Ef
;
( M . (Ef `) = 0 & dom f = Ef & f is Ef -measurable & (abs f) to_power k is_integrable_on M )
consider EE being
Element of
S such that A7:
(
M . EE = 0 &
g | (EE `) = f | (EE `) )
by A3;
reconsider E1 =
ND \/ EE as
Element of
S ;
EE c= E1
by XBOOLE_1:7;
then
E1 ` c= EE `
by SUBSET_1:12;
then A8:
(
f | (E1 `) = (f | (EE `)) | (E1 `) &
g | (E1 `) = (g | (EE `)) | (E1 `) )
by FUNCT_1:51;
A9:
dom (abs f) = Ef
by A6, VALUED_1:def 11;
then
dom ((abs f) to_power k) = Ef
by MESFUN6C:def 4;
then A10:
(
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
Ef -measurable
by A6, MESFUNC6:48;
then
(abs f) to_power k is
Ef -measurable
by A9, MESFUN6C:29;
then A11:
(
Ef = dom (R_EAL ((abs f) to_power k)) &
R_EAL ((abs f) to_power k) is
Ef -measurable )
by A9, MESFUN6C:def 4;
then A12:
(
max+ (R_EAL ((abs f) to_power k)) is
Ef -measurable &
max- (R_EAL ((abs f) to_power k)) is
Ef -measurable )
by MESFUNC2:25, MESFUNC2:26;
( ( 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:12, MESFUNC2:13;
then A13:
(
max+ (R_EAL ((abs f) to_power k)) is
nonnegative &
max- (R_EAL ((abs f) to_power k)) is
nonnegative )
by SUPINF_2:39;
A14:
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:69;
then A15:
(
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 A10, A12, A13, A14, MESFUNC5:81, XBOOLE_1:89;
A16:
(
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 A12, A13, A10, MESFUNC5:80;
(
ND is
measure_zero of
M &
EE is
measure_zero of
M )
by A5, A7, MEASURE1:def 7;
then
E1 is
measure_zero of
M
by MEASURE1:37;
then
M . E1 = 0
by MEASURE1:def 7;
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 A10, A12, A13, MESFUNC5:82;
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 A10, A12, A13, A16, MESFUNC5:83, XBOOLE_1:17;
then A17:
(
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 A15, XXREAL_3:4;
Ef \ E1 = Ef /\ (E1 `)
by SUBSET_1:13;
then A18:
E2 c= E1 `
by XBOOLE_1:17;
then
f | E2 = (g | (E1 `)) | E2
by A7, A8, FUNCT_1:51;
then A19:
f | E2 = g | E2
by A18, FUNCT_1:51;
A20:
(
(abs f) | E2 = abs (f | E2) &
(abs g) | E2 = abs (g | E2) )
by RFUNCT_1:46;
A21:
(
((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 Th20;
A22:
(
(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:28;
A23:
R_EAL ((abs g) to_power k) is_integrable_on M
by A5;
then A24:
(
integral+ (
M,
(max+ (R_EAL ((abs g) to_power k))))
< +infty &
integral+ (
M,
(max- (R_EAL ((abs g) to_power k))))
< +infty )
;
(
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 A23, MESFUNC5:97;
then
(
integral+ (
M,
(max+ (R_EAL ((abs f) to_power k))))
< +infty &
integral+ (
M,
(max- (R_EAL ((abs f) to_power k))))
< +infty )
by A17, A19, A20, A21, A22, A24, XXREAL_0:2;
then
R_EAL ((abs f) to_power k) is_integrable_on M
by A11;
hence
(
M . (Ef `) = 0 &
dom f = Ef &
f is
Ef -measurable &
(abs f) to_power k is_integrable_on M )
by A6;
verum
end;
hence
f in Lp_Functions (M,k)
; verum