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 4;
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 1;
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:46; :: 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:7;
reconsider g = Br --> (1 / (n + 1)) as PartFunc of X,REAL by RELSET_1:7;
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:61
.= 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:47; :: 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:5;
A24: for x being set st x in dom g holds
g . x = 1 / (n + 1) by A11, FUNCOP_1:7;
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:68;
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:11;
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 14;
then f . y <> 0 by A34, ABSVALUE:2;
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:13;
then A40: dom ((X --> 0) | (EQ `)) = EQ ` by RELAT_1:62;
A41: dom (f | (EQ `)) = EQ ` by A3, A37, A38, RELAT_1:62, 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:47;
then consider n being Element of NAT such that
A46: 1 / (n + 1) < ((abs f) . z) - 0 by MESFUNC1:10;
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:4;
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:47;
then (f | (EQ `)) . y = 0 by A41, A49, A51;
then (f | (EQ `)) . y = (X --> 0) . y by A51, FUNCOP_1:7;
hence (f | (EQ `)) . y = ((X --> 0) | (EQ `)) . y by A41, A40, A51, FUNCT_1:47; :: thesis: verum
end;
then A52: f | (EQ `) = (X --> 0) | (EQ `) by A39, A40, FUNCT_1:2, RELAT_1:62;
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:11;
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 7; :: thesis: verum
end;
then A55: union (rng F) is measure_zero of M by MEASURE2:14;
ND is measure_zero of M by A36, MEASURE1:def 7;
then EQ is measure_zero of M by A55, MEASURE1:37;
then M . EQ = 0 by MEASURE1:def 7;
hence f a.e.= X --> 0,M by A52, Def10; :: thesis: verum