:: Egoroff's Theorem
:: by Noboru Endou , Yasunari Shidama and Keiko Narita
::
:: Received October 30, 2007
:: Copyright (c) 2007-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, PROB_1, MEASURE1, FUNCT_1, SUBSET_1, XXREAL_0,
ARYTM_3, RELAT_1, SETFAM_1, TARSKI, MEASURE2, ARYTM_1, SETLIM_1, NAT_1,
ORDINAL2, CARD_3, CARD_1, SEQ_2, SEQFUNC, PARTFUN1, PBOOLE, RINFSUP1,
MESFUNC1, XXREAL_2, ZFMISC_1, MESFUNC5, VALUED_0, COMPLEX1, REAL_1,
SUPINF_2, SEQ_1, FUNCOP_1, VALUED_1, PREPOWER, NEWTON, SERIES_1,
MESFUNC8, SEQ_4, XCMPLX_0;
notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS,
XXREAL_3, XCMPLX_0,
XREAL_0, COMPLEX1, XXREAL_0, XXREAL_2, VALUED_0, PROB_1, REAL_1,
SETFAM_1, MEASURE1, KURATO_0, SETLIM_1, MEASURE2, RELAT_1, FUNCT_1,
RELSET_1, PARTFUN1, RFUNCT_3, FUNCT_2, SUPINF_2, RINFSUP1, SEQFUNC,
MEASURE6, VALUED_1, NAT_1, SEQ_1, SEQ_2, SEQ_4, NEWTON, PREPOWER,
SERIES_1, EXTREAL1, MESFUNC1, MESFUNC5, RINFSUP2, CARD_3, FUNCOP_1;
constructors REAL_1, NAT_1, EXTREAL1, NEWTON, PREPOWER, SERIES_1, MESFUNC1,
PROB_2, MEASURE6, MEASURE3, PARTFUN3, KURATO_0, RINFSUP1, SETLIM_1,
MESFUNC5, RINFSUP2, SUPINF_1, SEQFUNC, SEQ_4, RELSET_1, BINOP_2, RVSUM_1,
COMSEQ_2;
registrations SUBSET_1, XREAL_0, MEMBERED, ORDINAL1, PARTFUN1, FUNCT_2,
RELAT_1, XXREAL_0, XBOOLE_0, FUNCT_1, NUMBERS, VALUED_0, VALUED_1,
SETLIM_1, SEQ_4, NAT_1, XXREAL_3, RELSET_1, NEWTON, SEQ_2;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XXREAL_2;
equalities CARD_3, FUNCT_6, RINFSUP1, SETLIM_1, XCMPLX_0, RINFSUP2, VALUED_1,
XXREAL_3;
expansions TARSKI, CARD_3, RINFSUP1, XXREAL_2;
theorems ABSVALUE, MEASURE1, MEASURE2, MEASURE3, NAT_1, TARSKI, PARTFUN1,
FUNCT_1, FUNCT_2, KURATO_0, SUPINF_2, EXTREAL1, SETFAM_1, SEQ_1, SEQ_2,
SEQM_3, SEQ_4, SERIES_1, RINFSUP1, MESFUNC1, XREAL_0, PROB_1, XBOOLE_0,
XBOOLE_1, MESFUNC2, XREAL_1, PREPOWER, XXREAL_0, ZFMISC_1, SETLIM_1,
PROB_4, PARTFUN2, ORDINAL1, MESFUNC5, RINFSUP2, XXREAL_2, VALUED_0,
FUNCOP_1, XXREAL_3, RELAT_1;
schemes FUNCT_2, SEQFUNC, PARTFUN2;
begin
reserve n,k for Nat,
X for non empty set,
S for SigmaField of X;
theorem Th1:
for M be sigma_Measure of S, F be sequence of S, n holds
{x where x is Element of X : for k st n <= k holds x in F.k}
is Element of S
proof
let M be sigma_Measure of S, F be sequence of S, n;
set G = {x where x is Element of X : for k st n <= k holds x in F.k};
deffunc Fn(Element of NAT) = F.(n+$1);
consider E be sequence of S such that
A1: for k be Element of NAT holds E.k=Fn(k) from FUNCT_2:sch 4;
now
let z be object;
assume z in G; then
A2: ex x be Element of X st z=x & for k be Nat st n <= k holds
x in F.k;
for Y be set st Y in rng E holds z in Y
proof
let Y be set;
assume Y in rng E;
then consider l be object such that
A3: l in NAT and
A4: Y=E.l by FUNCT_2:11;
reconsider l as Element of NAT by A3;
z in F.(n+l) by A2,NAT_1:12;
hence thesis by A1,A4;
end;
hence z in meet rng E by SETFAM_1:def 1;
end; then
A5: G c= meet rng E;
rng E is N_Sub_set_fam of X by MEASURE1:23;
then rng E is N_Measure_fam of S by MEASURE2:def 1; then
A6: meet rng E is Element of S by MEASURE2:2;
now
let z be object;
assume
A7: z in meet rng E;
now
let k be Nat;
assume n <= k;
then reconsider l=k-n as Element of NAT by NAT_1:21;
E.l in rng E by FUNCT_2:4;
then z in E.l by A7,SETFAM_1:def 1;
then z in F.(n+l) by A1;
hence z in F.k;
end;
hence z in G by A6,A7;
end;
then meet rng E c= G;
hence thesis by A6,A5,XBOOLE_0:def 10;
end;
theorem Th2:
for F be SetSequence of X, n be Nat holds
(superior_setsequence F).n = union rng (F^\n) &
(inferior_setsequence F).n = meet rng (F^\n)
proof
let F be SetSequence of X, n be Nat;
{F.k where k is Nat: n <= k} = rng (F^\n) by SETLIM_1:6;
hence (superior_setsequence F).n = union rng (F ^\ n) by SETLIM_1:def 3;
(inferior_setsequence F).n = meet({F.k where k: n <= k}) by SETLIM_1:def 2;
hence thesis by SETLIM_1:6;
end;
theorem Th3:
for M be sigma_Measure of S, F be SetSequence of S
ex G be sequence of S st
G = inferior_setsequence F & M.(lim_inf F) = sup rng(M*G)
proof
let M be sigma_Measure of S, F be SetSequence of S;
rng inferior_setsequence F c= S;
then reconsider G = inferior_setsequence(F) as sequence of S by FUNCT_2:6;
for n being Nat holds G.n c= G.(n+1) by PROB_1:def 5,NAT_1:12;
then M.(union rng G)= sup rng(M*G) by MEASURE2:23;
hence thesis;
end;
theorem Th4:
for M be sigma_Measure of S, F be SetSequence of S st
M.(Union F) < +infty holds
ex G be sequence of S st G= superior_setsequence F &
M.(lim_sup F) = inf rng(M*G)
proof
let M be sigma_Measure of S, F be SetSequence of S;
rng superior_setsequence F c= S;
then reconsider G= superior_setsequence F as sequence of S by FUNCT_2:6;
reconsider F1 = F, G1 = G as SetSequence of X;
A1: for n being Nat holds G.(n+1) c= G.n by NAT_1:12,PROB_1:def 4;
G.0 = union {F.k where k: 0 <= k} by SETLIM_1:def 3; then
A2: G.0 = union rng F by SETLIM_1:5;
consider f being SetSequence of X such that
A3: lim_sup F1 = meet f and
A4: for n being Nat holds f.n = Union (F1^\n) by KURATO_0:def 2;
now
let n be Element of NAT;
f.n = Union (F1^\n) by A4;
hence f.n = G1.n by Th2;
end; then
A5: f = G1 by FUNCT_2:63;
assume M.(Union F) < +infty;
then M.(meet rng G)= inf rng(M*G) by A1,A2,MEASURE3:12;
hence thesis by A3,A5;
end;
theorem
for M be sigma_Measure of S, F be SetSequence of S st F is convergent
holds ex G be sequence of S st
G = inferior_setsequence F & M.(lim F) = sup rng (M*G)
proof
let M be sigma_Measure of S, F be SetSequence of S;
assume F is convergent;
then lim_inf F = lim F by KURATO_0:def 5;
hence thesis by Th3;
end;
theorem
for M be sigma_Measure of S, F be SetSequence of S st F is convergent
& M.(Union F) < +infty holds ex G be sequence of S st
G = superior_setsequence F & M.(lim F) = inf rng(M*G) by Th4;
definition
let X,Y be set, F be Functional_Sequence of X,Y;
attr F is with_the_same_dom means
rng F is with_common_domain;
end;
definition
let X,Y be set, F be Functional_Sequence of X,Y;
redefine attr F is with_the_same_dom means :: redefines with_the_same_dom (MESFUNC8, definition)
:Def2:
for n,m be Nat holds dom(F.n) = dom(F.m);
correctness
proof
A1: (for n,m be Nat holds dom(F.n) = dom(F.m)) implies F is with_the_same_dom
proof
assume
A2: for n,m be Nat holds dom(F.n)=dom(F.m);
now
let f,g be Function;
assume that
A3: f in rng F and
A4: g in rng F;
consider m be object such that
A5: m in dom F and
A6: g = F.m by A4,FUNCT_1:def 3;
consider n be object such that
A7: n in dom F and
A8: f = F.n by A3,FUNCT_1:def 3;
reconsider n,m as Nat by A7,A5;
dom(F.n) = dom(F.m) by A2;
hence dom f = dom g by A8,A6;
end;
then rng F is with_common_domain;
hence thesis;
end;
F is with_the_same_dom implies for n,m be Nat holds dom(F.n) = dom(F.m)
proof
assume F is with_the_same_dom; then
A9: rng F is with_common_domain;
hereby
let n,m be Nat;
A10: dom F = NAT by FUNCT_2:def 1;
then m in dom F by ORDINAL1:def 12; then
A11: F.m in rng F by FUNCT_1:3;
n in dom F by A10,ORDINAL1:def 12;
then F.n in rng F by FUNCT_1:3;
hence dom(F.n) = dom(F.m) by A9,A11;
end;
end;
hence thesis by A1;
end;
end;
registration
let X,Y be set;
cluster with_the_same_dom for Functional_Sequence of X,Y;
existence
proof
deffunc f(Nat) = <:{},X,Y:>;
consider F be Functional_Sequence of X,Y such that
A1: for n be Nat holds F.n = f(n) from SEQFUNC:sch 1;
take F;
hereby
let n,m be Nat;
F.n = <:{},X,Y:> by A1;
hence dom(F.n) = dom(F.m) by A1;
end;
end;
end;
definition
let X be non empty set, f be Functional_Sequence of X,ExtREAL;
func inf f -> PartFunc of X,ExtREAL means
:Def3:
dom it = dom(f.0) &
for x be Element of X st x in dom it holds it.x = inf(f#x);
existence
proof
defpred P[set] means $1 in dom(f.0);
deffunc F(Element of X) = inf (f#$1);
consider g being PartFunc of X,ExtREAL such that
A1: (for x be Element of X holds x in dom g iff P[x]) & for x be
Element of X st x in dom g holds g/.x = F(x) from PARTFUN2:sch 2;
take g;
A2: now
let x be Element of X;
assume
A3: x in dom g;
then g/.x = inf (f#x) by A1;
hence g.x = inf (f#x) by A3,PARTFUN1:def 6;
end;
for x be object holds x in dom g iff x in dom(f.0) by A1;
hence thesis by A2,TARSKI:2;
end;
uniqueness
proof
let g,h be PartFunc of X,ExtREAL;
assume that
A4: dom g = dom (f.0) and
A5: for x be Element of X st x in dom g holds g.x=inf(f#x);
assume that
A6: dom h = dom (f.0) and
A7: for x be Element of X st x in dom h holds h.x=inf(f#x);
now
let x be Element of X;
assume
A8: x in dom g;
then g/.x = g.x by PARTFUN1:def 6;
then g/.x = inf(f#x) by A5,A8;
then g/.x = h.x by A4,A6,A7,A8;
hence g/.x = h/.x by A4,A6,A8,PARTFUN1:def 6;
end;
hence thesis by A4,A6,PARTFUN2:1;
end;
end;
definition
let X be non empty set, f be Functional_Sequence of X,ExtREAL;
func sup f -> PartFunc of X,ExtREAL means
:Def4:
dom it = dom(f.0) &
for x be Element of X st x in dom it holds it.x = sup(f#x);
existence
proof
defpred P[set] means $1 in dom(f.0);
deffunc F(Element of X) = sup(f#$1);
consider g being PartFunc of X,ExtREAL such that
A1: (for x be Element of X holds x in dom g iff P[x]) & for x be
Element of X st x in dom g holds g/.x = F(x) from PARTFUN2:sch 2;
take g;
A2: now
let x be Element of X;
assume
A3: x in dom g;
then g/.x =sup (f#x) by A1;
hence g.x =sup (f#x) by A3,PARTFUN1:def 6;
end;
for x be object holds x in dom g iff x in dom(f.0) by A1;
hence thesis by A2,TARSKI:2;
end;
uniqueness
proof
let g,h be PartFunc of X,ExtREAL;
assume that
A4: dom g = dom(f.0) and
A5: for x be Element of X st x in dom g holds g.x=sup(f#x);
assume that
A6: dom h = dom(f.0) and
A7: for x be Element of X st x in dom h holds h.x=sup(f#x);
now
let x be Element of X;
assume
A8: x in dom g;
then g/.x = g.x by PARTFUN1:def 6;
then g/.x = sup(f#x) by A5,A8;
then g/.x = h.x by A4,A6,A7,A8;
hence g/.x = h/.x by A4,A6,A8,PARTFUN1:def 6;
end;
hence thesis by A4,A6,PARTFUN2:1;
end;
end;
definition
let X be non empty set, f be Functional_Sequence of X,ExtREAL;
func inferior_realsequence f -> with_the_same_dom Functional_Sequence of X,
ExtREAL means
:Def5:
for n be Nat holds dom(it.n) = dom(f.0) &
for x be Element of X st x in dom(it.n) holds
(it.n).x=(inferior_realsequence(f#x)).n;
existence
proof
defpred P[Element of NAT,Function] means dom $2 = dom(f.0) & for x be
Element of X st x in dom $2 holds $2.x=(inferior_realsequence(f#x)).$1;
A1: for n being Element of NAT ex y being Element of PFuncs(X,ExtREAL) st
P[n,y]
proof
defpred P[set] means $1 in dom(f.0);
let n being Element of NAT;
deffunc F(Element of X) = (inferior_realsequence(f#$1)).n;
consider g being PartFunc of X,ExtREAL such that
A2: (for x be Element of X holds x in dom g iff P[x]) & for x be
Element of X st x in dom g holds g/.x = F(x) from PARTFUN2:sch 2;
take g;
A3: now
let x be Element of X;
assume
A4: x in dom g;
then g/.x =(inferior_realsequence (f#x)).n by A2;
hence g.x =(inferior_realsequence (f#x)).n by A4,PARTFUN1:def 6;
end;
for x be object holds x in dom g iff x in dom(f.0) by A2;
hence thesis by A3,PARTFUN1:45,TARSKI:2;
end;
consider g being sequence of PFuncs(X,ExtREAL) such that
A5: for n being Element of NAT holds P[n,g.n] from FUNCT_2:sch 3(A1);
A6: for n holds dom(g.n) = dom(f.0) & for x be Element of X st x in dom(g
.n) holds (g.n).x = (inferior_realsequence(f#x)).n
proof
let n;
reconsider n9=n as Element of NAT by ORDINAL1:def 12;
dom(g.n9) = dom(f.0) by A5;
hence thesis by A5;
end;
reconsider g as Functional_Sequence of X,ExtREAL;
now
let k,l be Nat;
reconsider k9=k, l9=l as Element of NAT by ORDINAL1:def 12;
dom(g.k9) = dom(f.0) by A5;
then dom(g.k) = dom(g.l9) by A5;
hence dom(g.k) = dom(g.l);
end;
then reconsider
g as with_the_same_dom Functional_Sequence of X,ExtREAL by Def2;
take g;
thus thesis by A6;
end;
uniqueness
proof
let g,h be with_the_same_dom Functional_Sequence of X,ExtREAL;
assume
A7: for n be Nat holds dom (g.n) = dom (f.0) &
for x be Element of X st x in dom (g.n) holds
(g.n).x=(inferior_realsequence(f#x)).n;
assume
A8: for n be Nat holds dom (h.n) = dom (f.0) & for x be
Element of X st x in dom (h.n) holds (h.n).x=(inferior_realsequence(f#x)).n;
now
let n be Element of NAT;
A9: dom(g.n) = dom(f.0) by A7
.=dom(h.n) by A8;
now
let x be Element of X;
assume
A10: x in dom (g.n);
then (g.n)/.x = (g.n).x by PARTFUN1:def 6;
then (g.n)/.x = (inferior_realsequence (f#x)).n by A7,A10;
then (g.n)/.x = (h.n).x by A8,A9,A10;
hence (g.n)/.x = (h.n)/.x by A9,A10,PARTFUN1:def 6;
end;
hence g.n=h.n by A9,PARTFUN2:1;
end;
hence thesis by FUNCT_2:63;
end;
end;
definition
let X be non empty set, f be Functional_Sequence of X,ExtREAL;
func superior_realsequence f -> with_the_same_dom Functional_Sequence of X,
ExtREAL means
:Def6:
for n be Nat holds dom(it.n) = dom(f.0) &
for x be Element of X st x in dom(it.n) holds
(it.n).x = (superior_realsequence(f#x))
.n;
existence
proof
defpred P[Element of NAT,Function] means dom $2 = dom(f.0) & for x be
Element of X st x in dom $2 holds $2.x=(superior_realsequence(f#x)).$1;
A1: for n being Element of NAT ex y being Element of PFuncs(X,ExtREAL) st
P[n, y]
proof
defpred P[set] means $1 in dom(f.0);
let n being Element of NAT;
deffunc F(Element of X) = (superior_realsequence(f#$1)).n;
consider g being PartFunc of X,ExtREAL such that
A2: (for x be Element of X holds x in dom g iff P[x]) & for x be
Element of X st x in dom g holds g/.x = F(x) from PARTFUN2:sch 2;
take g;
A3: now
let x be Element of X;
assume
A4: x in dom g;
then g/.x =(superior_realsequence(f#x)).n by A2;
hence g.x =(superior_realsequence(f#x)).n by A4,PARTFUN1:def 6;
end;
for x be object holds x in dom g iff x in dom(f.0) by A2;
hence thesis by A3,PARTFUN1:45,TARSKI:2;
end;
consider g being sequence of PFuncs(X,ExtREAL) such that
A5: for n being Element of NAT holds P[n,g.n] from FUNCT_2:sch 3(A1);
A6: for n holds dom(g.n) = dom(f.0) & for x be Element of X st x in dom(g
.n) holds (g.n).x = (superior_realsequence(f#x)).n
proof
let n;
reconsider n9=n as Element of NAT by ORDINAL1:def 12;
dom(g.n9) = dom(f.0) by A5;
hence thesis by A5;
end;
reconsider g as Functional_Sequence of X,ExtREAL;
now
let k,l be Nat;
reconsider k9=k, l9=l as Element of NAT by ORDINAL1:def 12;
dom(g.k9) = dom(f.0) by A5;
then dom(g.k) = dom(g.l9) by A5;
hence dom(g.k) = dom(g.l);
end;
then reconsider
g as with_the_same_dom Functional_Sequence of X,ExtREAL by Def2;
take g;
thus thesis by A6;
end;
uniqueness
proof
let g,h be with_the_same_dom Functional_Sequence of X,ExtREAL;
assume
A7: for n holds dom (g.n) = dom (f.0) & for x be Element of X st x in
dom (g.n) holds (g.n).x=(superior_realsequence(f#x)).n;
assume
A8: for n holds dom (h.n) = dom (f.0) & for x be Element of X st x in
dom (h.n) holds (h.n).x=(superior_realsequence(f#x)).n;
now
let n be Element of NAT;
A9: dom(g.n) = dom(f.0) by A7
.=dom(h.n) by A8;
now
let x be Element of X;
assume
A10: x in dom (g.n);
then (g.n)/.x =(g.n).x by PARTFUN1:def 6;
then (g.n)/.x =(superior_realsequence(f#x)).n by A7,A10;
then (g.n)/.x =(h.n).x by A8,A9,A10;
hence (g.n)/.x =(h.n)/.x by A9,A10,PARTFUN1:def 6;
end;
hence g.n=h.n by A9,PARTFUN2:1;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem Th7:
for f be Functional_Sequence of X,ExtREAL holds
for x be Element of X st x in dom (f.0) holds
(inferior_realsequence f)#x = inferior_realsequence(f#x)
proof
let f be Functional_Sequence of X,ExtREAL;
set F = inferior_realsequence f;
hereby
let x be Element of X;
assume
A1: x in dom (f.0);
now
let n be Element of NAT;
A2: (F#x).n = (F.n).x by MESFUNC5:def 13;
dom(F.n) = dom (f.0) by Def5;
hence (F#x).n =(inferior_realsequence (f#x)).n by A1,A2,Def5;
end;
hence F#x = inferior_realsequence(f#x) by FUNCT_2:63;
end;
end;
registration
let X,Y be set;
let f be with_the_same_dom Functional_Sequence of X,Y;
let n be Nat;
cluster f^\n -> with_the_same_dom for Functional_Sequence of X,Y;
coherence
proof
for k,l be Nat holds dom((f^\n).k)=dom((f^\n).l)
proof
reconsider g=f as sequence of PFuncs(X,Y);
let k,l be Nat;
reconsider k9=k, l9=l as Element of NAT by ORDINAL1:def 12;
dom((f^\n).k) = dom((g.(n+k9))) by NAT_1:def 3;
then dom((f^\n).k) = dom((g.(n+l9))) by Def2;
hence thesis by NAT_1:def 3;
end;
hence thesis;
end;
end;
theorem Th8:
for f be with_the_same_dom Functional_Sequence of X,ExtREAL,
n be Nat holds (inferior_realsequence f).n = inf(f^\n)
proof
let f be with_the_same_dom Functional_Sequence of X,ExtREAL, n be Nat;
reconsider g=f as sequence of PFuncs(X,ExtREAL);
dom inf(f^\n) =dom((f^\n).0) by Def3;
then dom inf(f^\n) =dom(g.(n+(0 qua Nat))) by NAT_1:def 3;
then
A1: dom inf(f^\n) =dom(f.0) by Def2;
A2: dom((inferior_realsequence f).n) = dom(f.0) by Def5;
now
let x be Element of X;
assume
A3: x in dom inf(f^\n);
now
let k be Element of NAT;
((f^\n)#x).k =((f^\n).k).x by MESFUNC5:def 13;
then ((f^\n)#x).k =(g.(n+k)).x by NAT_1:def 3;
then ((f^\n)#x).k =(f#x).(n+k) by MESFUNC5:def 13;
hence ((f^\n)#x).k = ((f#x)^\n).k by NAT_1:def 3;
end;
then (f^\n)#x = (f#x)^\n by FUNCT_2:63;
then
A4: (inf(f^\n)).x =inf((f#x)^\n) by A3,Def3;
((inferior_realsequence f).n ).x = (inferior_realsequence(f#x)).n by A2,A1
,A3,Def5;
hence (inf(f^\n)).x = ((inferior_realsequence f).n).x by A4,RINFSUP2:27;
end;
hence thesis by A2,A1,PARTFUN1:5;
end;
theorem Th9:
for f be with_the_same_dom Functional_Sequence of X,ExtREAL,
n be Nat holds (superior_realsequence f).n = sup(f^\n)
proof
let f be with_the_same_dom Functional_Sequence of X,ExtREAL, n be Nat;
reconsider g=f as sequence of PFuncs(X,ExtREAL);
dom sup(f^\n) = dom((f^\n).0) by Def4;
then dom sup(f^\n) = dom(g.(n+(0 qua Nat))) by NAT_1:def 3;
then
A1: dom sup(f^\n) = dom(f.0) by Def2;
A2: dom ((superior_realsequence f).n) = dom(f.0) by Def6;
now
let x be Element of X;
assume
A3: x in dom sup(f^\n);
now
let k be Element of NAT;
((f^\n)#x).k =((f^\n).k).x by MESFUNC5:def 13;
then ((f^\n)#x).k =(g.(n+k)).x by NAT_1:def 3;
then ((f^\n)#x).k =(f#x).(n+k) by MESFUNC5:def 13;
hence ((f^\n)#x).k = ((f#x)^\n).k by NAT_1:def 3;
end;
then (f^\n)#x = (f#x)^\n by FUNCT_2:63;
then
A4: (sup(f^\n)).x =sup ((f#x)^\n) by A3,Def4;
((superior_realsequence f).n ).x = (superior_realsequence (f#x)).n by A2,A1
,A3,Def6;
hence (sup (f^\n)).x = ((superior_realsequence f).n ).x by A4,RINFSUP2:27;
end;
hence thesis by A2,A1,PARTFUN1:5;
end;
theorem Th10:
for f be Functional_Sequence of X,ExtREAL, x be Element of X st
x in dom(f.0) holds (superior_realsequence f)#x = superior_realsequence(f#x)
proof
let f be Functional_Sequence of X,ExtREAL, x be Element of X;
set F = superior_realsequence f;
assume
A1: x in dom(f.0);
now
let n be Element of NAT;
A2: (F#x).n = (F.n).x by MESFUNC5:def 13;
dom(F.n) = dom(f.0) by Def6;
hence (F#x).n =(superior_realsequence(f#x)).n by A1,A2,Def6;
end;
hence thesis by FUNCT_2:63;
end;
definition
let X be non empty set, f be Functional_Sequence of X,ExtREAL;
func lim_inf f -> PartFunc of X,ExtREAL means
:Def7:
dom it = dom (f.0) &
for x be Element of X st x in dom it holds it.x = lim_inf(f#x);
existence
proof
defpred P[set] means $1 in dom(f.0);
deffunc F(Element of X) = lim_inf(f#$1);
consider g being PartFunc of X,ExtREAL such that
A1: (for x be Element of X holds x in dom g iff P[x]) & for x be
Element of X st x in dom g holds g/.x = F(x) from PARTFUN2:sch 2;
take g;
A2: now
let x be Element of X;
assume
A3: x in dom g;
then g/.x =lim_inf(f#x) by A1;
hence g.x =lim_inf(f#x) by A3,PARTFUN1:def 6;
end;
for x be object holds x in dom g iff x in dom(f.0) by A1;
hence thesis by A2,TARSKI:2;
end;
uniqueness
proof
let g,h be PartFunc of X,ExtREAL;
assume that
A4: dom g = dom(f.0) and
A5: for x be Element of X st x in dom g holds g.x=lim_inf(f#x) and
A6: dom h = dom(f.0) and
A7: for x be Element of X st x in dom h holds h.x=lim_inf(f#x);
now
let x be Element of X;
assume
A8: x in dom g;
then g/.x =g.x by PARTFUN1:def 6;
then g/.x =lim_inf (f#x) by A5,A8;
then g/.x =h.x by A4,A6,A7,A8;
hence g/.x =h/.x by A4,A6,A8,PARTFUN1:def 6;
end;
hence thesis by A4,A6,PARTFUN2:1;
end;
end;
definition
let X be non empty set, f be Functional_Sequence of X,ExtREAL;
func lim_sup f -> PartFunc of X,ExtREAL means
:Def8:
dom it = dom (f.0) &
for x be Element of X st x in dom it holds it.x = lim_sup(f#x);
existence
proof
defpred P[set] means $1 in dom(f.0);
deffunc F(Element of X) = lim_sup(f#$1);
consider g being PartFunc of X,ExtREAL such that
A1: (for x be Element of X holds x in dom g iff P[x]) & for x be
Element of X st x in dom g holds g/.x = F(x) from PARTFUN2:sch 2;
take g;
A2: now
let x be Element of X;
assume
A3: x in dom g;
then g/.x =lim_sup(f#x) by A1;
hence g.x =lim_sup(f#x) by A3,PARTFUN1:def 6;
end;
for x be object holds x in dom g iff x in dom(f.0) by A1;
hence thesis by A2,TARSKI:2;
end;
uniqueness
proof
let g,h be PartFunc of X,ExtREAL;
assume that
A4: dom g = dom(f.0) and
A5: for x be Element of X st x in dom g holds g.x=lim_sup(f#x);
assume that
A6: dom h = dom(f.0) and
A7: for x be Element of X st x in dom h holds h.x=lim_sup(f#x);
now
let x be Element of X;
assume
A8: x in dom g;
then g/.x = g.x by PARTFUN1:def 6;
then g/.x = lim_sup (f#x) by A5,A8;
then g/.x = h.x by A4,A6,A7,A8;
hence g/.x = h/.x by A4,A6,A8,PARTFUN1:def 6;
end;
hence thesis by A4,A6,PARTFUN2:1;
end;
end;
theorem Th11:
for f be Functional_Sequence of X,ExtREAL holds
(for x be Element of X st x in dom lim_inf f holds
(lim_inf f).x=sup inferior_realsequence(f#x) &
(lim_inf f).x=sup ((inferior_realsequence f)#x) &
(lim_inf f).x=sup (inferior_realsequence f).x) &
lim_inf f = sup inferior_realsequence f
proof
let f be Functional_Sequence of X,ExtREAL;
dom(sup inferior_realsequence f) =dom((inferior_realsequence f).0) by Def4;
then dom(sup inferior_realsequence f) = dom(f.0) by Def5;
then
A1: dom(sup inferior_realsequence f) = dom(lim_inf f) by Def7;
A2: now
let x be Element of X;
assume
A3: x in dom lim_inf f; then
A4: (lim_inf f).x=lim_inf(f#x) by Def7;
hence (lim_inf f).x= sup inferior_realsequence(f#x);
dom lim_inf f = dom(f.0) by Def7;
hence (lim_inf f).x = sup((inferior_realsequence f)#x) by A3,A4,Th7;
hence (lim_inf f).x =(sup inferior_realsequence f).x by A1,A3,Def4;
end;
then for x be Element of X st x in dom lim_inf f holds (lim_inf f).x =(sup
inferior_realsequence f).x;
hence thesis by A1,A2,PARTFUN1:5;
end;
theorem Th12:
for f be Functional_Sequence of X,ExtREAL holds
(for x be Element of X st x in dom lim_sup f holds
(lim_sup f).x=inf superior_realsequence(f#x) &
(lim_sup f).x=inf ((superior_realsequence f)#x) &
(lim_sup f).x=inf (superior_realsequence f).x ) &
lim_sup f = inf superior_realsequence f
proof
let f be Functional_Sequence of X,ExtREAL;
A1: dom(inf superior_realsequence f) =dom((superior_realsequence f).0) by Def3
.=dom(f.0) by Def6
.=dom lim_sup f by Def8;
A2: now
let x be Element of X;
assume
A3: x in dom lim_sup f; then
A4: (lim_sup f).x=lim_sup (f#x) by Def8;
hence (lim_sup f).x = inf superior_realsequence(f#x);
dom lim_sup f = dom(f.0) by Def8;
hence (lim_sup f).x = inf((superior_realsequence f)#x) by A3,A4,Th10;
hence (lim_sup f).x = (inf superior_realsequence f).x by A1,A3,Def3;
end;
then for x be Element of X st x in dom lim_sup f holds (lim_sup f).x =(inf
superior_realsequence f).x;
hence thesis by A1,A2,PARTFUN1:5;
end;
theorem
for f be Functional_Sequence of X,ExtREAL, x be Element of X st
x in dom (f.0) holds f#x is convergent iff (lim_sup f).x = (lim_inf f).x
proof
let f be Functional_Sequence of X,ExtREAL, x be Element of X;
assume
A1: x in dom(f.0);
then x in dom(lim_inf f) by Def7;
then
A2: (lim_inf f).x = lim_inf (f#x) by Def7;
x in dom(lim_sup f) by A1,Def8;
then (lim_sup f).x = lim_sup (f#x) by Def8;
hence thesis by A2,RINFSUP2:40;
end;
definition
let X be non empty set, f be Functional_Sequence of X,ExtREAL;
func lim f -> PartFunc of X,ExtREAL means :Def9:
dom it = dom (f.0) & for x
be Element of X st x in dom it holds it.x=lim(f#x);
existence
proof
defpred P[set] means $1 in dom(f.0);
deffunc F(Element of X) = lim (f#$1);
consider g being PartFunc of X,ExtREAL such that
A1: (for x be Element of X holds x in dom g iff P[x]) & for x be
Element of X st x in dom g holds g/.x = F(x) from PARTFUN2:sch 2;
take g;
A2: now
let x be Element of X;
assume
A3: x in dom g;
then g/.x =lim(f#x) by A1;
hence g.x =lim(f#x) by A3,PARTFUN1:def 6;
end;
for x be object holds x in dom g iff x in dom(f.0) by A1;
hence thesis by A2,TARSKI:2;
end;
uniqueness
proof
let g,h be PartFunc of X,ExtREAL;
assume that
A4: dom g = dom (f.0) and
A5: for x be Element of X st x in dom g holds g.x=lim(f#x);
assume that
A6: dom h = dom (f.0) and
A7: for x be Element of X st x in dom h holds h.x=lim(f#x);
now
let x be Element of X;
assume
A8: x in dom g;
then g/.x = g.x by PARTFUN1:def 6;
then g/.x = lim (f#x) by A5,A8;
then g/.x = h.x by A4,A6,A7,A8;
hence g/.x = h/.x by A4,A6,A8,PARTFUN1:def 6;
end;
hence thesis by A4,A6,PARTFUN2:1;
end;
end;
theorem Th14:
for f be Functional_Sequence of X,ExtREAL, x be Element of X st
x in dom lim f & f#x is convergent holds
(lim f).x = (lim_sup f).x &
(lim f).x = (lim_inf f).x
proof
let f be Functional_Sequence of X,ExtREAL;
let x be Element of X;
assume that
A1: x in dom lim f and
A2: f#x is convergent;
A3: lim (f#x) = lim_inf (f#x) by A2,RINFSUP2:41;
A4: x in dom (f.0) by A1,Def9;
then x in dom(lim_sup f) by Def8; then
A5: (lim_sup f).x = lim_sup (f#x) by Def8;
x in dom(lim_inf f) by A4,Def7; then
A6: (lim_inf f).x = lim_inf (f#x) by Def7;
lim (f#x) = lim_sup (f#x) by A2,RINFSUP2:41;
hence thesis by A1,A5,A6,A3,Def9;
end;
theorem Th15:
for f be with_the_same_dom Functional_Sequence of X,ExtREAL,
F be SetSequence of S, r be Real st
(for n be Nat holds F.n = dom(f.0) /\ great_dom(f.n,r)) holds
union rng F = dom(f.0) /\ great_dom(sup f,r)
proof
let f be with_the_same_dom Functional_Sequence of X,ExtREAL,
F be SetSequence of S, r be Real;
set E = dom(f.0);
assume
A1: for n be Nat holds F.n = E /\ great_dom(f.n,r);
now
let x be object;
assume
A2: x in E /\ great_dom(sup f,r);
then reconsider z=x as Element of X;
A3: x in E by A2,XBOOLE_0:def 4;
x in great_dom(sup f,r) by A2,XBOOLE_0:def 4;
then
A4: r < (sup f).z by MESFUNC1:def 13;
ex n be Element of NAT st r < (f.n).z
proof
assume
A5: for n be Element of NAT holds (f.n).z <= r;
for x be ExtReal st x in rng (f#z) holds x <= r
proof
let x be ExtReal;
assume x in rng (f#z);
then consider m be object such that
A6: m in NAT and
A7: x=(f#z).m by FUNCT_2:11;
reconsider m as Element of NAT by A6;
x=(f.m).z by A7,MESFUNC5:def 13;
hence thesis by A5;
end;
then r is UpperBound of rng (f#z) by XXREAL_2:def 1;
then
A8: sup (f#z) <= r by XXREAL_2:def 3;
x in dom (sup f) by A3,Def4;
hence contradiction by A4,A8,Def4;
end;
then consider n be Element of NAT such that
A9: r < (f.n).z;
x in dom (f.n) by A3,Def2;
then
A10: x in great_dom(f.n,r) by A9,MESFUNC1:def 13;
A11: F.n in rng F by FUNCT_2:4;
A12: F.n = E /\ great_dom(f.n,r) by A1;
x in E by A2,XBOOLE_0:def 4;
then x in F.n by A10,A12,XBOOLE_0:def 4;
hence x in union rng F by A11,TARSKI:def 4;
end;
then
A13: E /\ great_dom((sup f),r) c= union rng F;
now
let x be object;
assume x in union rng F;
then consider y be set such that
A14: x in y and
A15: y in rng(F qua SetSequence of X) by TARSKI:def 4;
reconsider z=x as Element of X by A14,A15;
consider n be object such that
A16: n in dom F and
A17: y=F.n by A15,FUNCT_1:def 3;
reconsider n as Element of NAT by A16;
A18: F.n = E /\ great_dom(f.n,r) by A1;
then x in great_dom(f.n,r) by A14,A17,XBOOLE_0:def 4;
then
A19: r < (f.n).z by MESFUNC1:def 13;
A20: (f.n).z=(f#z).n by MESFUNC5:def 13;
A21: x in E by A14,A17,A18,XBOOLE_0:def 4;
then
A22: x in dom (sup f) by Def4;
then (sup f).z = sup(f#z) by Def4;
then (f.n).z <= (sup f).z by A20,RINFSUP2:23;
then r < (sup f).z by A19,XXREAL_0:2;
then x in great_dom(sup f,r) by A22,MESFUNC1:def 13;
hence x in E /\ great_dom(sup f,r) by A21,XBOOLE_0:def 4;
end;
then union rng F c= E /\ great_dom(sup f,r);
hence thesis by A13,XBOOLE_0:def 10;
end;
theorem Th16:
for f be with_the_same_dom Functional_Sequence of X,ExtREAL,
F be SetSequence of S, r be Real st
(for n be Nat holds F.n = dom(f.0) /\ great_eq_dom(f.n,r)) holds
meet rng F = dom(f.0) /\ great_eq_dom(inf f,r)
proof
let f be with_the_same_dom Functional_Sequence of X,ExtREAL,
F be SetSequence of S, r be Real;
set E = dom(f.0);
assume
A1: for n be Nat holds F.n = dom(f.0) /\ great_eq_dom(f.n, r);
now
let x be object;
assume
A2: x in meet rng(F qua SetSequence of X);
then reconsider z=x as Element of X;
A3: F.0 = E /\ great_eq_dom(f.0,r) by A1;
F.0 in rng F by FUNCT_2:4;
then x in F.0 by A2,SETFAM_1:def 1;
then
A4: x in E by A3,XBOOLE_0:def 4; then
A5: x in dom inf f by Def3;
A6: now
let n be Element of NAT;
F.n in rng F by FUNCT_2:4; then
A7: z in F.n by A2,SETFAM_1:def 1;
F.n = E /\ great_eq_dom(f.n,r) by A1;
then x in great_eq_dom(f.n,r) by A7,XBOOLE_0:def 4;
then r <= (f.n).z by MESFUNC1:def 14;
hence r <= (f#z).n by MESFUNC5:def 13;
end;
now
let s be ExtReal;
assume s in rng (f#z);
then ex k be object st k in NAT & s=(f#z).k by FUNCT_2:11;
hence r <= s by A6;
end;
then r is LowerBound of rng (f#z) by XXREAL_2:def 2;
then r <= inf (f#z) by XXREAL_2:def 4;
then r <= (inf f).x by A5,Def3;
then x in great_eq_dom(inf f,r) by A5,MESFUNC1:def 14;
hence x in E /\ great_eq_dom(inf f,r) by A4,XBOOLE_0:def 4;
end;
then
A8: meet rng F c= E /\ great_eq_dom(inf f,r);
now
let x be object;
assume
A9: x in E /\ great_eq_dom(inf f,r);
then reconsider z=x as Element of X;
A10: x in E by A9,XBOOLE_0:def 4;
x in great_eq_dom(inf f,r) by A9,XBOOLE_0:def 4;
then
A11: r <= (inf f).z by MESFUNC1:def 14;
now
let y be set;
assume y in rng F;
then consider n be object such that
A12: n in NAT and
A13: y=F.n by FUNCT_2:11;
reconsider n as Element of NAT by A12;
A14: x in dom (f.n) by A10,Def2;
x in dom inf f by A10,Def3;
then
A15: (inf f).z = inf(f#z) by Def3;
A16: x in E by A9,XBOOLE_0:def 4;
(f.n).z=(f#z).n by MESFUNC5:def 13;
then inf (f#z)<= (f.n).z by RINFSUP2:23;
then r <= (f.n).z by A11,A15,XXREAL_0:2;
then
A17: x in great_eq_dom(f.n,r) by A14,MESFUNC1:def 14;
F.n = E /\ great_eq_dom(f.n,r) by A1;
hence x in y by A13,A16,A17,XBOOLE_0:def 4;
end;
hence x in meet rng F by SETFAM_1:def 1;
end;
then E /\ great_eq_dom((inf f),r) c= meet rng F;
hence thesis by A8,XBOOLE_0:def 10;
end;
theorem Th17:
for f be with_the_same_dom Functional_Sequence of X,ExtREAL, F
be SetSequence of S, r be Real st (for n be Nat holds F.n =
dom(f.0) /\ great_dom(f.n,r)) holds for n be Nat holds (
superior_setsequence F).n = dom(f.0) /\ great_dom((superior_realsequence f).n,
r)
proof
let f be with_the_same_dom Functional_Sequence of X,ExtREAL, F be
SetSequence of S, r be Real;
set E = dom(f.0);
assume
A1: for n be Nat holds F.n = E /\ great_dom(f.n,r);
let n be Nat;
reconsider n9=n as Element of NAT by ORDINAL1:def 12;
set f1=f^\n9;
set F1=F^\n9;
A2: now
let k be Nat;
reconsider k9=k as Element of NAT by ORDINAL1:def 12;
F1.k = F.(n+k9) by NAT_1:def 3;
then F1.k = E /\ great_dom(f.(n+k9),r) by A1;
hence F1.k = E /\ great_dom(f1.k,r) by NAT_1:def 3;
end;
A3: union rng (F^\n9) = (superior_setsequence F).n by Th2;
consider g be sequence of PFuncs(X,ExtREAL) such that
A4: f=g and
f^\n9=g^\n9;
f1.0 = g.(n+(0 qua Nat)) by A4,NAT_1:def 3;
then dom(f1.0)= E by A4,Def2;
then union rng F1 = E /\ great_dom(sup f1,r) by A2,Th15;
hence thesis by A3,Th9;
end;
theorem Th18:
for f be with_the_same_dom Functional_Sequence of X,ExtREAL,
F be SetSequence of S, r be Real st
(for n be Nat holds F.n = dom(f.0) /\ great_eq_dom(f.n,r))
holds for n be Nat holds
(inferior_setsequence F).n = dom(f.0) /\
great_eq_dom((inferior_realsequence f).n,r)
proof
let f be with_the_same_dom Functional_Sequence of X,ExtREAL, F be
SetSequence of S, r be Real;
set E = dom(f.0);
assume that
A1: for n be Nat holds F.n = E /\ great_eq_dom(f.n,r);
let n be Nat;
reconsider n9=n as Element of NAT by ORDINAL1:def 12;
set f1=f^\n9;
set F1=F^\n9;
A2: now
let k be Nat;
reconsider k9=k as Element of NAT by ORDINAL1:def 12;
F1.k = F.(n+k9) by NAT_1:def 3;
then F1.k = E /\ great_eq_dom(f.(n+k9),r) by A1;
hence F1.k = E /\ great_eq_dom(f1.k,r) by NAT_1:def 3;
end;
A3: meet rng(F^\n9) = (inferior_setsequence F).n by Th2;
consider g be sequence of PFuncs(X,ExtREAL) such that
A4: f=g and
f^\n9=g^\n9;
f1.0 = g.(n+(0 qua Nat)) by A4,NAT_1:def 3;
then dom(f1.0) = E by A4,Def2;
then meet rng F1 = E /\ great_eq_dom(inf f1,r) by A2,Th16;
hence thesis by A3,Th8;
end;
theorem Th19:
for f be with_the_same_dom Functional_Sequence of X,ExtREAL,
E be Element of S st dom (f.0) = E &
(for n be Nat holds f.n is E-measurable) holds
for n holds (superior_realsequence f).n is E-measurable
proof
let f be with_the_same_dom Functional_Sequence of X,ExtREAL, E be Element of
S;
assume that
A1: dom (f.0) = E and
A2: for n be Nat holds f.n is E-measurable;
let n;
reconsider n9=n as Element of NAT by ORDINAL1:def 12;
A3: now
let r be Real;
deffunc G(Element of NAT) = E /\ great_dom(f.$1,r);
consider F being sequence of bool X such that
A4: for x being Element of NAT holds F.x = G(x) from FUNCT_2:sch 4;
now
let i be Nat;
A5: f.i is E-measurable by A2;
i in NAT by ORDINAL1:def 12;
then
A6: F.i=E /\ great_dom(f.i,r) by A4;
dom (f.i) = E by A1,Def2;
hence F.i in S by A6,A5,MESFUNC1:29;
end;
then
A7: rng F c= S by NAT_1:52;
A8: for x being Nat holds F.x = E /\ great_dom(f.x,r)
proof
let x be Nat;
reconsider x9=x as Element of NAT by ORDINAL1:def 12;
F.x9 = E /\ great_dom(f.x9,r) by A4;
hence thesis;
end;
reconsider F as SetSequence of S by A7,RELAT_1:def 19;
(superior_setsequence F).n9 in rng (superior_setsequence F) by NAT_1:51;
then (superior_setsequence F).n9 in S;
hence E /\ great_dom((superior_realsequence f).n,r) in S by A1,A8,Th17;
end;
dom((superior_realsequence f).n9) = E by A1,Def6;
hence thesis by A3,MESFUNC1:29;
end;
theorem Th20:
for f be with_the_same_dom Functional_Sequence of X,ExtREAL,
E be Element of S st dom (f.0) = E &
(for n be Nat holds f.n is E-measurable) holds
for n be Nat holds (inferior_realsequence f).n is E-measurable
proof
let f be with_the_same_dom Functional_Sequence of X,ExtREAL,
E be Element of S;
assume that
A1: dom(f.0) = E and
A2: for n be Nat holds f.n is E-measurable;
let n be Nat;
reconsider n9=n as Element of NAT by ORDINAL1:def 12;
A3: now
let r be Real;
deffunc G(Element of NAT) = E /\ great_eq_dom(f.$1,r);
consider F being sequence of bool X such that
A4: for x being Element of NAT holds F.x = G(x) from FUNCT_2:sch 4;
now
let i be Nat;
A5: f.i is E-measurable by A2;
i in NAT by ORDINAL1:def 12;
then
A6: F.i=E /\ great_eq_dom(f.i,r) by A4;
dom (f.i) = E by A1,Def2;
hence F.i in S by A6,A5,MESFUNC1:27;
end;
then
A7: rng F c= S by NAT_1:52;
A8: for x being Nat holds F.x = E /\ great_eq_dom(f.x,r)
proof
let x be Nat;
reconsider x9=x as Element of NAT by ORDINAL1:def 12;
F.x9 = E /\ great_eq_dom(f.x9,r) by A4;
hence thesis;
end;
reconsider F as SetSequence of S by A7,RELAT_1:def 19;
(inferior_setsequence F).n9 in rng inferior_setsequence F by NAT_1:51;
then (inferior_setsequence F).n9 in S;
hence
E /\ great_eq_dom((inferior_realsequence f).n,r ) in S by A1,A8,Th18;
end;
dom((inferior_realsequence f).n9) = E by A1,Def5;
hence thesis by A3,MESFUNC1:27;
end;
theorem Th21:
for f be Functional_Sequence of X,ExtREAL, F be SetSequence of S,
r be Real st
(for n be Nat holds F.n = dom(f.0) /\
great_eq_dom((superior_realsequence f).n,r)) holds
meet F = dom(f.0) /\ great_eq_dom(lim_sup f,r)
proof
let f be Functional_Sequence of X,ExtREAL, F be SetSequence of S, r be Real;
set E = dom(f.0);
set g=superior_realsequence f;
assume
A1: for n be Nat holds F.n = E /\ great_eq_dom(g.n,r);
dom(g.0) = dom(f.0) by Def6;
then meet rng F = E /\ great_eq_dom(inf g,r) by A1,Th16;
hence thesis by Th12;
end;
theorem Th22:
for f be Functional_Sequence of X,ExtREAL, F be SetSequence of S,
r be Real st (for n be Nat holds F.n = dom(f.0) /\ great_dom
((inferior_realsequence f).n,r)) holds
union rng F = dom(f.0) /\ great_dom(lim_inf f,r)
proof
let f be Functional_Sequence of X,ExtREAL, F be SetSequence of S, r be Real;
set E = dom(f.0);
set g=inferior_realsequence f;
assume
A1: for n be Nat holds F.n = E /\ great_dom(g.n,r);
dom(g.0) = dom(f.0) by Def5;
then union rng F = E /\ great_dom(sup g,r) by A1,Th15;
hence thesis by Th11;
end;
theorem Th23:
for f be with_the_same_dom Functional_Sequence of X,ExtREAL,
E be Element of S st dom (f.0) = E &
(for n be Nat holds f.n is E-measurable) holds lim_sup f is E-measurable
proof
let f be with_the_same_dom Functional_Sequence of X,ExtREAL, E be Element of
S;
assume that
A1: dom (f.0) = E and
A2: for n be Nat holds f.n is E-measurable;
A3: now
let r be Real;
deffunc G(Element of NAT) = E /\ great_eq_dom((superior_realsequence f).$1
,r);
consider F being sequence of bool X such that
A4: for x being Element of NAT holds F.x = G(x) from FUNCT_2:sch 4;
now
let i be Nat;
A5: dom((superior_realsequence f).i) = dom(f.0) by Def6;
i in NAT by ORDINAL1:def 12;
then
A6: F.i = E /\ great_eq_dom((superior_realsequence f).i,r) by A4;
(superior_realsequence f).i is E-measurable by A1,A2,Th19;
hence F.i in S by A1,A6,A5,MESFUNC1:27;
end;
then
A7: rng F c= S by NAT_1:52;
A8: for x being Nat holds
F.x = E /\ great_eq_dom((superior_realsequence f).x,r)
proof
let x be Nat;
reconsider x9=x as Element of NAT by ORDINAL1:def 12;
F.x9 = E /\ great_eq_dom((superior_realsequence f).x9,r) by A4;
hence thesis;
end;
reconsider F as SetSequence of S by A7,RELAT_1:def 19;
rng F c= S;
then F is sequence of S by FUNCT_2:6;
then
A9: rng F is N_Sub_set_fam of X by MEASURE1:23;
A10: rng F is N_Measure_fam of S by A9,MEASURE2:def 1;
meet F = E /\ great_eq_dom(lim_sup f,r) by A1,A8,Th21;
hence E /\ great_eq_dom(lim_sup f,r) in S by A10,MEASURE2:2;
end;
dom (lim_sup f) = dom(f.0) by Def8;
hence thesis by A1,A3,MESFUNC1:27;
end;
theorem
for f be with_the_same_dom Functional_Sequence of X,ExtREAL,
E be Element of S st dom(f.0) = E &
(for n be Nat holds f.n is E-measurable) holds lim_inf f is E-measurable
proof
let f be with_the_same_dom Functional_Sequence of X,ExtREAL,
E be Element of S;
assume that
A1: dom(f.0) = E and
A2: for n be Nat holds f.n is E-measurable;
A3: now
let r be Real;
deffunc G(Element of NAT) = E /\ great_dom((inferior_realsequence f).$1,
r);
consider F being sequence of bool X such that
A4: for x being Element of NAT holds F.x = G(x) from FUNCT_2:sch 4;
now
let i be Nat;
i in NAT by ORDINAL1:def 12;
then
A5: F.i = E /\ great_dom((inferior_realsequence f).i,r) by A4;
A6: dom((inferior_realsequence f).i) = E by A1,Def5;
(inferior_realsequence f).i is E-measurable by A1,A2,Th20;
hence F.i in S by A5,A6,MESFUNC1:29;
end;
then
A7: rng F c= S by NAT_1:52;
A8: for x be Nat holds F.x = E /\ great_dom((
inferior_realsequence f).x,r)
proof
let x be Nat;
reconsider x9=x as Element of NAT by ORDINAL1:def 12;
F.x9 = E /\ great_dom((inferior_realsequence f).x9,r) by A4;
hence thesis;
end;
reconsider F as SetSequence of S by A7,RELAT_1:def 19;
rng F c= S;
then F is sequence of S by FUNCT_2:6;
then
A9: rng F is N_Sub_set_fam of X by MEASURE1:23;
A10: rng F is N_Measure_fam of S by A9,MEASURE2:def 1;
union rng F = E /\ great_dom(lim_inf f,r) by A1,A8,Th22;
hence E /\ great_dom(lim_inf f,r) in S by A10,MEASURE2:2;
end;
dom lim_inf f = E by A1,Def7;
hence thesis by A3,MESFUNC1:29;
end;
theorem Th25:
for f be with_the_same_dom Functional_Sequence of X,ExtREAL,
E be Element of S st dom(f.0) = E &
(for n be Nat holds f.n is E-measurable) &
(for x be Element of X st x in E holds f#x is convergent) holds
lim f is E-measurable
proof
let f be with_the_same_dom Functional_Sequence of X,ExtREAL,
E be Element of S;
assume
A1: dom (f.0) = E; then
A2: dom lim_sup f = E by Def8;
assume that
A3: for n be Nat holds f.n is E-measurable and
A4: for x be Element of X st x in E holds f#x is convergent;
A5: dom lim f = E by A1,Def9;
A6: now
let x be Element of X;
assume
A7: x in dom lim f;
then f#x is convergent by A5,A4;
hence (lim f).x= (lim_sup f).x by A7,Th14;
end;
lim_sup f is E-measurable by A1,A3,Th23;
hence thesis by A5,A2,A6,PARTFUN1:5;
end;
theorem Th26:
for f be with_the_same_dom Functional_Sequence of X,ExtREAL,
g be PartFunc of X,ExtREAL, E be Element of S st
dom(f.0) = E &
(for n be Nat holds f.n is E-measurable) & dom g = E &
for x be Element of X st x in E holds f#x is convergent &
g.x = lim(f#x) holds g is E-measurable
proof
let f be with_the_same_dom Functional_Sequence of X,ExtREAL, g be PartFunc
of X,ExtREAL, E be Element of S;
assume that
A1: dom (f.0) = E and
A2: for n be Nat holds f.n is E-measurable and
A3: dom g = E and
A4: for x be Element of X st x in E holds f#x is convergent & g.x = lim( f#x);
A5: dom lim f = E by A1,Def9;
now
let x be Element of X;
assume
A6: x in dom lim f;
then g.x= lim(f#x) by A4,A5;
hence g.x = (lim f).x by A6,Def9;
end;
then
A7: g = lim f by A3,A5,PARTFUN1:5;
for x be Element of X st x in E holds f#x is convergent by A4;
hence thesis by A1,A2,A7,Th25;
end;
theorem Th27:
for f be Functional_Sequence of X,ExtREAL, g be PartFunc of X,ExtREAL st
for x be Element of X st x in dom g holds
f#x is convergent_to_finite_number &
g.x = lim (f#x) holds g is real-valued
proof
let f be Functional_Sequence of X,ExtREAL, g be PartFunc of X,ExtREAL;
assume
A1: for x be Element of X st x in dom g holds
f#x is convergent_to_finite_number & g.x = lim (f#x);
now
let x be Element of X;
assume
A2: x in dom g; then
A3: not (lim (f#x)=+infty & f#x is convergent_to_+infty ) by A1,MESFUNC5:50;
f#x is convergent_to_finite_number by A1,A2; then
A4: f#x is convergent by MESFUNC5:def 11;
not (lim (f#x)=-infty & f#x is convergent_to_-infty ) by A1,A2,MESFUNC5:51;
then consider g0 be Real such that
A5: lim (f#x) = g0 and
for p be Real st 0<p ex n be Nat st for m be Nat st n<=m holds
|.(f#x).m-lim (f#x).| < p and
f#x is convergent_to_finite_number by A4,A3,MESFUNC5:def 12;
|. g.x .| = |.g0 qua Complex.| by A1,A2,A5,EXTREAL1:12;
hence |. g.x .| < +infty by XXREAL_0:9,XREAL_0:def 1;
end;
hence thesis by MESFUNC2:def 1;
end;
begin :: Egoroff's Theorem
theorem Th28:
for M be sigma_Measure of S,
f be with_the_same_dom Functional_Sequence of X,ExtREAL,
g be PartFunc of X,ExtREAL, E be Element of S st
M.E < +infty & dom(f.0) = E &
(for n be Nat holds f.n is E-measurable & f.n is real-valued) &
dom g = E & for x be Element of X st x in E holds
f#x is convergent_to_finite_number & g.x = lim(f#x) holds
for r,e be Real st 0 < r & 0 < e ex H be Element of S, N be Nat st
H c= E & M.H < r & for k be Nat st N < k holds
for x be Element of X st x in E\H holds |. (f.k).x - g.x .| < e
proof
let M be sigma_Measure of S,
f be with_the_same_dom Functional_Sequence of X,ExtREAL,
g be PartFunc of X,ExtREAL, E be Element of S;
assume that
A1: M.E < +infty and
A2: dom (f.0) = E and
A3: for n be Nat holds f.n is E-measurable & f.n is
real-valued and
A4: dom g = E and
A5: for x be Element of X st x in E holds f#x is
convergent_to_finite_number & g.x = lim(f#x);
let r,e be Real;
defpred P[Element of NAT,set] means $2 =E /\ less_dom(|.f.$1 - g.|,e);
A6: g is real-valued by A4,A5,Th27;
for x be Element of X st x in E holds f#x is convergent & g.x = lim(f#x)
proof
let x be Element of X;
assume
A7: x in E;
then f#x is convergent_to_finite_number by A5;
hence f#x is convergent by MESFUNC5:def 11;
thus thesis by A5,A7;
end;
then
A8: g is E-measurable by A2,A3,A4,Th26;
A9: for n be Element of NAT holds |.f.n - g.| is E-measurable & dom(f.n-
g) = E & dom(|.f.n - g.|) = E
proof
let n be Element of NAT;
A10: f.n is real-valued by A3;
dom(f.n-g) = dom(f.n) /\ dom g by A6,MESFUNC2:2; then
A11: dom(f.n-g) = E /\ E by A2,A4,Def2;
f.n is E-measurable by A3;
then f.n - g is E-measurable by A4,A8,A6,A10,MESFUNC2:11;
hence thesis by A11,MESFUNC1:def 10,MESFUNC2:27;
end;
A12: for n be Element of NAT ex Z be Element of S st P[n,Z]
proof
let n be Element of NAT;
|.f.n - g.| is E-measurable by A9;
then E /\ less_dom(|.f.n - g.|,e) in S by MESFUNC1:def 16;
hence thesis;
end;
consider K be sequence of S such that
A13: for n be Element of NAT holds P[n,K.n] from FUNCT_2:sch 3(A12);
defpred Q[Nat,set] means $2 ={x where x is Element of X : for k
st $1 <= k holds x in K.k};
A14: for n be Element of NAT ex Z be Element of S st Q[n,Z]
proof
let n be Element of NAT;
take {x where x is Element of X : for k st n <= k holds x in K.k};
thus thesis by Th1;
end;
consider EN be sequence of S such that
A15: for n be Element of NAT holds Q[n,EN.n] from FUNCT_2:sch 3(A14);
A16: for n be Nat holds Q[n,EN.n]
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A15;
end;
A17: 0. <= M.E by MEASURE1:def 2;
then reconsider ME= M.E as Element of REAL by A1,XXREAL_0:14;
defpred R[Element of NAT,set] means $2=M.(EN.$1);
A18: for n be Nat holds EN.n c= E & M.(EN.n) <= M.E & M.(EN.n) is
Element of REAL & M.(E \ EN.n)= M.E - M.(EN.n) & M.(E \ EN.n) is Element of
REAL
proof
reconsider r1= M.E as Element of REAL by A1,A17,XXREAL_0:14;
let n be Nat;
reconsider n9=n as Element of NAT by ORDINAL1:def 12;
thus
A19: EN.n c= E
proof
let z be object;
assume z in EN.n;
then
z in {x where x is Element of X : for k st n9 <= k holds x in K.k }
by A16;
then ex x be Element of X st z=x & for k st n <= k holds x in K.k;
then z in K.n;
then z in E /\ less_dom(|.f.n9 - g.| ,e) by A13;
hence thesis by XBOOLE_0:def 4;
end;
hence
A20: M.(EN.n) <= M.E by MEASURE1:31;
A21: -infty < M.(EN.n) by MEASURE1:def 2;
then reconsider r2= M.(EN.n) as Element of REAL by A1,A20,XXREAL_0:14;
thus M.(EN.n) is Element of REAL by A1,A20,A21,XXREAL_0:14;
thus M.(E \ EN.n)= M.E - M.(EN.n) by A1,A19,A20,MEASURE1:32,XXREAL_0:4;
M.E - M.(EN.n) = r1-r2 by SUPINF_2:3;
hence thesis by A19,MEASURE1:32,XXREAL_0:4;
end;
A22: now
let n be Element of NAT;
M.(EN.n) is Element of REAL by A18;
hence ex y be Element of REAL st R[n,y];
end;
consider seq1 be Real_Sequence such that
A23: for n be Element of NAT holds R[n,seq1.n] from FUNCT_2:sch 3(A22);
assume
A24: 0 < r;
assume
A25: 0 < e;
A26: E c= union rng EN
proof
let z be object;
assume
A27: z in E;
then reconsider x= z as Element of X;
A28: not (lim(f#x) = +infty & f#x is convergent_to_+infty)
by A5,A27,MESFUNC5:50;
f#x is convergent_to_finite_number by A5,A27; then
A29: f#x is convergent by MESFUNC5:def 11;
not (lim(f#x) = -infty & f#x is convergent_to_-infty) by A5,A27,MESFUNC5:51
;
then ex g be Real st lim(f#x) = g & (for p be Real st 0 < p
ex n be Nat st for m be Nat st n<=m holds |.(f#x).m - lim(f#x).| < p) & f#x is
convergent_to_finite_number by A29,A28,MESFUNC5:def 12;
then consider n be Nat such that
A30: for m be Nat st n<=m holds |.(f#x).m - lim(f#x).| < e by A25;
reconsider n0=n as Element of NAT by ORDINAL1:def 12;
A31: g.x = lim (f#x) by A5,A27;
now
let k;
reconsider k9=k as Element of NAT by ORDINAL1:def 12;
A32: dom |.f.k9 - g.| = E by A9;
assume n0 <=k;
then |.(f#x).k-lim (f#x).| < e by A30;
then
A33: |.(f.k).x-g.x.| < e by A31,MESFUNC5:def 13;
dom(f.k9 - g) = E by A9;
then |.(f.k - g).x .| < e by A27,A33,MESFUNC1:def 4;
then (|.f.k - g.|).x < e by A27,A32,MESFUNC1:def 10;
then x in less_dom(|.f.k - g.|,e) by A27,A32,MESFUNC1:def 11;
then x in E /\ less_dom(|.f.k - g.|,e) by A27,XBOOLE_0:def 4;
then x in K.k9 by A13;
hence x in K.k;
end;
then x in {y where y is Element of X : for k st n0 <= k holds y in K.k};
then
A34: x in EN.n0 by A16;
EN.n0 in rng EN by FUNCT_2:4;
hence thesis by A34,TARSKI:def 4;
end;
defpred U[Element of NAT,set] means $2=M.(E \ EN.$1);
A35: dom(M*EN) = NAT by FUNCT_2:def 1;
A36: for n,m be Nat st n <= m holds EN.n c= EN.m & M.(EN.n) <= M.(EN.m)
proof
let n,m be Nat;
assume
A37: n <= m;
thus EN.n c= EN.m
proof
let z be object;
assume z in EN.n;
then z in {x where x is Element of X : for k st n <= k holds x in K.k}
by A16;
then
A38: ex x be Element of X st z=x & for k st n <= k holds x in K.k;
then for k st m <= k holds z in K.k by A37,XXREAL_0:2;
then z in {y where y is Element of X : for k st m <= k holds y in K.k}
by A38;
hence thesis by A16;
end;
hence thesis by MEASURE1:31;
end;
set seq3 = NAT --> ME;
A39: for n be Nat holds seq3.n=ME by ORDINAL1:def 12,FUNCOP_1:7; then
A40: seq3 is constant by VALUED_0:def 18;
A41: now
let x be object;
assume
A42: x in dom (M*EN);
then reconsider n=x as Element of NAT;
(M*EN).x = M.(EN.n) by A42,FUNCT_1:12;
hence (M*EN).x = seq1.x by A23;
end;
dom seq1 = NAT by FUNCT_2:def 1;
then
A43: M*EN=seq1 by A35,A41,FUNCT_1:2;
now
let y be set;
assume y in rng EN;
then consider x be object such that
A44: x in NAT and
A45: y=EN.x by FUNCT_2:11;
reconsider x9=x as Nat by A44;
y = EN.x9 by A45;
hence y c= E by A18;
end;
then union rng EN c= E by ZFMISC_1:76; then
A46: union rng EN=E by A26,XBOOLE_0:def 10;
A47: seq1 is convergent & lim seq1 = M.E
proof
reconsider r1 = M.E as Element of REAL by A1,A17,XXREAL_0:14;
A48: for n being Nat holds EN.n c= EN.(n+1)
proof
let n be Nat;
n <=n+1 by NAT_1:12;
hence thesis by A36;
end;
A49: now
let n be Nat;
A50: n in NAT by ORDINAL1:def 12;
M.(EN.n) <= M.E by A18;
then
A51: seq1.n <= r1 by A23,A50;
r1+(0 qua Nat) < r1+1 by XREAL_1:8;
hence seq1.n < r1+1 by A51,XXREAL_0:2;
end; then
A52: seq1 is bounded_above by SEQ_2:def 3;
consider r be Real such that
A53: for n be Nat holds seq1.n < r by A49;
r is UpperBound of rng seq1
proof
let d be ExtReal;
assume d in rng seq1;
then ex x be object st x in NAT & d=seq1.x by FUNCT_2:11;
hence d <= r by A53;
end;
then rng seq1 is bounded_above;
then
A54: sup rng(M*EN) = upper_bound rng seq1 by A43,RINFSUP2:1;
now
let n,m be Nat;
assume
A55: n<=m;
A56: n in NAT by ORDINAL1:def 12;
A57: m in NAT by ORDINAL1:def 12;
A58: seq1.m = M.(EN.m) by A23,A57;
seq1.n = M.(EN.n) by A23,A56;
hence seq1.n <= seq1.m by A36,A55,A58;
end; then
A59: seq1 is non-decreasing by SEQM_3:6;
hence seq1 is convergent by A52;
lim seq1 = upper_bound seq1 by A59,A52,RINFSUP1:24;
hence thesis by A46,A54,A48,MEASURE2:23;
end;
A60: now
let n be Element of NAT;
M.(E \ EN.n) is Element of REAL by A18;
hence ex y be Element of REAL st U[n,y];
end;
consider seq2 be Real_Sequence such that
A61: for n be Element of NAT holds U[n,seq2.n] from FUNCT_2:sch 3(A60);
now
let n be Nat;
A62: n in NAT by ORDINAL1:def 12;
seq2.n = M.(E \ EN.n) by A61,A62; then
A63: seq2.n = M.E-M.(EN.n) by A18;
M.(EN.n)=seq1.n by A23,A62;
then seq2.n = ME- seq1.n by A63,SUPINF_2:3;
then seq2.n = seq3.n - seq1.n by A39;
hence seq2.n = seq3.n +(- seq1).n by SEQ_1:10;
end;
then
A64: seq2 = seq3 - seq1 by SEQ_1:7;
then
A65: seq2 is convergent by A47,A40;
A66: seq3.0 = ME by A39;
lim seq2 = lim seq3 -lim seq1 by A47,A64,A40,SEQ_2:12;
then lim seq2 =ME - ME by A47,A40,A66,SEQ_4:25;
then consider N be Nat such that
A67: for m be Nat st N<=m holds |.seq2.m-0 qua Complex .|< r by A24,A65,
SEQ_2:def 7;
reconsider H = E \ EN.N as Element of S;
A68: E\H = E /\ EN.N by XBOOLE_1:48;
EN.N c= E by A18;
then
A69: E\H = EN.N by A68,XBOOLE_1:28;
A70: for k be Nat st N < k holds for x be Element of X st x in E
\H holds |. (f.k).x - g.x .| < e
proof
let k be Nat;
reconsider k9=k as Element of NAT by ORDINAL1:def 12;
assume
A71: N < k;
let x be Element of X;
assume x in E\H;
then x in {y where y is Element of X :
for k st N <= k holds y in K.k} by
A16,A69;
then ex y be Element of X st x=y & for k st N <= k holds y in K.k;
then x in K.k by A71; then
A72: x in E /\ less_dom(|.f.k9 - g.|,e) by A13; then
A73: x in E by XBOOLE_0:def 4;
x in less_dom(|.f.k - g.|,e) by A72,XBOOLE_0:def 4; then
A74: (|.f.k - g.|).x < e by MESFUNC1:def 11;
A75: dom (f.k9 - g) = E by A9;
dom |.f.k9 - g.| = E by A9;
then |.(f.k - g).x .| < e by A73,A74,MESFUNC1:def 10;
hence thesis by A73,A75,MESFUNC1:def 4;
end;
take H,N;
A76: N in NAT by ORDINAL1:def 12;
M.(E \ EN.N)=seq2.N by A61,A76;
then
A77: 0 <= seq2.N by MEASURE1:def 2;
|.seq2.N - 0 qua Complex .|< r by A67;
then seq2.N < r by A77,ABSVALUE:def 1;
hence thesis by A61,A70,XBOOLE_1:36,A76;
end;
theorem
for X,Y be non empty set, E be set, F,G be Function of X,Y st
for x be Element of X holds G.x = E \ F.x holds
union rng G = E \ meet rng F
proof
let X,Y be non empty set,E be set,F,G be Function of X,Y;
assume
A1: for x be Element of X holds G.x = E \ F.x;
A2: dom G = X by FUNCT_2:def 1;
now
let Z be object;
assume Z in DIFFERENCE({E},rng F);
then consider X1,Y be set such that
A3: X1 in {E} and
A4: Y in rng F and
A5: Z = X1 \ Y by SETFAM_1:def 6;
consider x be object such that
A6: x in dom F and
A7: Y = F.x by A4,FUNCT_1:def 3;
reconsider x as Element of X by A6;
X1 = E by A3,TARSKI:def 1;
then Z = G.x by A1,A5,A7;
hence Z in rng G by A2,FUNCT_1:3;
end;
then
A8: DIFFERENCE({E},rng F) c= rng G;
A9: dom F = X by FUNCT_2:def 1;
now
let Z be object;
A10: E in {E} by TARSKI:def 1;
assume Z in rng G;
then consider x be object such that
A11: x in dom G and
A12: Z = G.x by FUNCT_1:def 3;
reconsider x as Element of X by A11;
A13: F.x in rng F by A9,FUNCT_1:3;
Z = E \ F.x by A1,A12;
hence Z in DIFFERENCE({E},rng F) by A13,A10,SETFAM_1:def 6;
end;
then rng G c= DIFFERENCE({E},rng F);
then DIFFERENCE({E},rng F) = rng G by A8,XBOOLE_0:def 10;
hence thesis by SETFAM_1:27;
end;
reconsider jj=1 as Real;
::$N Egorov's theorem
theorem
for M be sigma_Measure of S,
f be with_the_same_dom Functional_Sequence of X,ExtREAL,
g be PartFunc of X,ExtREAL, E be Element of S st
(dom (f.0) = E & for n be Nat holds f.n is E-measurable) &
M.E < +infty &
(for n be Nat holds ex L be Element of S st L c= E &
M.(E\L) = 0 &
for x be Element of X st x in L holds |. (f.n).x .| < +infty) &
ex G be Element of S st G c= E & M.(E\G) = 0 &
(for x be Element of X st x in E holds
f#x is convergent_to_finite_number) & dom g = E &
(for x be Element of X st x in G holds g.x = lim (f#x)) holds
for e be Real st 0 < e ex F be Element of S st
F c= E & M.(E\F) <= e & for p be Real st 0 < p ex N be Nat st
for n be Nat st N < n holds
for x be Element of X st x in F holds |. (f.n).x - g.x .| < p
proof
let M be sigma_Measure of S,
f be with_the_same_dom Functional_Sequence of X,ExtREAL,
g be PartFunc of X,ExtREAL, E be Element of S such that
A1: dom(f.0) = E and
A2: for n be Nat holds f.n is E-measurable and
A3: M.E < +infty and
A4: for n be Nat holds ex L be Element of S st L c= E & M.(E\
L) = 0 & for x be Element of X st x in L holds |. (f.n).x .| < +infty and
A5: ex G be Element of S st G c= E & M.(E\G) = 0 & (for x be Element of
X st x in E holds (f#x) is convergent_to_finite_number) & dom g = E & for x be
Element of X st x in G holds g.x = lim (f#x);
defpred P[Element of NAT,set] means $2 c= E & M.(E\$2) = 0 & for x be
Element of X st x in ($2) holds |. (f.$1).x .| < +infty;
A6: for n be Element of NAT ex Z be Element of S st P[n,Z] by A4;
consider LN be sequence of S such that
A7: for n be Element of NAT holds P[n,LN.n] from FUNCT_2:sch 3(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;
assume
A8: 0 < e0;
set e=e0/2;
consider G be Element of S such that
A9: G c= E and
A10: M.(E\G) = 0 and
A11: for x be Element of X st x in E holds f#x is
convergent_to_finite_number and
A12: dom g = E and
A13: for x be 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 gL = dom g /\ L by RELAT_1:61; then
A16: dom gL = L by A9,A12,A14,XBOOLE_1:1,28;
deffunc FNL(Nat) = (f.$1)|L;
consider fL be Functional_Sequence of X,ExtREAL such that
A17: for n be Nat holds fL.n=FNL(n) from SEQFUNC:sch 1;
for n,m be Nat holds dom (fL.n) = dom (fL.m)
proof
let n,m be Nat;
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 thesis by A18,Def2;
end;
then reconsider fL as with_the_same_dom Functional_Sequence of X,ExtREAL by
Def2;
A19: L c= E by A9,A14;
A20: for x be Element of X st x in L holds fL#x is
convergent_to_finite_number & gL.x = lim (fL#x)
proof
let x be Element of X;
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;
A24: for y be object st y in NAT holds (fL#x).y = (f#x).y
proof
let y be object;
assume y in NAT;
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 thesis by A25,MESFUNC5:def 13;
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;
L c= G by XBOOLE_1:17;
then g.x = lim (f#x) by A13,A23;
hence thesis by A23,A26,FUNCT_1:49;
end;
defpred R[Element of NAT,set] means $2 c= L & M.($2) < (e(#)(1/2)GeoSeq).$1
& ex Np be Element of NAT st for k be Element of NAT st Np < k holds for x be
Element of X st x in L\$2 holds |. (fL.k).x - gL.x .| < ((1/2)GeoSeq).$1;
A27: for n be Nat holds dom (fL.n) = L & fL.n is L-measurable
& fL.n is real-valued
proof
let n be Nat;
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,28;
f.n is L-measurable by A2,A19,MESFUNC1:30;
hence fL.n is L-measurable by A28,A29,A30,MESFUNC5:42;
for x be Element of X st x in dom (fL.n) holds |. (fL.n).x .| < +infty
proof
let x be Element of X;
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);
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 thesis by A28,A32,FUNCT_1:47;
end;
hence thesis by MESFUNC2:def 1;
end; then
A33: dom (fL.0) = L;
A34: for p be Nat ex Hp be Element of S, Np be Nat st
Hp c= L & M.(Hp) < (e(#) (1/2) GeoSeq).p & for k be Nat st Np < k
holds for x be Element of X st x in L\Hp holds |. (fL.k).x - gL.x .| < ((1/2)
GeoSeq).p
proof
let p be Nat;
reconsider p9=p as Element of NAT by ORDINAL1:def 12;
A35: (e(#)(1/2) GeoSeq).p = e*((1/2)GeoSeq).p9 by SEQ_1:9;
0 < (jj/2)|^p by PREPOWER:6;
then
A36: 0 < ((1/2)GeoSeq).p9 by PREPOWER:def 1;
0 < (jj/2)|^p by PREPOWER:6;
then
A37: 0 < ((1/2)GeoSeq).p9 by PREPOWER:def 1;
e0/2 = e0 qua ExtReal/2;
then 0 < e by A8;
then 0 < (e(#)(1/2) GeoSeq).p by A36,A35,XREAL_1:129;
hence thesis by A15,A27,A33,A16,A20,A37,Th28;
end;
A38: for n be Element of NAT ex Z be Element of S st R[n,Z]
proof
let n be Element of NAT;
reconsider n9=n as Nat;
consider Z be Element of S, Np be Nat such that
A39: Z c= L and
A40: M.Z < (e(#)(1/2)GeoSeq).n9 and
A41: for k be Nat st Np < k holds for x be Element of X st
x in L\Z holds |. (fL.k).x - gL.x .| < ((1/2)GeoSeq).n9 by A34;
reconsider Np9=Np as Element of NAT by ORDINAL1:def 12;
for k be Element of NAT st Np9 < k holds for x be Element of X st x
in L\Z holds |. (fL.k).x - gL.x .| < ((1/2)GeoSeq).n9 by A41;
hence thesis by A39,A40;
end;
consider HP be sequence of S such that
A42: for p be Element of NAT holds R[p,HP.p] from FUNCT_2:sch 3(A38);
defpred U[Element of NAT,set] means $2= M.(HP.$1);
A43: for n be Element of NAT ex y be Element of REAL st U[n,y]
proof
let n be Element of NAT;
A44: -infty < M.(HP.n) by MEASURE1:def 2;
M.(HP.n) < (e(#)(1/2)GeoSeq).n by A42;
then M.(HP.n) in REAL by A44,XXREAL_0:48;
hence thesis;
end;
consider me be Real_Sequence such that
A45: for p be Element of NAT holds U[p,me.p] from FUNCT_2:sch 3(A43);
A46: for p be Element of NAT holds me.p <= (e(#)(1/2) GeoSeq).p
proof
let p be Element of NAT;
me.p = M.(HP.p) by A45;
hence thesis by A42;
end;
A47: for p be Nat holds 0 <=me.p & me.p <= (e(#)(1/2)GeoSeq).p
proof
let p be Nat;
A48: p in NAT by ORDINAL1:def 12;
0. <= M.(HP.p) by MEASURE1:def 2;
hence thesis by A45,A46,A48;
end;
then for p be Nat holds 0 <=me.p & me.p <= (e(#)(1/2)GeoSeq).p; then
A49: me is nonnegative;
deffunc ELN(Element of NAT) = E \ (LN.$1);
consider ELN be sequence of S such that
A50: for n be Element of NAT holds ELN.n=ELN(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;
A51: 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 being set;
assume A in RELN;
then consider n be object such that
A52: n in NAT and
A53: A=ELN.n by FUNCT_2:11;
reconsider n as Element of NAT by A52;
M.(ELN.n) = M.(E \(LN.n)) by A50
.=0 by A7;
hence thesis by A53,MEASURE1:def 7;
end;
then union RELN is measure_zero of M by MEASURE2:14; then
A54: M.(union RELN) = 0. by MEASURE1:def 7;
now
let x be object;
assume
A55: x in E \ (meet rng LN); then
A56: x in E by XBOOLE_0:def 5;
not x in meet rng LN by A55,XBOOLE_0:def 5;
then consider Y be set such that
A57: Y in rng LN and
A58: not x in Y by SETFAM_1:def 1;
consider m be object such that
A59: m in dom LN and
A60: Y = LN.m by A57,FUNCT_1:def 3;
reconsider m as Element of NAT by A59;
dom ELN = NAT by FUNCT_2:def 1;
then
A61: ELN.m in rng ELN by FUNCT_1:3;
ELN.m = E \ (LN.m) by A50;
then x in ELN.m by A56,A58,A60,XBOOLE_0:def 5;
hence x in union RELN by A61,TARSKI:def 4;
end;
then
A62: E \ (meet rng LN) c= union RELN;
now
let x be object;
assume x in union RELN;
then consider Y be set such that
A63: x in Y and
A64: Y in RELN by TARSKI:def 4;
consider m be object such that
A65: m in dom ELN and
A66: ELN.m = Y by A64,FUNCT_1:def 3;
reconsider m as Element of NAT by A65;
dom LN = NAT by FUNCT_2:def 1;
then
A67: LN.m in rng LN by FUNCT_1:3;
A68: Y = E \ (LN.m) by A50,A66;
then not x in LN.m by A63,XBOOLE_0:def 5;
then
A69: not x in meet(rng LN) by A67,SETFAM_1:def 1;
x in E by A63,A68,XBOOLE_0:def 5;
hence x in E \ (meet rng LN) by A69,XBOOLE_0:def 5;
end;
then union RELN c= E \ (meet rng LN);
then
A70: union RELN = E\(meet rng LN) by A62,XBOOLE_0:def 10;
rng HP is N_Sub_set_fam of X by MEASURE1:23;
then
A71: 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 be Element of S such that
A72: 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 A70,MEASURE1:33;
then M.(E\L) <= 0. by A10,A54;
then
A73: M.(E\L) = 0 by MEASURE1:def 2;
reconsider MRHP= union rng HP as Element of S by MEASURE1:24;
A74: M.(E\L \/ MRHP) <= M.(E\L) + M.MRHP by MEASURE1:33;
E\F = (E\L) \/ E /\ (union rng HP) by A72,XBOOLE_1:52;
then M.(E\F) <= M.(E\L \/ MRHP) by A51,MEASURE1:31,XBOOLE_1:9;
then M.(E\F) <= M.(E\L) + M.MRHP by A74,XXREAL_0:2;
then
A75: M.(E\F) <= M.MRHP by A73,XXREAL_3:4;
dom me =NAT by FUNCT_2:def 1;
then
A76: dom me = dom (M*HP) by FUNCT_2:def 1;
A77: for x be object st x in dom me holds me.x = (M*HP).x
proof
let x be object;
assume
A78: x in dom me;
then (M*HP).x= M.(HP.x) by A76,FUNCT_1:12;
hence thesis by A45,A78;
end;
A79: |.1/2 qua Complex.| = 1/2 by ABSVALUE:def 1;
then
A80: (1/2)GeoSeq is summable by SERIES_1:24;
then
A81: e(#)(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 A49,A76,A77,FUNCT_1:2,PROB_4:12;
then
A82: M.(union rng HP) <= Sum me by A71,MEASURE2:11;
A83: for q be Real st 0 < q ex p be Element of NAT st ((1/2) GeoSeq)
.p < q
proof
let q be Real;
assume
A84: 0 < q;
A85: lim (1/2)GeoSeq = 0 by A80,SERIES_1:4;
(1/2) GeoSeq is convergent by A80,SERIES_1:4;
then consider p be Nat such that
A86: for n be Nat st p <=n holds |.((1/2) GeoSeq).n - 0 qua Complex .|
< q by A84,A85,SEQ_2:def 7;
take p;
0 < (jj/2)|^p by PREPOWER:6;
then
A87: 0 <= ((1/2) GeoSeq).p by PREPOWER:def 1;
A88: p in NAT by ORDINAL1:def 12;
|.((1/2) GeoSeq).p- 0 qua Complex .| < q by A86;
hence thesis by A87,ABSVALUE:def 1,A88;
end;
A89: for x be Element of X st x in F holds for p be Element of NAT holds x
in L \ HP.p
proof
let x be Element of X;
assume
A90: x in F;
let p be Element of NAT;
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 thesis by A72,A90;
end;
A91: for q be Real st 0 < q ex N be Nat st for n be
Nat st N < n holds for x be Element of X st x in F holds |. (f.n).x
- g.x .| < q
proof
let q be Real;
assume 0 < q;
then consider p be Element of NAT such that
A92: ((1/2) GeoSeq).p < q by A83;
consider Np be Element of NAT such that
A93: for k be Element of NAT st Np < k holds for x be Element of X st
x in L\HP.p holds |. (fL.k).x - gL.x .| < ((1/2)GeoSeq).p by A42;
take Np;
hereby
let n be Nat;
reconsider n9 =n as Element of NAT by ORDINAL1:def 12;
assume
A94: Np < n;
hereby
let x be Element of X;
A95: fL.n= (f.n)|L by A17;
assume
A96: x in F;
then |. (fL.n9).x - gL.x .| < ((1/2)GeoSeq).p by A89,A93,A94;
then
A97: |. (fL.n).x - gL.x .| < q by A92,XXREAL_0:2;
A98: F c= L by A72,XBOOLE_1:36;
then gL.x = g.x by A96,FUNCT_1:49;
hence |. (f.n).x - g.x .| < q by A96,A97,A95,A98,FUNCT_1:49;
end;
end;
end;
Sum((1/2)GeoSeq) = 1/(1-(1/2)) by A79,SERIES_1:24;
then
A99: Sum(e(#)(1/2)GeoSeq) = e* 2 by A80,SERIES_1:10;
Sum me <= Sum(e(#)(1/2)GeoSeq) by A81,A47,SERIES_1:20;
then M.MRHP <= 2*e by A82,A99,XXREAL_0:2;
then
A100: M.(E \ F) <= e0 by A75,XXREAL_0:2;
F c= L by A72,XBOOLE_1:36;
hence thesis by A19,A100,A91,XBOOLE_1:1;
end;