:: Egoroff's Theorem
:: by Noboru Endou , Yasunari Shidama and Keiko Narita
::
:: Received October 30, 2007
:: Copyright (c) 2007 Association of Mizar Users
environ
vocabularies PARTFUN1, MEASURE1, MEASURE2, RELAT_1, ABSVALUE, FUNCT_1,
FUNCT_2, ORDINAL2, FINSEQ_4, COMPLEX1, SEQ_1, SEQ_2, SEQM_3, PREPOWER,
MEASURE6, BOOLE, ARYTM, ARYTM_1, SETFAM_1, MESFUNC1, TARSKI, ARYTM_3,
RLVECT_1, GROUP_1, PROB_1, SEQFUNC, TDGROUP, MESFUNC5, SUPINF_1,
SUPINF_2, SETLIM_1, RINFSUP1, MESFUNC8, FINSET_1, PRALG_2;
notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, COMPLEX1, XXREAL_0, SUPINF_1, PROB_1, REAL_1, SETFAM_1,
MEASURE1, KURATO_2, SETLIM_1, MEASURE2, MEASURE6, RELAT_1, FUNCT_1,
RELSET_1, PARTFUN1, RFUNCT_3, FUNCT_2, SUPINF_2, RINFSUP1, SEQFUNC,
PSCOMP_1, VALUED_1, NAT_1, SEQ_1, SEQ_4, SEQ_2, SEQM_3, NEWTON, PREPOWER,
SERIES_1, EXTREAL1, MESFUNC1, MESFUNC2, MESFUNC5, RINFSUP2, CARD_3;
constructors REAL_1, NAT_1, EXTREAL1, NEWTON, PREPOWER, SERIES_1, MESFUNC1,
PROB_2, MEASURE6, MEASURE3, PARTFUN3, KURATO_2, RINFSUP1, SETLIM_1,
MESFUNC5, RINFSUP2, SEQ_1;
registrations SUBSET_1, XREAL_0, MEMBERED, ORDINAL1, PARTFUN1, MEASURE1,
FUNCT_2, RELAT_1, XXREAL_0, XBOOLE_0, FUNCT_1, NUMBERS, VALUED_0,
VALUED_1, SETLIM_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, CARD_3, FUNCT_6, MEASURE6, RINFSUP1, SETLIM_1, XCMPLX_0,
RINFSUP2, VALUED_1;
theorems ABSVALUE, MEASURE1, MEASURE2, MEASURE3, NAT_1, TARSKI, SUPINF_1,
PARTFUN1, FUNCT_1, FUNCT_2, SEQFUNC, KURATO_2, SUPINF_2, RELSET_1,
EXTREAL1, EXTREAL2, 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, REAL_2, PROB_4,
PARTFUN2, ORDINAL1, MESFUNC5, RINFSUP2, CARD_3;
schemes SEQ_1, FUNCT_2, SEQFUNC, PARTFUN2;
begin :: Selected Properties of Functional Sequences
reserve n,k for natural number,
X for non empty set,
S for SigmaField of X;
theorem Th1:
for M be sigma_Measure of S, F be Function of NAT,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 Function of NAT,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 Function of NAT,S such that
A1: for k be Element of NAT holds E.k=Fn(k) from FUNCT_2:sch 4;
rng E is N_Sub_set_fam of X by MEASURE1:52;
then rng E is N_Measure_fam of S by MEASURE2:def 1;
then
A2: meet rng E is Element of S by MEASURE2:3;
now
let z be set;
assume z in G;
then
A3: ex x be Element of X st
z=x & for k be natural number 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 set such that
A4: l in NAT & Y=E.l by FUNCT_2:17;
reconsider l as Element of NAT by A4;
z in F.(n+l) by A3,NAT_1:12;
hence z in Y by A1,A4;
end;
hence z in meet rng E by SETFAM_1:def 1;
end;
then
A5: G c= meet rng E by TARSKI:def 3;
now
let z be set;
assume
A6: z in meet rng E;
now
let k be natural number;
assume n <= k;
then reconsider l=k-n as Element of NAT by NAT_1:21;
E.l in rng E by FUNCT_2:6;
then z in E.l by A6,SETFAM_1:def 1;
then z in F.(n+l) by A1;
hence z in F.k;
end;
hence z in G by A2,A6;
end;
then meet rng E c= G by TARSKI:def 3;
hence thesis by A2,A5,XBOOLE_0:def 10;
end;
theorem Th2:
for F be SetSequence of X, n be Element of 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 Element of NAT;
{F.k where k is Element of 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 is Element of NAT : n <= k}) by SETLIM_1:def 2;
hence (inferior_setsequence F).n = meet rng (F ^\ n) by SETLIM_1:6;
end;
theorem Th3:
for M be sigma_Measure of S, F be SetSequence of S
ex G be Function of NAT,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;
A1: dom(inferior_setsequence(F)) = NAT by FUNCT_2:def 1;
for x be set st x in NAT holds (inferior_setsequence(F)).x in S
by PROB_1:def 9;
then reconsider G= inferior_setsequence(F) as Function of NAT,S by A1,
FUNCT_2:5;
now
let n being Element of NAT;
A2: n<=n+1 by NAT_1:12;
inferior_setsequence(F) is non-decreasing by SETLIM_1:73;
hence G.n c= G.(n+1) by A2,PROB_1:def 7;
end;
then M.(union rng G)= sup rng(M*G) by MEASURE2:27;
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 Function of NAT,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;
assume
A1: M.(Union F) < +infty;
A2: dom(superior_setsequence F) = NAT by FUNCT_2:def 1;
for x be set st x in NAT holds (superior_setsequence F).x in S
by PROB_1:def 9;
then reconsider G= superior_setsequence F as Function of NAT,S by A2,
FUNCT_2:5;
A3: for n being Element of NAT holds G.(n+1) c= G.n
proof
let n be Element of NAT;
A4: n<=n+1 by NAT_1:12;
superior_setsequence F is non-increasing by SETLIM_1:72;
hence thesis by A4,PROB_1:def 6;
end;
G.0 = union {F.k where k is Element of NAT : 0 <= k} by SETLIM_1:def 3;
then G.0 = union rng F by SETLIM_1:5;
then
A5: M.(meet rng G)= inf rng(M*G) by A1,A3,MEASURE3:14;
reconsider F1 = F, G1 = G as SetSequence of X;
consider f being SetSequence of X such that
A6: lim_sup F1 = meet f &
for n being Element of NAT holds f.n = Union (F1^\n) by KURATO_2:def 4;
now
let n be Element of NAT;
f.n = Union (F1^\n) by A6;
hence f.n = G1.n by Th2;
end;
then f = G1 by FUNCT_2:113;
hence thesis by A5,A6;
end;
theorem
for M be sigma_Measure of S, F be SetSequence of S st F is convergent holds
ex G be Function of NAT,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_2:def 7;
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 Function of NAT,S st
G = superior_setsequence F & M.(lim F) = inf rng(M*G)
proof
let M be sigma_Measure of S, F be SetSequence of S;
assume
A1: F is convergent & M.(Union F) < +infty;
then lim_sup F = lim F by KURATO_2:def 7;
hence thesis by A1,Th4;
end;
definition
let X,Y be set, F be Functional_Sequence of X,Y;
attr F is with_the_same_dom means
:Def1:
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
:Def2:
for n,m be natural number holds dom(F.n) = dom(F.m);
correctness
proof
A1: F is with_the_same_dom implies
for n,m be natural number holds dom(F.n) = dom(F.m)
proof
assume F is with_the_same_dom;
then
A2: rng F is with_common_domain by Def1;
hereby
let n,m be natural number;
dom F = NAT by SEQFUNC:def 1;
then n in dom F & m in dom F by ORDINAL1:def 13;
then F.n in rng F & F.m in rng F by FUNCT_1:12;
hence dom(F.n) = dom(F.m) by A2,CARD_3:def 10;
end;
end;
(for n,m be natural number holds dom(F.n) = dom(F.m)) implies
F is with_the_same_dom
proof
assume
A3: for n,m be natural number holds dom(F.n)=dom(F.m);
now
let f,g be Function;
assume
A4: f in rng F & g in rng F;
then consider n be set such that
A5: n in dom F & f = F.n by FUNCT_1:def 5;
consider m be set such that
A6: m in dom F & g = F.m by A4,FUNCT_1:def 5;
n in NAT & m in NAT by A5,A6,SEQFUNC:def 1;
then reconsider n,m as Nat by ORDINAL1:def 13;
dom(F.n) = dom(F.m) by A3;
hence dom f = dom g by A5,A6;
end;
then rng F is with_common_domain by CARD_3:def 10;
hence F is with_the_same_dom by Def1;
end;
hence thesis by A1;
end;
end;
registration
let X,Y be set;
cluster with_the_same_dom 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 natural number;
F.n = <:{},X,Y:> & F.m = <:{},X,Y:> by A1;
hence dom(F.n) = dom(F.m);
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
deffunc F(Element of X) = inf (f#$1);
defpred P[set] means $1 in dom(f.0);
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: for x be set holds x in dom g iff x in dom(f.0) by A1;
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 8;
end;
hence thesis by A2,TARSKI:2;
end;
uniqueness
proof
let g,h be PartFunc of X,ExtREAL;
assume
A4: dom g = dom (f.0) &
for x be Element of X st x in dom g holds g.x=inf(f#x);
assume
A5: dom h = dom (f.0) &
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
A6: x in dom g;
then g/.x = g.x by PARTFUN1:def 8;
then g/.x = inf(f#x) by A4,A6;
then g/.x = h.x by A4,A5,A6;
hence g/.x = h/.x by A4,A5,A6,PARTFUN1:def 8;
end;
hence thesis by A4,A5,PARTFUN2:3;
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
deffunc F(Element of X) = sup(f#$1);
defpred P[set] means $1 in dom(f.0);
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: for x be set holds x in dom g iff x in dom(f.0) by A1;
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 8;
end;
hence thesis by A2,TARSKI:2;
end;
uniqueness
proof
let g,h be PartFunc of X,ExtREAL;
assume
A4: dom g = dom(f.0) & for x be Element of X st x in dom g holds g.x=sup(f#x);
assume
A5: dom h = dom(f.0) & 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
A6: x in dom g;
then g/.x = g.x by PARTFUN1:def 8;
then g/.x = sup(f#x) by A4,A6;
then g/.x = h.x by A4,A5,A6;
hence g/.x = h/.x by A4,A5,A6,PARTFUN1:def 8;
end;
hence thesis by A4,A5,PARTFUN2:3;
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 natural number 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
let n being Element of NAT;
deffunc F(Element of X) = (inferior_realsequence(f#$1)).n;
defpred P[set] means $1 in dom(f.0);
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: for x be set holds x in dom g iff x in dom(f.0) by A2;
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 8;
end;
hence thesis by A3,PARTFUN1:119,TARSKI:2;
end;
consider g being Function of NAT,PFuncs(X,ExtREAL) such that
A5: for n being Element of NAT holds P[n,g.n] from FUNCT_2:sch 10(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 n'=n as Element of NAT by ORDINAL1:def 13;
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' by A5;
hence thesis;
end;
A7: dom g = NAT by FUNCT_2:def 1;
for n be Element of NAT holds g.n is PartFunc of X,ExtREAL;
then reconsider g as Functional_Sequence of X,ExtREAL by A7,SEQFUNC:1;
now
let k,l be natural number;
reconsider k'=k, l'=l as Element of NAT by ORDINAL1:def 13;
dom(g.k') = dom(f.0) by A5;
then dom(g.k) = dom(g.l') 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
A8: for n be natural number 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
A9: for n be natural number 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;
A10: dom(g.n) = dom(f.0) by A8
.=dom(h.n) by A9;
now
let x be Element of X;
assume
A11: x in dom (g.n);
then (g.n)/.x = (g.n).x by PARTFUN1:def 8;
then (g.n)/.x = (inferior_realsequence (f#x)).n by A8,A11;
then (g.n)/.x = (h.n).x by A9,A10,A11;
hence (g.n)/.x = (h.n)/.x by A10,A11,PARTFUN1:def 8;
end;
hence g.n=h.n by A10,PARTFUN2:3;
end;
hence thesis by SEQFUNC:2;
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 natural number 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
let n being Element of NAT;
deffunc F(Element of X) = (superior_realsequence(f#$1)).n;
defpred P[set] means $1 in dom(f.0);
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: for x be set holds x in dom g iff x in dom(f.0) by A2;
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 8;
end;
hence thesis by A3,PARTFUN1:119,TARSKI:2;
end;
consider g being Function of NAT, PFuncs(X,ExtREAL) such that
A5: for n being Element of NAT holds P[n,g.n] from FUNCT_2:sch 10(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 n'=n as Element of NAT by ORDINAL1:def 13;
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' by A5;
hence thesis;
end;
A7: dom g = NAT by FUNCT_2:def 1;
for n be Element of NAT holds g.n is PartFunc of X,ExtREAL;
then reconsider g as Functional_Sequence of X,ExtREAL by A7,SEQFUNC:1;
now
let k,l be Nat;
reconsider k'=k, l'=l as Element of NAT by ORDINAL1:def 13;
dom(g.k') = dom(f.0) by A5;
then dom(g.k) = dom(g.l') 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
A8: 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
A9: 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;
A10: dom(g.n) = dom(f.0) by A8
.=dom(h.n) by A9;
now
let x be Element of X;
assume
A11: x in dom (g.n);
then (g.n)/.x =(g.n).x by PARTFUN1:def 8;
then (g.n)/.x =(superior_realsequence(f#x)).n by A8,A11;
then (g.n)/.x =(h.n).x by A9,A10,A11;
hence (g.n)/.x =(h.n)/.x by A10,A11,PARTFUN1:def 8;
end;
hence g.n=h.n by A10,PARTFUN2:3;
end;
hence thesis by SEQFUNC:2;
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: dom(F.n) = dom (f.0) by Def5;
(F#x).n = (F.n).x by MESFUNC5:def 13;
hence (F#x).n =(inferior_realsequence (f#x)).n by A1,A2,Def5;
end;
hence F#x = inferior_realsequence(f#x) by FUNCT_2:113;
end;
end;
definition
let X,Y be set;
redefine mode Functional_Sequence of X,Y -> Function of NAT,PFuncs(X,Y);
coherence
proof
let f be Functional_Sequence of X,Y;
dom f = NAT & rng f c= PFuncs(X,Y) by SEQFUNC:def 1;
hence thesis by FUNCT_2:4;
end;
end;
definition canceled;
:: let X,Y be set, f be Functional_Sequence of X,Y, n be Element of NAT;
:: func f^\n -> Functional_Sequence of X,Y equals
:: f^\n;
:: correctness;
end;
registration
let X,Y be set;
let f be with_the_same_dom Functional_Sequence of X,Y;
let n be Element of NAT;
cluster f^\n -> with_the_same_dom;
coherence
proof
for k,l be Nat holds dom((f^\n).k)=dom((f^\n).l)
proof
let k,l be Nat;
reconsider k'=k, l'=l as Element of NAT by ORDINAL1:def 13;
reconsider g=f as Function of NAT,PFuncs(X,Y);
dom((f^\n).k) = dom((g.(n+k'))) by KURATO_2:def 2;
then dom((f^\n).k) = dom((g.(n+l'))) by Def2;
hence dom((f^\n).k)=dom((f^\n).l) by KURATO_2:def 2;
end;
hence f^\n is with_the_same_dom by Def2;
end;
end;
theorem Th8:
for f be with_the_same_dom Functional_Sequence of X,ExtREAL,
n be Element of NAT holds (inferior_realsequence f).n = inf(f^\n)
proof
let f be with_the_same_dom Functional_Sequence of X,ExtREAL,
n be Element of NAT;
reconsider g=f as Function of NAT,PFuncs(X,ExtREAL);
A1: dom((inferior_realsequence f).n) = dom(f.0) by Def5;
dom inf(f^\n) =dom((f^\n).0) by Def3;
then dom inf(f^\n) =dom(g.(n+(0 qua Nat))) by KURATO_2:def 2;
then
A2: dom inf(f^\n) =dom(f.0) by Def2;
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 KURATO_2:def 2;
then ((f^\n)#x).k =(f#x).(n+k) by MESFUNC5:def 13;
hence ((f^\n)#x).k = ((f#x)^\n).k by KURATO_2:def 2;
end;
then (f^\n)#x = (f#x)^\n by FUNCT_2:113;
then
A4: (inf(f^\n)).x =inf((f#x)^\n) by A3,Def3;
((inferior_realsequence f).n ).x = (inferior_realsequence(f#x)).n
by A1,A2,A3,Def5;
hence (inf(f^\n)).x = ((inferior_realsequence f).n).x by A4,RINFSUP2:27;
end;
hence thesis by A1,A2,PARTFUN1:34;
end;
theorem Th9:
for f be with_the_same_dom Functional_Sequence of X,ExtREAL,
n be Element of NAT holds (superior_realsequence f).n = sup(f^\n)
proof
let f be with_the_same_dom Functional_Sequence of X,ExtREAL,
n be Element of NAT;
reconsider g=f as Function of NAT,PFuncs(X,ExtREAL);
A1: dom ((superior_realsequence f).n) = dom(f.0) by Def6;
dom sup(f^\n) = dom((f^\n).0) by Def4;
then dom sup(f^\n) = dom(g.(n+(0 qua Nat))) by KURATO_2:def 2;
then
A2: dom sup(f^\n) = dom(f.0) by Def2;
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 KURATO_2:def 2;
then ((f^\n)#x).k =(f#x).(n+k) by MESFUNC5:def 13;
hence ((f^\n)#x).k = ((f#x)^\n).k by KURATO_2:def 2;
end;
then (f^\n)#x = (f#x)^\n by FUNCT_2:113;
then
A4: (sup(f^\n)).x =sup ((f#x)^\n) by A3,Def4;
((superior_realsequence f).n ).x = (superior_realsequence (f#x)).n
by A1,A2,A3,Def6;
hence (sup (f^\n)).x = ((superior_realsequence f).n ).x by A4,RINFSUP2:27;
end;
hence thesis by A1,A2,PARTFUN1:34;
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;
assume
A1: x in dom(f.0);
set F = superior_realsequence f;
now
let n be Element of NAT;
dom(F.n) = dom(f.0) & (F#x).n = (F.n).x by Def6,MESFUNC5:def 13;
hence (F#x).n =(superior_realsequence(f#x)).n by A1,Def6;
end;
hence F#x = superior_realsequence(f#x) by FUNCT_2:113;
end;
definition
let X be non empty set, f be Functional_Sequence of X,ExtREAL;
func lim_inf 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_inf(f#x);
existence
proof
deffunc F(Element of X) = lim_inf(f#$1);
defpred P[set] means $1 in dom(f.0);
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: for x be set holds x in dom g iff x in dom(f.0) by A1;
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 8;
end;
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) &
for x be Element of X st x in dom g holds g.x=lim_inf(f#x) and
A5: dom h = dom(f.0) &
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
A6: x in dom g;
then g/.x =g.x by PARTFUN1:def 8;
then g/.x =lim_inf (f#x) by A4,A6;
then g/.x =h.x by A4,A5,A6;
hence g/.x =h/.x by A4,A5,A6,PARTFUN1:def 8;
end;
hence thesis by A4,A5,PARTFUN2:3;
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
:Def9:
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
deffunc F(Element of X) = lim_sup(f#$1);
defpred P[set] means $1 in dom(f.0);
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: for x be set holds x in dom g iff x in dom(f.0) by A1;
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 8;
end;
hence thesis by A2,TARSKI:2;
end;
uniqueness
proof
let g,h be PartFunc of X,ExtREAL;
assume
A4: dom g = dom(f.0) &
for x be Element of X st x in dom g holds g.x=lim_sup(f#x);
assume
A5: dom h = dom(f.0) &
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
A6: x in dom g;
then g/.x = g.x by PARTFUN1:def 8;
then g/.x = lim_sup (f#x) by A4,A6;
then g/.x = h.x by A4,A5,A6;
hence g/.x = h/.x by A4,A5,A6,PARTFUN1:def 8;
end;
hence thesis by A4,A5,PARTFUN2:3;
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 Def8;
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 Def8;
hence (lim_inf f).x= sup inferior_realsequence(f#x);
dom lim_inf f = dom(f.0) by Def8;
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:34;
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 Def9;
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 Def9;
hence (lim_sup f).x = inf superior_realsequence(f#x);
dom lim_sup f = dom(f.0) by Def9;
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:34;
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 x in dom(f.0);
then x in dom(lim_sup f) & x in dom(lim_inf f) by Def8,Def9;
then (lim_sup f).x = lim_sup (f#x) & (lim_inf f).x = lim_inf (f#x)
by Def8,Def9;
hence thesis by 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
:Def10:
dom it = dom (f.0) &
for x be Element of X st x in dom it holds it.x=lim(f#x);
existence
proof
deffunc F(Element of X) = lim (f#$1);
defpred P[set] means $1 in dom(f.0);
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: for x be set holds x in dom g iff x in dom(f.0) by A1;
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 8;
end;
hence thesis by A2,TARSKI:2;
end;
uniqueness
proof
let g,h be PartFunc of X,ExtREAL;
assume
A4: dom g = dom (f.0) &
for x be Element of X st x in dom g holds g.x=lim(f#x);
assume
A5: dom h = dom (f.0) &
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
A6: x in dom g;
then g/.x = g.x by PARTFUN1:def 8;
then g/.x = lim (f#x) by A4,A6;
then g/.x = h.x by A4,A5,A6;
hence g/.x = h/.x by A4,A5,A6,PARTFUN1:def 8;
end;
hence thesis by A4,A5,PARTFUN2:3;
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
A1: x in dom lim f & f#x is convergent;
then x in dom (f.0) by Def10;
then x in dom(lim_sup f) & x in dom(lim_inf f) by Def8,Def9;
then
A2: (lim_sup f).x = lim_sup (f#x) & (lim_inf f).x = lim_inf (f#x)
by Def8,Def9;
lim (f#x) = lim_sup (f#x) & lim (f#x) = lim_inf (f#x) by A1,RINFSUP2:41;
hence thesis by A1,A2,Def10;
end;
theorem Th15:
for f be with_the_same_dom Functional_Sequence of X,ExtREAL,
F be SetSequence of S, r be real number st
(for n be natural number holds F.n = dom(f.0) /\ great_dom(f.n,R_EAL r))
holds union rng F = dom(f.0) /\ great_dom(sup f,R_EAL r)
proof
let f be with_the_same_dom Functional_Sequence of X,ExtREAL,
F be SetSequence of S, r be real number;
set E = dom(f.0);
assume
A1: for n be natural number holds F.n = E /\ great_dom(f.n,R_EAL r);
now
let x be set;
assume x in union rng F;
then consider y be set such that
A2: x in y & y in rng F by TARSKI:def 4;
consider n be set such that
A3: n in dom F & y=F.n by A2,FUNCT_1:def 5;
reconsider z=x as Element of X by A2;
reconsider n as Element of NAT by A3;
F.n = E /\ great_dom(f.n,R_EAL r) by A1;
then
A4: x in E & x in great_dom(f.n,r) by A2,A3,XBOOLE_0:def 3;
then
A5: r < (f.n).z by MESFUNC1:def 14;
A6: x in dom (sup f) by A4,Def4;
then
A7: (sup f).z = sup(f#z) by Def4;
(f.n).z=(f#z).n by MESFUNC5:def 13;
then (f.n).z <= (sup f).z by A7,RINFSUP2:23;
then R_EAL r < (sup f).z by A5,XXREAL_0:2;
then x in great_dom(sup f,R_EAL r) by A6,MESFUNC1:def 14;
hence x in E /\ great_dom(sup f,R_EAL r) by A4,XBOOLE_0:def 3;
end;
then
A8: union rng F c= E /\ great_dom(sup f,R_EAL r) by TARSKI:def 3;
now
let x be set;
assume
A9: x in E /\ great_dom(sup f,R_EAL r);
then reconsider z=x as Element of X;
A10: x in E & x in great_dom(sup f,R_EAL r) by A9,XBOOLE_0:def 3;
then
A11: R_EAL r < (sup f).z by MESFUNC1:def 14;
ex n be Element of NAT st R_EAL r < (f.n).z
proof
assume
A12: for n be Element of NAT holds (f.n).z <= R_EAL r;
for x be ext-real number st x in rng (f#z) holds x <= R_EAL r
proof
let x be ext-real number;
assume x in rng (f#z);
then consider m be set such that
A13: m in NAT & x=(f#z).m by FUNCT_2:17;
reconsider m as Element of NAT by A13;
x=(f.m).z by A13,MESFUNC5:def 13;
hence thesis by A12;
end;
then R_EAL r is majorant of rng (f#z) by SUPINF_1:def 9;
then
A14: sup (f#z) <= R_EAL r by SUPINF_1:def 16;
x in dom (sup f) by A10,Def4;
hence contradiction by A11,A14,Def4;
end;
then consider n be Element of NAT such that
A15: R_EAL r < (f.n).z;
x in dom (f.n) by A10,Def2;
then
A16: x in E & x in great_dom(f.n,R_EAL r)
by A9,A15,MESFUNC1:def 14,XBOOLE_0:def 3;
F.n = E /\ great_dom(f.n,R_EAL r) by A1;
then
A17: x in F.n by A16,XBOOLE_0:def 3;
F.n in rng F by FUNCT_2:6;
hence x in union rng F by A17,TARSKI:def 4;
end;
then E /\ great_dom((sup f),R_EAL r) c= union rng F by TARSKI:def 3;
hence union rng F = E /\ great_dom(sup f,R_EAL r) by A8,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 number st
(for n be natural number holds F.n = dom(f.0) /\ great_eq_dom(f.n,R_EAL r))
holds meet rng F = dom(f.0) /\ great_eq_dom(inf f,R_EAL r)
proof
let f be with_the_same_dom Functional_Sequence of X,ExtREAL,
F be SetSequence of S, r be real number;
assume
A1: for n be natural number holds F.n = dom(f.0) /\ great_eq_dom(f.n,R_EAL r);
set E = dom(f.0);
now
let x be set;
assume
A2: x in meet rng F;
then reconsider z=x as Element of X;
F.0 in rng F by FUNCT_2:6;
then
A3: x in F.0 by A2,SETFAM_1:def 1;
F.0 = E /\ great_eq_dom(f.0,R_EAL r) by A1;
then
A4: x in E & x in great_eq_dom(f.0,R_EAL r) by A3,XBOOLE_0:def 3;
A5: now
let n be Element of NAT;
F.n in rng F by FUNCT_2:6;
then
A6: z in F.n by A2,SETFAM_1:def 1;
F.n = E /\ great_eq_dom(f.n,R_EAL r) by A1;
then z in E & x in great_eq_dom(f.n,R_EAL r) by A6,XBOOLE_0:def 3;
then R_EAL r <= (f.n).z by MESFUNC1:def 15;
hence R_EAL r <= (f#z).n by MESFUNC5:def 13;
end;
now
let s be ext-real number;
assume s in rng (f#z);
then ex k be set st k in NAT & s=(f#z).k by FUNCT_2:17;
hence R_EAL r <= s by A5;
end;
then R_EAL r is minorant of rng (f#z) by SUPINF_1:def 10;
then
A7: R_EAL r <= inf (f#z) by SUPINF_1:def 17;
A8: x in dom (inf f) by A4,Def3;
then R_EAL r <= (inf f).x by A7,Def3;
then x in great_eq_dom(inf f,R_EAL r) by A8,MESFUNC1:def 15;
hence x in E /\ great_eq_dom(inf f,R_EAL r) by A4,XBOOLE_0:def 3;
end;
then
A9: meet rng F c= E /\ great_eq_dom(inf f,R_EAL r) by TARSKI:def 3;
now
let x be set;
assume
A10: x in E /\ great_eq_dom(inf f,R_EAL r);
then reconsider z=x as Element of X;
A11: x in E & x in great_eq_dom(inf f,R_EAL r) by A10,XBOOLE_0:def 3;
then
A12: R_EAL r <= (inf f).z by MESFUNC1:def 15;
now
let y be set;
assume y in rng F;
then consider n be set such that
A13: n in NAT & y=F.n by FUNCT_2:17;
reconsider n as Element of NAT by A13;
x in dom inf f by A11,Def3;
then
A14: (inf f).z = inf(f#z) by Def3;
(f.n).z=(f#z).n by MESFUNC5:def 13;
then inf (f#z)<= (f.n).z by RINFSUP2:23;
then
A15: R_EAL r <= (f.n).z by A12,A14,XXREAL_0:2;
x in dom (f.n) by A11,Def2;
then
A16: x in E & x in great_eq_dom(f.n,R_EAL r)
by A10,A15,MESFUNC1:def 15,XBOOLE_0:def 3;
F.n = E /\ great_eq_dom(f.n,R_EAL r) by A1;
hence x in y by A13,A16,XBOOLE_0:def 3;
end;
hence x in meet rng F by SETFAM_1:def 1;
end;
then E /\ great_eq_dom((inf f),R_EAL r) c= meet rng F by TARSKI:def 3;
hence meet rng F = E /\ great_eq_dom(inf f,R_EAL r) by A9,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 number st
(for n be natural number holds F.n = dom(f.0) /\ great_dom(f.n,R_EAL r))
holds for n be natural number holds (superior_setsequence F).n
= dom(f.0) /\ great_dom((superior_realsequence f).n,R_EAL r)
proof
let f be with_the_same_dom Functional_Sequence of X,ExtREAL,
F be SetSequence of S, r be real number;
set E = dom(f.0);
assume
A1: for n be natural number holds F.n = E /\ great_dom(f.n,R_EAL r);
let n be natural number;
reconsider n'=n as Element of NAT by ORDINAL1:def 13;
set f1=f^\n';
set F1=F^\n';
now
let k be Element of NAT;
F1.k= F.(n+k) by KURATO_2:def 2;
hence F1.k in S by PROB_1:def 9;
end;
then
A2: F1 is SetSequence of S by PROB_1:def 9;
consider g be Function of NAT,PFuncs(X,ExtREAL) such that
A3: f=g & f^\n'=g^\n';
f1.0 = g.(n+(0 qua Nat)) by A3,KURATO_2:def 2;
then
A4: dom(f1.0)= E by A3,Def2;
now
let k be natural number;
reconsider k'=k as Element of NAT by ORDINAL1:def 13;
F1.k = F.(n+k') by KURATO_2:def 2;
then F1.k = E /\ great_dom(f.(n+k'),R_EAL r) by A1;
hence F1.k = E /\ great_dom(f1.k,R_EAL r) by KURATO_2:def 2;
end;
then
A5: union rng F1 = E /\ great_dom(sup f1,R_EAL r) by A2,A4,Th15;
union rng (F^\n') = (superior_setsequence F).n by Th2;
hence thesis by A5,Th9;
end;
theorem Th18:
for f be with_the_same_dom Functional_Sequence of X,ExtREAL,
F be SetSequence of S, r be real number st
(for n be natural number holds F.n = dom(f.0) /\ great_eq_dom(f.n,R_EAL r))
holds for n be natural number holds (inferior_setsequence F).n
= dom(f.0) /\ great_eq_dom((inferior_realsequence f).n,R_EAL r)
proof
let f be with_the_same_dom Functional_Sequence of X,ExtREAL,
F be SetSequence of S, r be real number;
set E = dom(f.0);
assume that
A1: for n be natural number holds F.n = E /\ great_eq_dom(f.n,R_EAL r);
let n be natural number;
reconsider n'=n as Element of NAT by ORDINAL1:def 13;
set f1=f^\n';
set F1=F^\n';
now
let k be Element of NAT;
F1.k= F.(n+k) by KURATO_2:def 2;
hence F1.k in S by PROB_1:def 9;
end;
then
A2: F1 is SetSequence of S by PROB_1:def 9;
consider g be Function of NAT,PFuncs(X,ExtREAL) such that
A3: f=g & f^\n'=g^\n';
f1.0 = g.(n+(0 qua Nat)) by A3,KURATO_2:def 2;
then
A4: dom(f1.0) = E by A3,Def2;
now
let k be natural number;
reconsider k'=k as Element of NAT by ORDINAL1:def 13;
F1.k = F.(n+k') by KURATO_2:def 2;
then F1.k = E /\ great_eq_dom(f.(n+k'),R_EAL r) by A1;
hence F1.k = E /\ great_eq_dom(f1.k,R_EAL r) by KURATO_2:def 2;
end;
then
A5: meet rng F1 = E /\ great_eq_dom(inf f1,R_EAL r) by A2,A4,Th16;
meet rng(F^\n') = (inferior_setsequence F).n by Th2;
hence thesis by A5,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 natural number holds f.n is_measurable_on E) holds
for n holds (superior_realsequence f).n is_measurable_on E
proof
let f be with_the_same_dom Functional_Sequence of X,ExtREAL,
E be Element of S;
assume
A1: dom (f.0) = E & for n be natural number holds f.n is_measurable_on E;
let n;
reconsider n'=n as Element of NAT by ORDINAL1:def 13;
A2: dom((superior_realsequence f).n') = E by A1,Def6;
now
let r be real number;
deffunc G(Element of NAT) = E /\ great_dom(f.$1,R_EAL r);
consider F being Function of NAT,bool X such that
A3: for x being Element of NAT holds F.x = G(x) from FUNCT_2:sch 4;
A4: for x being natural number holds F.x = E /\ great_dom(f.x,R_EAL r)
proof
let x be natural number;
reconsider x'=x as Element of NAT by ORDINAL1:def 13;
F.x' = E /\ great_dom(f.x',R_EAL r) by A3;
hence thesis;
end;
now
let i be Element of NAT;
A5: F.i=E /\ great_dom(f.i,R_EAL r) by A3;
A6: f.i is_measurable_on E by A1;
dom (f.i) = E by A1,Def2;
hence F.i in S by A5,A6,MESFUNC1:33;
end;
then reconsider F as SetSequence of S by PROB_1:def 9;
for x be set st x in NAT holds (superior_setsequence F).x in S
by PROB_1:def 9;
then (superior_setsequence F).n' in S;
hence E /\ great_dom((superior_realsequence f).n,R_EAL r) is_measurable_on
S by A1,A4,Th17;
end;
hence (superior_realsequence f).n is_measurable_on E by A2,MESFUNC1:33;
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 natural number holds f.n is_measurable_on E) holds
for n be natural number holds (inferior_realsequence f).n is_measurable_on E
proof
let f be with_the_same_dom Functional_Sequence of X,ExtREAL,
E be Element of S;
assume
A1: dom(f.0) = E & for n be natural number holds f.n is_measurable_on E;
let n be natural number;
reconsider n'=n as Element of NAT by ORDINAL1:def 13;
A2: dom((inferior_realsequence f).n') = E by A1,Def5;
now
let r be real number;
deffunc G(Element of NAT) = E /\ great_eq_dom(f.$1,R_EAL r);
consider F being Function of NAT,bool X such that
A3: for x being Element of NAT holds F.x = G(x) from FUNCT_2:sch 4;
A4: for x being natural number holds F.x = E /\ great_eq_dom(f.x,R_EAL r)
proof
let x be natural number;
reconsider x'=x as Element of NAT by ORDINAL1:def 13;
F.x' = E /\ great_eq_dom(f.x',R_EAL r) by A3;
hence thesis;
end;
now
let i be Element of NAT;
A5: F.i=E /\ great_eq_dom(f.i,R_EAL r) by A3;
A6: f.i is_measurable_on E by A1;
dom (f.i) = E by A1,Def2;
hence F.i in S by A5,A6,MESFUNC1:31;
end;
then reconsider F as SetSequence of S by PROB_1:def 9;
for x be set st x in NAT holds (inferior_setsequence F).x in S
by PROB_1:def 9;
then (inferior_setsequence F).n' in S;
hence E /\ great_eq_dom((inferior_realsequence f).n,R_EAL r )
is_measurable_on S by A1,A4,Th18;
end;
hence (inferior_realsequence f).n is_measurable_on E by A2,MESFUNC1:31;
end;
theorem Th21:
for f be Functional_Sequence of X,ExtREAL, F be SetSequence of S,
r be real number st (for n be natural number holds
F.n = dom(f.0) /\ great_eq_dom((superior_realsequence f).n,R_EAL r)) holds
meet F = dom(f.0) /\ great_eq_dom(lim_sup f,R_EAL r)
proof
let f be Functional_Sequence of X,ExtREAL, F be SetSequence of S,
r be real number;
set E = dom(f.0);
set g=superior_realsequence f;
assume
A1: for n be natural number holds F.n = E /\ great_eq_dom(g.n,R_EAL r);
dom(g.0) = dom(f.0) by Def6;
then meet rng F = E /\ great_eq_dom(inf g,R_EAL 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 number st (for n be natural number holds
F.n= dom(f.0) /\ great_dom((inferior_realsequence f).n,R_EAL r)) holds
union rng F = dom(f.0) /\ great_dom(lim_inf f,R_EAL r)
proof
let f be Functional_Sequence of X,ExtREAL, F be SetSequence of S,
r be real number;
set E = dom(f.0);
set g=inferior_realsequence f;
assume
A1: for n be natural number holds F.n = E /\ great_dom(g.n,R_EAL r);
dom(g.0) = dom(f.0) by Def5;
then union rng F = E /\ great_dom(sup g,R_EAL 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 natural number holds f.n is_measurable_on E) holds
lim_sup f is_measurable_on E
proof
let f be with_the_same_dom Functional_Sequence of X,ExtREAL,
E be Element of S;
assume
A1: dom (f.0) = E & for n be natural number holds f.n is_measurable_on E;
A2: dom (lim_sup f) = dom(f.0) by Def9;
now
let r be real number;
deffunc G(Element of NAT)
= E /\ great_eq_dom((superior_realsequence f).$1,R_EAL r);
consider F being Function of NAT,bool X such that
A3: for x being Element of NAT holds F.x = G(x) from FUNCT_2:sch 4;
A4: for x being natural number holds
F.x = E /\ great_eq_dom((superior_realsequence f).x,R_EAL r)
proof
let x be natural number;
reconsider x'=x as Element of NAT by ORDINAL1:def 13;
F.x' = E /\ great_eq_dom((superior_realsequence f).x',R_EAL r) by A3;
hence thesis;
end;
now
let i be Element of NAT;
A5: F.i = E /\ great_eq_dom((superior_realsequence f).i,R_EAL r) by A3;
A6: (superior_realsequence f).i is_measurable_on E by A1,Th19;
dom((superior_realsequence f).i) = dom(f.0) by Def6;
hence F.i in S by A1,A5,A6,MESFUNC1:31;
end;
then reconsider F as SetSequence of S by PROB_1:def 9;
A7: meet F = E /\ great_eq_dom(lim_sup f,R_EAL r) by A1,A4,Th21;
A8: dom F = NAT by FUNCT_2:def 1;
for x be set st x in NAT holds F.x in S by PROB_1:def 9;
then
A9: F is Function of NAT,S by A8,FUNCT_2:5;
then
A10: rng F is N_Sub_set_fam of X by MEASURE1:52;
rng F c= S by A9,RELSET_1:12;
then rng F is N_Measure_fam of S by A10,MEASURE2:def 1;
hence E /\ great_eq_dom(lim_sup f,R_EAL r) is_measurable_on S by A7,
MEASURE2:3;
end;
hence lim_sup f is_measurable_on E by A1,A2,MESFUNC1:31;
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 natural number holds f.n is_measurable_on E) holds
lim_inf f is_measurable_on E
proof
let f be with_the_same_dom Functional_Sequence of X,ExtREAL,
E be Element of S;
assume
A1: dom(f.0) = E & for n be natural number holds f.n is_measurable_on E;
then
A2: dom lim_inf f = E by Def8;
now
let r be real number;
deffunc G(Element of NAT)
= E /\ great_dom((inferior_realsequence f).$1,R_EAL r);
consider F being Function of NAT,bool X such that
A3: for x being Element of NAT holds F.x = G(x) from FUNCT_2:sch 4;
A4: for x be natural number holds
F.x = E /\ great_dom((inferior_realsequence f).x,R_EAL r)
proof
let x be natural number;
reconsider x'=x as Element of NAT by ORDINAL1:def 13;
F.x' = E /\ great_dom((inferior_realsequence f).x',R_EAL r) by A3;
hence thesis;
end;
now
let i be Element of NAT;
A5: F.i = E /\ great_dom((inferior_realsequence f).i,R_EAL r) by A3;
A6: (inferior_realsequence f).i is_measurable_on E by A1,Th20;
dom((inferior_realsequence f).i) = E by A1,Def5;
hence F.i in S by A5,A6,MESFUNC1:33;
end;
then reconsider F as SetSequence of S by PROB_1:def 9;
A7: union rng F = E /\ great_dom(lim_inf f,R_EAL r) by A1,A4,Th22;
A8: dom F = NAT by FUNCT_2:def 1;
for x be set st x in NAT holds F.x in S by PROB_1:def 9;
then
A9: F is Function of NAT,S by A8,FUNCT_2:5;
then
A10: rng F c= S by RELSET_1:12;
rng F is N_Sub_set_fam of X by A9,MEASURE1:52;
then rng F is N_Measure_fam of S by A10,MEASURE2:def 1;
hence E /\ great_dom(lim_inf f,R_EAL r) is_measurable_on S by A7,MEASURE2:3;
end;
hence lim_inf f is_measurable_on E by A2,MESFUNC1:33;
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 natural number holds f.n is_measurable_on E) &
(for x be Element of X st x in E holds f#x is convergent) holds
lim f is_measurable_on E
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 f = E & dom lim_sup f = E by Def9,Def10;
assume that
A3: for n be natural number holds f.n is_measurable_on E and
A4: for x be Element of X st x in E holds f#x is convergent;
A5: now
let x be Element of X;
assume
A6: x in dom lim f;
then f#x is convergent by A2,A4;
hence (lim f).x= (lim_sup f).x by A6,Th14;
end;
lim_sup f is_measurable_on E by A1,A3,Th23;
hence thesis by A2,A5,PARTFUN1:34;
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 natural number holds f.n is_measurable_on E) & 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_measurable_on E
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 & for n be natural number holds f.n is_measurable_on E and
A2: dom g = E and
A3: for x be Element of X st x in E holds f#x is convergent & g.x = lim(f#x);
A4: for x be Element of X st x in E holds f#x is convergent by A3;
A5: dom lim f = E by A1,Def10;
now
let x be Element of X;
assume
A6: x in dom lim f;
then g.x= lim(f#x) by A3,A5;
hence g.x = (lim f).x by A6,Def10;
end;
then g = lim f by A2,A5,PARTFUN1:34;
hence thesis by A1,A4,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 finite
proof
let f be Functional_Sequence of X,ExtREAL, g be PartFunc of X,ExtREAL;
assume that
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: f#x is convergent_to_finite_number & g.x = lim (f#x) by A1;
then
A4: f#x is convergent by MESFUNC5:def 11;
not (lim (f#x)=-infty & f#x is convergent_to_-infty ) &
not (lim (f#x)=+infty & f#x is convergent_to_+infty )
by A3,MESFUNC5:56,57;
then consider g0 be real number such that
A5: lim (f#x) = g0 & (for p be real number st 0