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 f in L1_Functions M & Integral M,(abs f) = 0 holds
f a.e.= X --> 0 ,M
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL st f in L1_Functions M & Integral M,(abs f) = 0 holds
f a.e.= X --> 0 ,M
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,REAL st f in L1_Functions M & Integral M,(abs f) = 0 holds
f a.e.= X --> 0 ,M
let f be PartFunc of X,REAL ; :: thesis: ( f in L1_Functions M & Integral M,(abs f) = 0 implies f a.e.= X --> 0 ,M )
assume that
A1: f in L1_Functions M and
A2: Integral M,(abs f) = 0 ; :: thesis: f a.e.= X --> 0 ,M
set g = X --> 0 ;
defpred S1[ Element of NAT , set ] means ( $2 = great_eq_dom (abs f),(1 / ($1 + 1)) & M . $2 = 0 );
consider f1 being PartFunc of X,REAL such that
A3: f = f1 and
A4: ex ND being Element of S st
( M . ND = 0 & dom f1 = ND ` & f1 is_integrable_on M ) by A1;
A5: abs f is_integrable_on M by A3, A4, Th44;
then R_EAL (abs f) is_integrable_on M by MESFUNC6:def 9;
then consider E being Element of S such that
A6: E = dom (R_EAL (abs f)) and
A7: R_EAL (abs f) is_measurable_on E by MESFUNC5:def 17;
A8: abs f is_measurable_on E by A7, MESFUNC6:def 6;
now
let x be set ; :: thesis: ( x in dom (abs f) implies 0 <= (abs f) . x )
assume x in dom (abs f) ; :: thesis: 0 <= (abs f) . x
then (abs f) . x = abs (f . x) by VALUED_1:def 11;
hence 0 <= (abs f) . x by COMPLEX1:132; :: thesis: verum
end;
then A9: abs f is nonnegative by MESFUNC6:52;
A10: now
let n be Element of NAT ; :: thesis: ex B being Element of S st S1[n,B]
set r = 1 / (n + 1);
reconsider Br = E /\ (great_eq_dom (abs f),(1 / (n + 1))) as Element of S by A6, A8, MESFUNC6:13;
set g = Br --> (1 / (n + 1));
A11: dom (Br --> (1 / (n + 1))) = Br by FUNCT_2:def 1;
A12: for x being set st x in dom (Br --> (1 / (n + 1))) holds
(Br --> (1 / (n + 1))) . x = 1 / (n + 1) by FUNCOP_1:13;
reconsider g = Br --> (1 / (n + 1)) as PartFunc of X,REAL by RELSET_1:17;
A13: (abs f) | Br is_integrable_on M by A5, MESFUNC6:91;
for x being set st x in dom g holds
0 <= g . x by A12;
then g is nonnegative by MESFUNC6:52;
then A14: 0 <= Integral M,g by A11, A12, Th53, MESFUNC6:84;
A15: dom (abs g) = dom g by VALUED_1:def 11;
A16: now
let x be Element of X; :: thesis: ( x in dom (abs g) implies (abs g) . x = g . x )
assume A17: x in dom (abs g) ; :: thesis: (abs g) . x = g . x
then (abs g) . x = abs (g . x) by VALUED_1:def 11;
then (abs g) . x = abs (1 / (n + 1)) by A12, A15, A17;
then (abs g) . x = 1 / (n + 1) by ABSVALUE:def 1;
hence (abs g) . x = g . x by A12, A15, A17; :: thesis: verum
end;
A18: dom ((abs f) | Br) = (dom (abs f)) /\ Br by RELAT_1:90
.= Br by A6, XBOOLE_1:17, XBOOLE_1:28 ;
then A19: dom g = dom ((abs f) | Br) by FUNCT_2:def 1;
A20: now
let x be Element of X; :: thesis: ( x in dom g implies abs (g . x) <= ((abs f) | Br) . x )
assume A21: x in dom g ; :: thesis: abs (g . x) <= ((abs f) | Br) . x
then x in E /\ (great_eq_dom (abs f),(1 / (n + 1))) by FUNCT_2:def 1;
then x in great_eq_dom (abs f),(1 / (n + 1)) by XBOOLE_0:def 4;
then A22: ex y being Real st
( y = (abs f) . x & 1 / (n + 1) <= y ) by MESFUNC6:6;
abs (g . x) = abs (1 / (n + 1)) by A12, A21;
then abs (g . x) = 1 / (n + 1) by ABSVALUE:def 1;
hence abs (g . x) <= ((abs f) | Br) . x by A19, A21, A22, FUNCT_1:70; :: thesis: verum
end;
g is_measurable_on Br by A11, A12, Th53;
then Integral M,(abs g) <= Integral M,((abs f) | Br) by A11, A18, A13, A20, MESFUNC6:96;
then A23: Integral M,g <= Integral M,((abs f) | Br) by A15, A16, PARTFUN1:34;
A24: for x being set st x in dom g holds
g . x = 1 / (n + 1) by A11, FUNCOP_1:13;
Integral M,((abs f) | Br) <= Integral M,((abs f) | E) by A6, A8, A9, MESFUNC6:87, XBOOLE_1:17;
then Integral M,g = 0 by A2, A6, A23, A14, RELAT_1:97;
then (R_EAL (1 / (n + 1))) * (M . Br) = 0 by A11, A24, MESFUNC6:97;
then A25: M . Br = 0 ;
for x being set st x in great_eq_dom (abs f),(1 / (n + 1)) holds
x in dom (abs f) by MESFUNC6:6;
then great_eq_dom (abs f),(1 / (n + 1)) c= E by A6, TARSKI:def 3;
hence ex B being Element of S st S1[n,B] by A25, XBOOLE_1:28; :: thesis: verum
end;
consider F being Function of NAT ,S such that
A26: for n being Element of NAT holds S1[n,F . n] from FUNCT_2:sch 3(A10);
now
let y be set ; :: thesis: ( y in union (rng F) implies y in { x where x is Element of X : ( x in dom f & f . x <> 0 ) } )
assume y in union (rng F) ; :: thesis: y in { x where x is Element of X : ( x in dom f & f . x <> 0 ) }
then consider B being set such that
A27: y in B and
A28: B in rng F by TARSKI:def 4;
consider n being set such that
A29: n in NAT and
A30: B = F . n by A28, FUNCT_2:17;
reconsider m = n as Element of NAT by A29;
A31: y in great_eq_dom (abs f),(1 / (m + 1)) by A26, A27, A30;
then A32: y in dom (abs f) by MESFUNC6:6;
then A33: y in dom f by VALUED_1:def 11;
A34: (abs f) . y = abs (f . y) by A32, VALUED_1:def 11;
(abs f) . y <> 0 by A31, MESFUNC1:def 15;
then f . y <> 0 by A34, ABSVALUE:7;
hence y in { x where x is Element of X : ( x in dom f & f . x <> 0 ) } by A33; :: thesis: verum
end;
then A35: union (rng F) c= { x where x is Element of X : ( x in dom f & f . x <> 0 ) } by TARSKI:def 3;
consider ND being Element of S such that
A36: M . ND = 0 and
A37: dom f1 = ND ` and
f1 is_integrable_on M by A4;
reconsider EQ = (union (rng F)) \/ ND as Element of S ;
A38: EQ ` = (ND ` ) /\ ((union (rng F)) ` ) by XBOOLE_1:53;
then A39: EQ ` c= dom f by A3, A37, XBOOLE_1:17;
dom (X --> 0 ) = X by FUNCOP_1:19;
then A40: dom ((X --> 0 ) | (EQ ` )) = EQ ` by RELAT_1:91;
A41: dom (f | (EQ ` )) = EQ ` by A3, A37, A38, RELAT_1:91, XBOOLE_1:17;
now
let y be set ; :: thesis: ( y in { x where x is Element of X : ( x in dom f & f . x <> 0 ) } implies y in union (rng F) )
assume y in { x where x is Element of X : ( x in dom f & f . x <> 0 ) } ; :: thesis: y in union (rng F)
then consider z being Element of X such that
A42: y = z and
A43: z in dom f and
A44: f . z <> 0 ;
A45: z in dom (abs f) by A43, VALUED_1:def 11;
then (abs f) . z = abs (f . z) by VALUED_1:def 11;
then 0 < (abs f) . z by A44, COMPLEX1:133;
then consider n being Element of NAT such that
A46: 1 / (n + 1) < ((abs f) . z) - 0 by MESFUNC1:13;
z in great_eq_dom (abs f),(1 / (n + 1)) by A45, A46, MESFUNC6:6;
then A47: y in F . n by A26, A42;
F . n in rng F by FUNCT_2:6;
hence y in union (rng F) by A47, TARSKI:def 4; :: thesis: verum
end;
then { x where x is Element of X : ( x in dom f & f . x <> 0 ) } c= union (rng F) by TARSKI:def 3;
then A48: { x where x is Element of X : ( x in dom f & f . x <> 0 ) } = union (rng F) by A35, XBOOLE_0:def 10;
A49: now
let x be set ; :: thesis: ( x in EQ ` implies f . x = 0 )
assume A50: x in EQ ` ; :: thesis: f . x = 0
then x in (union (rng F)) ` by A38, XBOOLE_0:def 4;
then not x in union (rng F) by XBOOLE_0:def 5;
hence f . x = 0 by A48, A39, A50; :: thesis: verum
end;
now
let y be set ; :: thesis: ( y in dom (f | (EQ ` )) implies (f | (EQ ` )) . y = ((X --> 0 ) | (EQ ` )) . y )
assume A51: y in dom (f | (EQ ` )) ; :: thesis: (f | (EQ ` )) . y = ((X --> 0 ) | (EQ ` )) . y
then (f | (EQ ` )) . y = f . y by FUNCT_1:70;
then (f | (EQ ` )) . y = 0 by A41, A49, A51;
then (f | (EQ ` )) . y = (X --> 0 ) . y by A51, FUNCOP_1:13;
hence (f | (EQ ` )) . y = ((X --> 0 ) | (EQ ` )) . y by A41, A40, A51, FUNCT_1:70; :: thesis: verum
end;
then A52: f | (EQ ` ) = (X --> 0 ) | (EQ ` ) by A39, A40, FUNCT_1:9, RELAT_1:91;
now
let A be set ; :: thesis: ( A in rng F implies A is measure_zero of M )
assume A in rng F ; :: thesis: A is measure_zero of M
then consider n being set such that
A53: n in NAT and
A54: A = F . n by FUNCT_2:17;
reconsider n = n as Element of NAT by A53;
M . (F . n) = 0 by A26;
hence A is measure_zero of M by A54, MEASURE1:def 13; :: thesis: verum
end;
then A55: union (rng F) is measure_zero of M by MEASURE2:16;
ND is measure_zero of M by A36, MEASURE1:def 13;
then EQ is measure_zero of M by A55, MEASURE1:70;
then M . EQ = 0 by MEASURE1:def 13;
hence f a.e.= X --> 0 ,M by A52, Def10; :: thesis: verum