let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let f be with_the_same_dom Functional_Sequence of X,ExtREAL; :: thesis:
let g be PartFunc of X,ExtREAL; :: thesis:
let E be Element of S; :: thesis:
assume that
A1: dom (f . 0) = E and
A2: for n being natural number holds f . n is_measurable_on E and
A3: M . E < +infty and
A4: for n being natural number ex L being Element of S st
( L c= E & M . (E \ L) = 0 & ( for x being Element of X st x in L holds
|.((f . n) . x).| < +infty ) ) and
A5: ex G being Element of S st
( G c= E & M . (E \ G) = 0 & ( for x being Element of X st x in E holds
f # x is convergent_to_finite_number ) & dom g = E & ( for x being Element of X st x in G holds
g . x = lim (f # x) ) ) ; :: thesis:
defpred S₁[ Element of NAT , set ] means ( $2 c= E & M . (E \ $2) = 0 & ( for x being Element of X st x in $2 holds
|.((f . $1) . x).| < +infty ) );
A6: for n being Element of NAT ex Z being Element of S st S₁[n,Z] by A4;
consider LN being Function of NAT,S such that
A7: for n being Element of NAT holds S₁[n,LN . n] from FUNCT_2:sch 10(A6);
rng LN is N_Sub_set_fam of X by MEASURE1:23;
then rng LN is N_Measure_fam of S by MEASURE2:def 1;
then reconsider MRLN = meet (rng LN) as Element of S by MEASURE2:2;
let e0 be real number ; :: thesis:
assume A8: 0 < e0 ; :: thesis:
set e = e0 / 2;
consider G being Element of S such that
A9: G c= E and
A10: M . (E \ G) = 0 and
A11: for x being Element of X st x in E holds
f # x is convergent_to_finite_number and
A12: dom g = E and
A13: for x being Element of X st x in G holds
g . x = lim (f # x) by A5;
MRLN /\ G is Element of S ;
then reconsider L = (meet (rng LN)) /\ G as Element of S ;
set gL = g | L;
A14: L c= G by XBOOLE_1:17;
then M . L <= M . E by A9, MEASURE1:31, XBOOLE_1:1;
then A15: M . L < +infty by A3, XXREAL_0:2;
dom (g | L) = (dom g) /\ L by RELAT_1:61;
then A16: dom (g | L) = L by A9, A12, A14, XBOOLE_1:1, XBOOLE_1:28;
deffunc H₁( Nat) -> Element of bool [:X,ExtREAL:] = (f . $1) | L;
consider fL being Functional_Sequence of X,ExtREAL such that
A17: for n being Nat holds fL . n = H₁(n) from SEQFUNC:sch 1();
for n, m being Nat holds dom (fL . n) = dom (fL . m)

let n, m be Nat; :: thesis:
fL . m = (f . m) | L by A17;
then A18: dom (fL . m) = (dom (f . m)) /\ L by RELAT_1:61;
fL . n = (f . n) | L by A17;
then dom (fL . n) = (dom (f . n)) /\ L by RELAT_1:61;
hence dom (fL . n) = dom (fL . m) by A18, Def2; :: thesis:

end;

then reconsider fL = fL as with_the_same_dom Functional_Sequence of X,ExtREAL by Def2;
A19: L c= E by A9, A14, XBOOLE_1:1;
A20: for x being Element of X st x in L holds
( fL # x is convergent_to_finite_number & (g | L) . x = lim (fL # x) )

proof

let x be Element of X; :: thesis:
A21: dom (fL # x) = NAT by FUNCT_2:def 1;
A22: dom (f # x) = NAT by FUNCT_2:def 1;
assume A23: x in L ; :: thesis:
A24: for y being set st y in NAT holds
(fL # x) . y = (f # x) . y

proof

let y be set ; :: thesis:
assume y in NAT ; :: thesis:
then reconsider n = y as Element of NAT ;
((f . n) | L) . x = (f . n) . x by A23, FUNCT_1:49;
then A25: (fL . n) . x = (f . n) . x by A17;
(f . n) . x = (f # x) . n by MESFUNC5:def 13;
hence (fL # x) . y = (f # x) . y by A25, MESFUNC5:def 13; :: thesis:

end;

then A26: fL # x = f # x by FUNCT_2:12;
f # x is convergent_to_finite_number by A11, A19, A23;
hence fL # x is convergent_to_finite_number by A21, A22, A24, FUNCT_1:2; :: thesis:
L c= G by XBOOLE_1:17;
then g . x = lim (f # x) by A13, A23;
hence (g | L) . x = lim (fL # x) by A23, A26, FUNCT_1:49; :: thesis:

end;

defpred S₂[ Element of NAT , set ] means ( $2 c= L & M . $2 < ((e0 / 2) (#) ((1 / 2) GeoSeq)) . $1 & ex Np being Element of NAT st
for k being Element of NAT st Np < k holds
for x being Element of X st x in L \ $2 holds
|.(((fL . k) . x) - ((g | L) . x)).| < ((1 / 2) GeoSeq) . $1 );
A27: for n being natural number holds
( dom (fL . n) = L & fL . n is_measurable_on L & fL . n is real-valued )

proof

let n be natural number ; :: thesis:
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
A28: fL . n = (f . n) | L by A17;
then A29: dom (fL . n) = (dom (f . n)) /\ L by RELAT_1:61;
then dom (fL . n9) = E /\ L by A1, Def2;
hence A30: dom (fL . n) = L by A9, A14, XBOOLE_1:1, XBOOLE_1:28; :: thesis:
f . n is_measurable_on L by A2, A19, MESFUNC1:30;
hence fL . n is_measurable_on L by A28, A29, A30, MESFUNC5:42; :: thesis:
for x being Element of X st x in dom (fL . n) holds
|.((fL . n) . x).| < +infty

proof

let x be Element of X; :: thesis:
dom LN = NAT by FUNCT_2:def 1;
then A31: LN . n9 in rng LN by FUNCT_1:3;
assume A32: x in dom (fL . n) ; :: thesis:
then x in meet (rng LN) by A30, XBOOLE_0:def 4;
then x in LN . n by A31, SETFAM_1:def 1;
then |.((f . n9) . x).| < +infty by A7;
hence |.((fL . n) . x).| < +infty by A28, A32, FUNCT_1:47; :: thesis:

end;

hence fL . n is real-valued by MESFUNC2:def 1; :: thesis:

end;

then A33: dom (fL . 0) = L ;
A34: for p being natural number ex Hp being Element of S ex Np being natural number st
( Hp c= L & M . Hp < ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p & ( for k being natural number st Np < k holds
for x being Element of X st x in L \ Hp holds
|.(((fL . k) . x) - ((g | L) . x)).| < ((1 / 2) GeoSeq) . p ) )

proof

let p be natural number ; :: thesis:
reconsider p9 = p as Element of NAT by ORDINAL1:def 12;
A35: ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p = (e0 / 2) * (((1 / 2) GeoSeq) . p9) by SEQ_1:9;
0 < (1 / 2) |^ p by PREPOWER:6;
then A36: 0 < ((1 / 2) GeoSeq) . p9 by PREPOWER:def 1;
0 < (1 / 2) |^ p by PREPOWER:6;
then A37: 0 < ((1 / 2) GeoSeq) . p9 by PREPOWER:def 1;
0 < e0 / 2 by A8, XREAL_1:139;
then 0 < ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p by A36, A35, XREAL_1:129;
hence ex Hp being Element of S ex Np being natural number st
( Hp c= L & M . Hp < ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p & ( for k being natural number st Np < k holds
for x being Element of X st x in L \ Hp holds
|.(((fL . k) . x) - ((g | L) . x)).| < ((1 / 2) GeoSeq) . p ) ) by A15, A27, A33, A16, A20, A37, Th28; :: thesis:

end;

A38: for n being Element of NAT ex Z being Element of S st S₂[n,Z]

proof

let n be Element of NAT ; :: thesis:
reconsider n9 = n as natural number ;
consider Z being Element of S, Np being natural number such that
A39: Z c= L and
A40: M . Z < ((e0 / 2) (#) ((1 / 2) GeoSeq)) . n9 and
A41: for k being natural number st Np < k holds
for x being Element of X st x in L \ Z holds
|.(((fL . k) . x) - ((g | L) . x)).| < ((1 / 2) GeoSeq) . n9 by A34;
reconsider Np9 = Np as Element of NAT by ORDINAL1:def 12;
for k being Element of NAT st Np9 < k holds
for x being Element of X st x in L \ Z holds
|.(((fL . k) . x) - ((g | L) . x)).| < ((1 / 2) GeoSeq) . n9 by A41;
hence ex Z being Element of S st S₂[n,Z] by A39, A40; :: thesis:

end;

consider HP being Function of NAT,S such that
A42: for p being Element of NAT holds S₂[p,HP . p] from FUNCT_2:sch 10(A38);
defpred S₃[ Element of NAT , set ] means $2 = M . (HP . $1);
A43: for n being Element of NAT ex y being Element of REAL st S₃[n,y]

proof

let n be Element of NAT ; :: thesis:
A44: -infty < M . (HP . n) by MEASURE1:def 2;
M . (HP . n) < ((e0 / 2) (#) ((1 / 2) GeoSeq)) . n by A42;
then M . (HP . n) is Real by A44, XXREAL_0:48;
hence ex y being Element of REAL st S₃[n,y] ; :: thesis:

end;

consider me being Real_Sequence such that
A45: for p being Element of NAT holds S₃[p,me . p] from FUNCT_2:sch 10(A43);
A46: for p being Element of NAT holds me . p <= ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p

proof

let p be Element of NAT ; :: thesis:
me . p = M . (HP . p) by A45;
hence me . p <= ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p by A42; :: thesis:

end;

A47: for p being Element of NAT holds
( 0 <= me . p & me . p <= ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p )

proof

let p be Element of NAT ; :: thesis:
0. <= M . (HP . p) by MEASURE1:def 2;
hence ( 0 <= me . p & me . p <= ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p ) by A45, A46; :: thesis:

end;

then A48: me is nonnegative by RINFSUP1:def 3;
deffunc H₂( Element of NAT ) -> M13(X,S) = E \ (LN . $1);
consider ELN being Function of NAT,S such that
A49: for n being Element of NAT holds ELN . n = H₂(n) from FUNCT_2:sch 4();
rng ELN is N_Sub_set_fam of X by MEASURE1:23;
then reconsider RELN = rng ELN as N_Measure_fam of S by MEASURE2:def 1;
A50: E /\ (union (rng HP)) c= union (rng HP) by XBOOLE_1:17;
for A being set st A in RELN holds
A is measure_zero of M

proof

let A be set ; :: thesis:
assume A in RELN ; :: thesis:
then consider n being set such that
A51: n in NAT and
A52: A = ELN . n by FUNCT_2:11;
reconsider n = n as Element of NAT by A51;
M . (ELN . n) = M . (E \ (LN . n)) by A49
.= 0 by A7 ;
hence A is measure_zero of M by A52, MEASURE1:def 7; :: thesis:

end;

then union RELN is measure_zero of M by MEASURE2:14;
then A53: M . (union RELN) = 0. by MEASURE1:def 7;

now

let x be set ; :: thesis:
assume A54: x in E \ (meet (rng LN)) ; :: thesis:
then A55: x in E by XBOOLE_0:def 5;
not x in meet (rng LN) by A54, XBOOLE_0:def 5;
then consider Y being set such that
A56: Y in rng LN and
A57: not x in Y by SETFAM_1:def 1;
consider m being set such that
A58: m in dom LN and
A59: Y = LN . m by A56, FUNCT_1:def 3;
reconsider m = m as Element of NAT by A58;
dom ELN = NAT by FUNCT_2:def 1;
then A60: ELN . m in rng ELN by FUNCT_1:3;
ELN . m = E \ (LN . m) by A49;
then x in ELN . m by A55, A57, A59, XBOOLE_0:def 5;
hence x in union RELN by A60, TARSKI:def 4; :: thesis:

end;

then A61: E \ (meet (rng LN)) c= union RELN by TARSKI:def 3;

now

let x be set ; :: thesis:
assume x in union RELN ; :: thesis:
then consider Y being set such that
A62: x in Y and
A63: Y in RELN by TARSKI:def 4;
consider m being set such that
A64: m in dom ELN and
A65: ELN . m = Y by A63, FUNCT_1:def 3;
reconsider m = m as Element of NAT by A64;
dom LN = NAT by FUNCT_2:def 1;
then A66: LN . m in rng LN by FUNCT_1:3;
A67: Y = E \ (LN . m) by A49, A65;
then not x in LN . m by A62, XBOOLE_0:def 5;
then A68: not x in meet (rng LN) by A66, SETFAM_1:def 1;
x in E by A62, A67, XBOOLE_0:def 5;
hence x in E \ (meet (rng LN)) by A68, XBOOLE_0:def 5; :: thesis:

end;

then union RELN c= E \ (meet (rng LN)) by TARSKI:def 3;
then A69: union RELN = E \ (meet (rng LN)) by A61, XBOOLE_0:def 10;
rng HP is N_Sub_set_fam of X by MEASURE1:23;
then A70: rng HP is N_Measure_fam of S by MEASURE2:def 1;
reconsider MRHP = union (rng HP) as Element of S by MEASURE1:24;
L \ MRHP is Element of S ;
then consider F being Element of S such that
A71: F = L \ (union (rng HP)) ;
E \ L = (E \ (meet (rng LN))) \/ (E \ G) by XBOOLE_1:54;
then M . (E \ L) <= (M . (union RELN)) + (M . (E \ G)) by A69, MEASURE1:33;
then M . (E \ L) <= 0. by A10, A53;
then A72: M . (E \ L) = 0 by MEASURE1:def 2;
reconsider MRHP = union (rng HP) as Element of S by MEASURE1:24;
A73: M . ((E \ L) \/ MRHP) <= (M . (E \ L)) + (M . MRHP) by MEASURE1:33;
E \ F = (E \ L) \/ (E /\ (union (rng HP))) by A71, XBOOLE_1:52;
then M . (E \ F) <= M . ((E \ L) \/ MRHP) by A50, MEASURE1:31, XBOOLE_1:9;
then M . (E \ F) <= (M . (E \ L)) + (M . MRHP) by A73, XXREAL_0:2;
then A74: M . (E \ F) <= M . MRHP by A72, XXREAL_3:4;
dom me = NAT by FUNCT_2:def 1;
then A75: dom me = dom (M * HP) by FUNCT_2:def 1;
A76: for x being set st x in dom me holds
me . x = (M * HP) . x

proof

let x be set ; :: thesis:
assume A77: x in dom me ; :: thesis:
then (M * HP) . x = M . (HP . x) by A75, FUNCT_1:12;
hence me . x = (M * HP) . x by A45, A77; :: thesis:

end;

A78: abs (1 / 2) = 1 / 2 by ABSVALUE:def 1;
then A79: (1 / 2) GeoSeq is summable by SERIES_1:24;
then A80: (e0 / 2) (#) ((1 / 2) GeoSeq) is summable by SERIES_1:10;
then me is summable by A47, SERIES_1:20;
then Sum me = SUM (M * HP) by A48, A75, A76, FUNCT_1:2, PROB_4:12;
then A81: M . (union (rng HP)) <= Sum me by A70, MEASURE2:11;
A82: for q being real number st 0 < q holds
ex p being Element of NAT st ((1 / 2) GeoSeq) . p < q

proof

let q be real number ; :: thesis:
assume A83: 0 < q ; :: thesis:
A84: lim ((1 / 2) GeoSeq) = 0 by A79, SERIES_1:4;
(1 / 2) GeoSeq is convergent by A79, SERIES_1:4;
then consider p being Element of NAT such that
A85: for n being Element of NAT st p <= n holds
abs ((((1 / 2) GeoSeq) . n) - 0) < q by A83, A84, SEQ_2:def 7;
take p ; :: thesis:
0 < (1 / 2) |^ p by PREPOWER:6;
then A86: 0 <= ((1 / 2) GeoSeq) . p by PREPOWER:def 1;
abs ((((1 / 2) GeoSeq) . p) - 0) < q by A85;
hence ((1 / 2) GeoSeq) . p < q by A86, ABSVALUE:def 1; :: thesis:

end;

A87: for x being Element of X st x in F holds
for p being Element of NAT holds x in L \ (HP . p)

proof

let x be Element of X; :: thesis:
assume A88: x in F ; :: thesis:
let p be Element of NAT ; :: thesis:
dom HP = NAT by FUNCT_2:def 1;
then HP . p in rng HP by FUNCT_1:3;
then L \ (union (rng HP)) c= L \ (HP . p) by XBOOLE_1:34, ZFMISC_1:74;
hence x in L \ (HP . p) by A71, A88; :: thesis:

end;

A89: for q being real number st 0 < q holds
ex N being natural number st
for n being natural number st N < n holds
for x being Element of X st x in F holds
|.(((f . n) . x) - (g . x)).| < q

proof

let q be real number ; :: thesis:
assume 0 < q ; :: thesis:
then consider p being Element of NAT such that
A90: ((1 / 2) GeoSeq) . p < q by A82;
consider Np being Element of NAT such that
A91: for k being Element of NAT st Np < k holds
for x being Element of X st x in L \ (HP . p) holds
|.(((fL . k) . x) - ((g | L) . x)).| < ((1 / 2) GeoSeq) . p by A42;
take Np ; :: thesis:

hereby :: thesis:

let n be natural number ; :: thesis:
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
assume A92: Np < n ; :: thesis:

hereby :: thesis:

end;

Sum ((1 / 2) GeoSeq) = 1 / (1 - (1 / 2)) by A78, SERIES_1:24;
then A97: Sum ((e0 / 2) (#) ((1 / 2) GeoSeq)) = (e0 / 2) * 2 by A79, SERIES_1:10;
Sum me <= Sum ((e0 / 2) (#) ((1 / 2) GeoSeq)) by A80, A47, SERIES_1:20;
then M . MRHP <= 2 * (e0 / 2) by A81, A97, XXREAL_0:2;
then A98: M . (E \ F) <= e0 by A74, XXREAL_0:2;
F c= L by A71, XBOOLE_1:36;
hence ex F being Element of S st
( F c= E & M . (E \ F) <= e0 & ( for p being real number st 0 < p holds
ex N being natural number st
for n being natural number st N < n holds
for x being Element of X st x in F holds
|.(((f . n) . x) - (g . x)).| < p ) ) by A19, A98, A89, XBOOLE_1:1; :: thesis: