:: Kolmogorov's Zero-one Law
:: by Agnes Doll
::
:: Received November 4, 2008
:: Copyright (c) 2008-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, SETFAM_1, SUBSET_1, RPR_1, FUNCT_1,
TARSKI, RELAT_1, REAL_1, CARD_1, ARYTM_1, CARD_3, PROB_3, NAT_1, ARYTM_3,
ZFMISC_1, PROB_2, DYNKIN, VALUED_1, XXREAL_0, SERIES_1, ORDINAL2,
FUNCOP_1, FINSEQ_1, FINSET_1, FINSUB_1, SETWISEO, ORDINAL4, EQREL_1,
KOLMOG01;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REAL_1, ORDINAL1, XCMPLX_0,
XXREAL_0, NAT_1, XREAL_0, NUMBERS, FINSET_1, DYNKIN, FINSUB_1, RELAT_1,
CARD_3, SEQ_2, SETFAM_1, FUNCT_1, RELSET_1, VALUED_1, FINSEQ_1, RVSUM_1,
PARTFUN1, FUNCT_2, PROB_3, SERIES_1, FUNCOP_1, SETWISEO, FINSEQOP,
KURATO_0, PROB_1, PROB_2;
constructors SEQ_2, DYNKIN, REAL_1, PROB_3, SERIES_1, KURATO_0, RINFSUP1,
SETFAM_1, BINOP_2, RVSUM_1, WELLORD2, FINSEQOP, SETWISEO, RELSET_1,
MEASURE1, COMSEQ_2;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, VALUED_1, RELSET_1, NUMBERS,
XREAL_0, MEMBERED, PROB_1, RELAT_1, FINSET_1, FINSEQ_1, FINSUB_1,
FUNCT_1, FUNCT_2, VALUED_0, PROB_3;
requirements SUBSET, NUMERALS, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0;
equalities PROB_1, SUBSET_1, XBOOLE_0, CARD_3;
expansions PROB_1, TARSKI, XBOOLE_0;
theorems XCMPLX_1, PROB_1, TARSKI, SUBSET_1, XBOOLE_0, DYNKIN, ZFMISC_1,
PROB_2, XBOOLE_1, SERIES_1, PROB_3, PROB_4, FUNCT_1, FUNCT_2, SEQ_1,
SEQ_2, RELAT_1, SETFAM_1, CARD_5, FINSUB_1, FINSEQ_1, FINSEQ_2, FINSEQ_3,
RVSUM_1, ORDINAL1, WELLORD2, FINSEQOP, NAT_1, VALUED_0, FUNCOP_1,
RELSET_1;
schemes NAT_1, XBOOLE_0, SETWISEO, PARTFUN1, FUNCT_2, XFAMILY;
begin
reserve Omega, I for non empty set;
reserve Sigma for SigmaField of Omega;
reserve P for Probability of Sigma;
reserve D, E, F for Subset-Family of Omega;
reserve B, sB for non empty Subset of Sigma;
reserve b for Element of B;
reserve a for Element of Sigma;
reserve p, q, u, v for Event of Sigma;
reserve n, m for Element of NAT;
reserve S, S9, X, x, y, z, i, j for set;
theorem Th1:
for f being Function, X being set st X c= dom f holds X <> {}
implies rng (f|X) <> {}
proof
let f be Function, X be set;
assume
A1: X c= dom f;
set x = the Element of X;
assume X <> {};
then x in X;
hence thesis by A1,FUNCT_1:50;
end;
theorem Th2:
for r being Real st r*r=r holds r=0 or r=1
proof
let r be Real;
assume r*r=r;
then r*(r-1)=0;
then r=0 or r-1=0 by XCMPLX_1:6;
hence thesis;
end;
theorem Th3:
for X being Subset-Family of Omega st X={} holds sigma(X) = {{}, Omega}
proof
let X be Subset-Family of Omega;
A1: for A1 being SetSequence of Omega st rng A1 c= {{},Omega} holds Union A1
in {{},Omega}
proof
let A1 be SetSequence of Omega;
assume
A2: rng A1 c= {{},Omega};
A3: for n being Nat
holds ((Partial_Union A1).n = {} or (Partial_Union A1).n = Omega )
proof
defpred P[Nat] means (Partial_Union A1).$1 = {} or (Partial_Union A1).$1
= Omega;
let n be Nat;
A4: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A5: (Partial_Union A1).k = {} or (Partial_Union A1).k = Omega;
reconsider k as Element of NAT by ORDINAL1:def 12;
A6: A1.(k+1) in rng A1 by NAT_1:51;
per cases by A5,PROB_3:def 2;
suppose
(Partial_Union A1).(k+1) = {} \/ A1.(k+1);
hence thesis by A2,A6,TARSKI:def 2;
end;
suppose
A7: (Partial_Union A1).(k+1) = Omega \/ A1.(k+1);
A1.(k+1) = {} or A1.(k+1) = Omega by A2,A6,TARSKI:def 2;
hence thesis by A7;
end;
end;
(Partial_Union A1).0 = A1.0 & A1.0 in rng A1 by NAT_1:51,PROB_3:def 2;
then
A8: P[0] by A2,TARSKI:def 2;
for k being Nat holds P[k] from NAT_1:sch 2(A8,A4);
hence thesis;
end;
Union Partial_Union A1 = {} or Union Partial_Union A1 = Omega
proof
per cases;
suppose
A9: for n being Nat holds (Partial_Union A1).n = {};
not ex x being object st x in Union Partial_Union A1
proof
given x being object such that
A10: x in Union Partial_Union A1;
reconsider x as set by TARSKI:1;
ex n being Nat st x in (Partial_Union A1).n by PROB_1:12,A10;
hence contradiction by A9;
end;
hence thesis by XBOOLE_0:def 1;
end;
suppose
not for n being Nat holds (Partial_Union A1).n = {};
then consider n being Nat such that
A11: (Partial_Union A1).n <> {};
(Partial_Union A1).n = Omega by A3,A11;
then for x being object holds
x in Omega implies x in Union Partial_Union A1 by PROB_1:12;
then Omega c= Union Partial_Union A1;
hence thesis;
end;
end;
then Union A1 = {} or Union A1 = Omega by PROB_3:15;
hence thesis by TARSKI:def 2;
end;
A12: for A being Subset of Omega st A in {{},Omega} holds A` in {{},Omega}
proof
let A be Subset of Omega;
assume A in {{},Omega};
then A={} or A=Omega by TARSKI:def 2;
then A`=Omega or A`={} by XBOOLE_1:37;
hence thesis by TARSKI:def 2;
end;
{} in sigma(X) & Omega in sigma(X) by PROB_1:4,5;
then for x being object holds
x in {{},Omega} implies x in sigma(X) by TARSKI:def 2;
then
A13: {{},Omega} c= sigma(X);
assume X={};
then
A14: X c= {{},Omega};
for x being object holds x in {{},Omega} implies x in bool Omega
proof let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in {{},Omega};
then x={} or x=Omega by TARSKI:def 2;
then xx c= Omega;
hence thesis;
end;
then {{},Omega} is SigmaField of Omega by A1,A12,PROB_4:4,TARSKI:def 3;
then sigma(X) c= {{},Omega} by A14,PROB_1:def 9;
hence thesis by A13;
end;
definition
let Omega be non empty set, Sigma be SigmaField of Omega, B be Subset of
Sigma, P be Probability of Sigma;
func Indep(B,P) -> Subset of Sigma means
:Def1:
for a being Element of Sigma
holds a in it iff for b being Element of B holds P.(a /\ b) = P.a * P.b;
existence
proof
defpred P[set] means for b being Element of B holds P.($1 /\ b) = P.$1 * P
.b;
consider X such that
A1: for x holds x in X iff x in Sigma & P[x] from XFAMILY:sch 1;
for x being object holds x in X implies x in Sigma by A1;
then reconsider X as Subset of Sigma by TARSKI:def 3;
take X;
let a be Element of Sigma;
thus thesis by A1;
end;
uniqueness
proof
let X1, X2 be Subset of Sigma;
assume
A2: for a being Element of Sigma holds a in X1 iff for b being Element
of B holds P.(a /\ b) = P.a * P.b;
assume
A3: for a being Element of Sigma holds a in X2 iff for b being Element
of B holds P.(a /\ b) = P.a * P.b;
now
let a be Element of Sigma;
a in X1 iff for b being Element of B holds P.(a /\ b) = P.a * P.b by A2;
hence a in X1 iff a in X2 by A3;
end;
hence thesis by SUBSET_1:3;
end;
end;
theorem Th4:
for f being SetSequence of Sigma holds (for n,b holds P.(f.n /\ b
) = P.(f.n) * P.b) & f is disjoint_valued implies P.(b /\ Union f) = P.b * P.
Union f
proof
let f be SetSequence of Sigma;
reconsider b as Element of Sigma;
reconsider r=P.b as Real;
for n being Nat holds seqIntersection(b,f).n is Event of Sigma
proof
let n be Nat;
A1: n in NAT by ORDINAL1:def 12;
b /\ f.n is Event of Sigma;
hence thesis by DYNKIN:def 1,A1;
end;
then reconsider seqIntf=seqIntersection(b,f) as SetSequence of Sigma by
PROB_1:25;
for n being Nat
holds seqIntersection(b,Partial_Union f).n is Event of Sigma
proof
let n be Nat;
A2: n in NAT by ORDINAL1:def 12;
b /\ (Partial_Union f).n is Event of Sigma;
hence thesis by DYNKIN:def 1,A2;
end;
then reconsider
seqIntPf = seqIntersection(b,Partial_Union f) as SetSequence of
Sigma by PROB_1:25;
A3: b /\ Union f = b /\ Union Partial_Union f by PROB_3:15
.= Union seqIntPf by DYNKIN:10;
assume
A4: for n,b holds P.(f.n /\ b) = P.(f.n) * P.b;
now
let n be Element of NAT;
thus (P*seqIntf).n = P.(seqIntf.n) by FUNCT_2:15
.= P.(f.n /\ b) by DYNKIN:def 1
.= P.(f.n) * P.b by A4
.= (P*f).n * r by FUNCT_2:15
.= (r(#)(P*f)).n by SEQ_1:9;
end;
then
A5: P*seqIntf = r(#)(P*f) by FUNCT_2:def 7;
A6: for n,m st n <= m holds x in (Partial_Union f).n implies x in (
Partial_Union f).m
proof
reconsider Pf = Partial_Union f as SetSequence of Sigma;
let n,m;
assume
A7: n <= m;
assume
A8: x in (Partial_Union f).n;
Pf is non-descending by PROB_3:11;
then Pf.n c= Pf.m by A7;
hence thesis by A8;
end;
for n,m being Nat st n <= m
holds seqIntersection(b,Partial_Union f).n c=
seqIntersection(b,Partial_Union f).m
proof
let n,m be Nat;
assume
A9: n <= m;
A10: m in NAT by ORDINAL1:def 12;
A11: n in NAT by ORDINAL1:def 12;
let x be object;
assume x in seqIntersection(b,Partial_Union f).n;
then
A12: x in b /\ (Partial_Union f).n by DYNKIN:def 1,A11;
then x in (Partial_Union f).n by XBOOLE_0:def 4;
then
A13: x in (Partial_Union f).m by A6,A9,A11,A10;
x in b by A12,XBOOLE_0:def 4;
then x in b /\ (Partial_Union f).m by A13,XBOOLE_0:def 4;
hence thesis by DYNKIN:def 1,A10;
end;
then
A14: seqIntersection(b,Partial_Union f) is non-descending;
assume
A15: f is disjoint_valued;
then
A16: seqIntersection(b,f) is disjoint_valued by DYNKIN:9;
for n holds (Partial_Union seqIntf).n = seqIntersection(b,
Partial_Union f).n
proof
defpred P[Nat] means (Partial_Union seqIntf).$1 = seqIntersection(b,
Partial_Union f).$1;
let n;
A17: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A18: (Partial_Union seqIntf).k = seqIntersection(b,Partial_Union f ).k;
reconsider k as Element of NAT by ORDINAL1:def 12;
(Partial_Union seqIntf).(k+1) = (Partial_Union seqIntf).k \/
seqIntf.(k+1) by PROB_3:def 2
.= (b /\ (Partial_Union f).k) \/ seqIntf.(k+1) by A18,DYNKIN:def 1
.= (b /\ (Partial_Union f).k) \/ (b /\ f.(k+1)) by DYNKIN:def 1
.= b /\ ((Partial_Union f).k \/ f.(k+1)) by XBOOLE_1:23
.= b /\ (Partial_Union f).(k+1) by PROB_3:def 2
.= seqIntersection(b,Partial_Union f).(k+1) by DYNKIN:def 1;
hence thesis;
end;
(Partial_Union seqIntf).0 = seqIntf.0 by PROB_3:def 2
.= b /\ f.0 by DYNKIN:def 1
.= b /\ (Partial_Union f).0 by PROB_3:def 2
.= seqIntersection(b,Partial_Union f).0 by DYNKIN:def 1;
then
A19: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A19,A17);
hence thesis;
end;
then
P * seqIntersection(b,Partial_Union f) = P * Partial_Union seqIntf by
FUNCT_2:63
.= Partial_Sums (P*seqIntf) by A16,PROB_3:44
.= r(#)Partial_Sums(P*f) by A5,SERIES_1:9
.= r(#)(P * Partial_Union f) by A15,PROB_3:44;
then r * lim (P*Partial_Union f) = lim (P*seqIntPf) by PROB_3:41,SEQ_2:8
.=P.(b /\ Union f) by A14,A3,PROB_2:10;
hence thesis by PROB_3:41;
end;
theorem Th5:
Indep(B,P) is Dynkin_System of Omega
proof
A1: for b holds P.({} /\ b) = P.{} * P.b
proof
let b;
reconsider b as Event of Sigma;
P.({} /\ b) = 0 by VALUED_0:def 19;
hence thesis;
end;
reconsider Indp=Indep(B,P) as Subset-Family of Omega by XBOOLE_1:1;
{} is Element of Sigma by PROB_1:22;
then
A2: {} in Indep(B,P) by A1,Def1;
A3: for g being SetSequence of Omega st rng g c= Indep(B,P) & g is
disjoint_valued holds Union g in Indep(B,P)
proof
let g be SetSequence of Omega;
assume that
A4: rng g c= Indep(B,P) and
A5: g is disjoint_valued;
now
let n be Nat;
g.n is Element of Sigma
proof
per cases;
suppose
n in dom g;
then g.n in rng g by FUNCT_1:3;
hence thesis by A4,TARSKI:def 3;
end;
suppose
not n in dom g;
then g.n = {} by FUNCT_1:def 2;
hence thesis by PROB_1:4;
end;
end;
hence g.n is Event of Sigma;
end;
then reconsider g as SetSequence of Sigma by PROB_1:25;
reconsider Ug = Union g as Element of Sigma by PROB_1:26;
for n,b holds P.(g.n /\ b) = P.(g.n) * P.b
proof
let n,b;
g.n in Indep(B,P)
proof
per cases;
suppose
n in dom g;
then g.n in rng g by FUNCT_1:3;
hence thesis by A4;
end;
suppose
not n in dom g;
hence thesis by A2,FUNCT_1:def 2;
end;
end;
hence thesis by Def1;
end;
then for b holds P.(Ug /\ b) = P.Ug * P.b by A5,Th4;
hence thesis by Def1;
end;
for Z being Subset of Omega st Z in Indep(B,P) holds Z` in Indep(B,P)
proof
let Z be Subset of Omega;
assume
A6: Z in Indep(B,P);
then reconsider Z as Event of Sigma;
reconsider Z9=Z` as Element of Sigma by PROB_1:20;
for b being Element of B holds P.(Z` /\ b) = P.Z` * P.b
proof
let b be Element of B;
P.(b /\ Z) = P.b * P.Z by A6,Def1;
then b,Z are_independent_respect_to P by PROB_2:def 4;
then b, ([#]Sigma\Z) are_independent_respect_to P by PROB_2:25;
hence thesis by PROB_2:def 4;
end;
then Z9 in Indep(B,P) by Def1;
hence thesis;
end;
then Indp is Dynkin_System of Omega by A2,A3,DYNKIN:def 5;
hence thesis;
end;
theorem Th6:
for A being Subset-Family of Omega st A is intersection_stable &
A c= Indep(B,P) holds sigma(A) c= Indep(B,P)
proof
reconsider Indp = Indep(B,P) as Dynkin_System of Omega by Th5;
let A be Subset-Family of Omega;
assume A is intersection_stable & A c= Indep(B,P);
then sigma(A) c= Indp by DYNKIN:24;
hence thesis;
end;
theorem Th7:
for A, B being non empty Subset of Sigma holds A c= Indep(B,P)
iff for p,q st p in A & q in B holds p,q are_independent_respect_to P
proof
let A, B be non empty Subset of Sigma;
A1: now
assume
A2: for p,q st p in A & q in B holds p,q are_independent_respect_to P;
thus A c= Indep(B,P)
proof
let x be object;
assume
A3: x in A;
then reconsider x as Event of Sigma;
for b being Element of B holds P.(x /\ b) = P.x * P.b
by A2,A3,PROB_2:def 4;
hence thesis by Def1;
end;
end;
now
assume
A4: A c= Indep(B,P);
thus for p,q st p in A & q in B holds p,q are_independent_respect_to P
proof
let p,q;
assume that
A5: p in A and
A6: q in B;
reconsider q as Element of B by A6;
reconsider p as Element of Sigma;
P.(p /\ q) = P.p * P.q by A4,A5,Def1;
hence thesis by PROB_2:def 4;
end;
end;
hence thesis by A1;
end;
theorem Th8:
for A,B being non empty Subset of Sigma st A c= Indep(B,P) holds
B c= Indep(A,P)
proof
let A, B be non empty Subset of Sigma;
assume
A1: A c= Indep(B,P);
for q,p st q in B & p in A holds q,p are_independent_respect_to P
by A1,Th7,PROB_2:19;
hence thesis by Th7;
end;
theorem Th9:
for A being Subset-Family of Omega st A is non empty Subset of
Sigma & A is intersection_stable for B being non empty Subset of Sigma st B is
intersection_stable holds A c= Indep(B,P) implies for D,sB st D=B & sigma(D)=sB
holds sigma(A) c= Indep(sB,P)
proof
let A be Subset-Family of Omega;
assume A is non empty Subset of Sigma;
then reconsider sA=sigma(A) as non empty Subset of Sigma by PROB_1:def 9;
assume
A1: A is intersection_stable;
let B be non empty Subset of Sigma;
assume
A2: B is intersection_stable;
assume A c= Indep(B,P);
then
A3: sigma(A) c= Indep(B,P) by A1,Th6;
let D, sB;
assume
A4: D=B & sigma(D)=sB;
reconsider B as Subset-Family of Omega by XBOOLE_1:1;
B c= Indep(sA,P) by A3,Th8;
then sigma(B) c= Indep(sA,P) by A2,Th6;
hence thesis by A4,Th8;
end;
theorem Th10:
for E,F st E is non empty Subset of Sigma & E is
intersection_stable & F is non empty Subset of Sigma & F is intersection_stable
holds (for p,q st p in E & q in F holds p,q are_independent_respect_to P)
implies for u,v st u in sigma(E) & v in sigma(F) holds u,v
are_independent_respect_to P
proof
let E,F;
assume
A1: E is non empty Subset of Sigma;
assume
A2: E is intersection_stable;
assume
A3: F is non empty Subset of Sigma;
assume
A4: F is intersection_stable;
assume
A5: for p,q st p in E & q in F holds p,q are_independent_respect_to P;
reconsider F as non empty Subset of Sigma by A3;
reconsider E as non empty Subset of Sigma by A1;
A6: E c= Indep(F,P) by A5,Th7;
reconsider E, F as Subset-Family of Omega;
reconsider sF=sigma(F) as non empty Subset of Sigma by PROB_1:def 9;
sigma(E) c= Indep(sF,P) by A2,A4,A6,Th9;
hence thesis by Th7;
end;
definition
let I be set, Omega be non empty set, Sigma be SigmaField of Omega;
mode ManySortedSigmaField of I,Sigma -> Function of I, bool Sigma means
:
Def2: for i st i in I holds it.i is SigmaField of Omega;
existence
proof
set F = I --> Sigma;
A1: rng F c= bool Sigma
proof
let y be object;
assume y in rng F;
then ex x being object st x in dom F & y = F.x by FUNCT_1:def 3;
then y = Sigma by FUNCOP_1:7;
hence thesis by ZFMISC_1:def 1;
end;
A2: for i st i in I holds F.i is SigmaField of Omega by FUNCOP_1:7;
dom F = I by FUNCOP_1:13;
then F is Function of I, bool Sigma by A1,FUNCT_2:2;
hence thesis by A2;
end;
end;
definition
let Omega be non empty set, Sigma be SigmaField of Omega, P be Probability
of Sigma, I be set, A be Function of I, Sigma;
pred A is_independent_wrt P means
for e being one-to-one FinSequence
of I st e <> {} holds Product (P*A*e) = P.(meet rng (A*e));
end;
definition
let Omega be non empty set, Sigma be SigmaField of Omega, I be set, J be
Subset of I, F be ManySortedSigmaField of I,Sigma;
mode SigmaSection of J,F -> Function of J, Sigma means
:Def4:
for i st i in J holds it.i in F.i;
existence
proof
set f = J --> {};
A1: for i st i in J holds f.i in F.i
proof
let i;
assume
A2: i in J;
then F.i is SigmaField of Omega by Def2;
then {} in F.i by PROB_1:4;
hence thesis by A2,FUNCOP_1:7;
end;
A3: dom f = J by FUNCOP_1:13;
rng f c= Sigma
proof
let y be object;
assume y in rng f;
then consider i being object such that
A4: i in J & y=f.i by A3,FUNCT_1:def 3;
y in F.i & F.i in bool Sigma by A1,A4,FUNCT_2:5;
hence thesis;
end;
then f is Function of J, Sigma by A3,FUNCT_2:2;
hence thesis by A1;
end;
end;
definition
let Omega be non empty set, Sigma be SigmaField of Omega, P be Probability
of Sigma, I be set, F be ManySortedSigmaField of I,Sigma;
pred F is_independent_wrt P means
for E being finite Subset of I, A
being SigmaSection of E,F holds A is_independent_wrt P;
end;
definition
let I be set, Omega be non empty set, Sigma be SigmaField of Omega, F be
ManySortedSigmaField of I,Sigma, J be Subset of I;
redefine func F|J -> Function of J, bool Sigma; :: redefines | (RELAT_1, definition)
coherence by FUNCT_2:32;
end;
definition
let I be set, J be Subset of I, Omega be non empty set, Sigma be SigmaField
of Omega, F be Function of J, bool Sigma;
redefine func Union F -> Subset-Family of Omega; :: redefines Union (CARD_3, definition)
coherence
proof
for y being object holds y in Union F implies y in bool Omega
proof let y be object;
assume y in Union F;
then consider i being object such that
A1: i in dom F & y in F.i by CARD_5:2;
reconsider i as set by TARSKI:1;
i in dom F & y in F.i by A1;
hence thesis;
end;
hence thesis by TARSKI:def 3;
end;
end;
definition
let I be set, Omega be non empty set, Sigma be SigmaField of Omega, F be
ManySortedSigmaField of I,Sigma, J be Subset of I;
func sigUn(F,J) -> SigmaField of Omega equals
sigma Union (F|J);
coherence;
end;
definition
let I be set, Omega be non empty set, Sigma be SigmaField of Omega, F be
ManySortedSigmaField of I, Sigma;
func futSigmaFields(F,I) -> Subset-Family of bool Omega means
:Def7:
for S
being Subset-Family of Omega holds S in it iff ex E being finite Subset of I st
S=sigUn(F,I\E);
existence
proof
defpred P[set] means ex E being finite Subset of I st $1=sigUn(F,I\E);
consider X such that
A1: for x holds x in X iff x in bool bool Omega & P[x] from XFAMILY:
sch 1;
A2: X is non empty
proof
set Ie=I\{}I;
sigUn(F,Ie) in X by A1;
hence thesis;
end;
for x being object holds x in X implies x in bool bool Omega by A1;
then reconsider X as non empty Subset-Family of bool Omega by A2,
TARSKI:def 3;
take X;
let S be Subset-Family of Omega;
thus thesis by A1;
end;
uniqueness
proof
let X1,X2 be Subset-Family of bool Omega;
assume
A3: for S being Subset-Family of Omega holds S in X1 iff ex E being
finite Subset of I st S=sigUn(F,I\E);
assume
A4: for S being Subset-Family of Omega holds S in X2 iff ex E being
finite Subset of I st S=sigUn(F,I\E);
now
let S be Subset-Family of Omega;
S in X1 iff ex E being finite Subset of I st S=sigUn(F,I\E) by A3;
hence S in X1 iff S in X2 by A4;
end;
hence thesis by SUBSET_1:3;
end;
end;
registration
let I be set, Omega be non empty set, Sigma be SigmaField of Omega, F be
ManySortedSigmaField of I, Sigma;
cluster futSigmaFields(F,I) -> non empty;
coherence
proof
set Ie=I\{}I;
sigUn(F,Ie) in futSigmaFields(F,I) by Def7;
hence thesis;
end;
end;
definition
let I be set, Omega be non empty set, Sigma be SigmaField of Omega, F be
ManySortedSigmaField of I, Sigma;
func tailSigmaField(F,I) -> Subset-Family of Omega equals
meet
futSigmaFields(F,I);
coherence;
end;
registration
let I be set, Omega be non empty set, Sigma be SigmaField of Omega, F be
ManySortedSigmaField of I, Sigma;
cluster tailSigmaField(F,I) -> non empty;
coherence
proof
for X holds X in futSigmaFields(F,I) implies {} in X
proof
let X;
assume X in futSigmaFields(F,I);
then ex E being finite Subset of I st X=sigUn(F,I\E) by Def7;
hence thesis by PROB_1:4;
end;
hence thesis by SETFAM_1:def 1;
end;
end;
definition
let Omega be non empty set, Sigma be SigmaField of Omega, I be non empty set
, J be non empty Subset of I, F be ManySortedSigmaField of I,Sigma;
func MeetSections(J,F) -> Subset-Family of Omega means
:Def9:
for x being
Subset of Omega holds x in it iff ex E being non empty finite Subset of I, f
being SigmaSection of E,F st E c= J & x = meet rng f;
existence
proof
defpred P[set] means ex E being non empty finite Subset of I, f being
SigmaSection of E,F st E c= J & $1 = meet rng f;
consider X such that
A1: for x holds x in X iff x in bool Omega & P[x] from XFAMILY:sch 1;
for x being object holds x in X implies x in bool Omega by A1;
then reconsider X as Subset-Family of Omega by TARSKI:def 3;
take X;
let x be Subset of Omega;
thus thesis by A1;
end;
uniqueness
proof
let X1,X2 be Subset-Family of Omega;
assume
A2: for x being Subset of Omega holds x in X1 iff ex E being non empty
finite Subset of I, f being SigmaSection of E,F st E c= J & x = meet rng f;
assume
A3: for x being Subset of Omega holds x in X2 iff ex E being non empty
finite Subset of I, f being SigmaSection of E,F st E c= J & x = meet rng f;
now
let x be Subset of Omega;
x in X1 iff ex E being non empty finite Subset of I, f being
SigmaSection of E,F st E c= J & x = meet rng f by A2;
hence x in X1 iff x in X2 by A3;
end;
hence thesis by SUBSET_1:3;
end;
end;
theorem Th11:
for F being ManySortedSigmaField of I, Sigma, J being non empty
Subset of I holds sigma MeetSections(J,F) = sigUn(F,J)
proof
let F be ManySortedSigmaField of I,Sigma, J be non empty Subset of I;
A1: Union (F|J) c= MeetSections(J,F)
proof
let x be object;
assume x in Union (F|J);
then consider y such that
A2: x in y and
A3: y in rng (F|J) by TARSKI:def 4;
consider i being object such that
A4: i in dom (F|J) and
A5: y = (F|J).i by A3,FUNCT_1:def 3;
reconsider i as set by TARSKI:1;
y = (F|J).i by A5;
then reconsider x as Subset of Omega by A2;
defpred P[object,object] means $2=x & $2 in F.$1;
A6: {i} c= J by A4,ZFMISC_1:31;
then reconsider E={i} as finite Subset of I by XBOOLE_1:1;
A7: for j being object st j in E ex y being object st y in Sigma & P[j,y]
proof
let j be object;
assume
A8: j in E;
i in I by A4,TARSKI:def 3;
then
A9: F.i in bool Sigma by FUNCT_2:5;
take y=x;
y in F.i by A2,A4,A5,FUNCT_1:49;
hence thesis by A8,A9,TARSKI:def 1;
end;
consider g being Function of E, Sigma such that
A10: for j being object st j in E holds P[j,g.j] from FUNCT_2:sch 1(A7);
for i st i in E holds g.i in F.i by A10;
then reconsider g as SigmaSection of E,F by Def4;
dom g = E by FUNCT_2:def 1;
then
A11: rng g = {g.i} by FUNCT_1:4;
i in E by TARSKI:def 1;
then x=g.i by A10
.= meet rng g by A11,SETFAM_1:10;
hence thesis by A6,Def9;
end;
MeetSections(J,F) c= sigma Union (F|J)
proof
let x be object;
assume x in MeetSections(J,F);
then consider
E being non empty finite Subset of I, f being SigmaSection of E,F
such that
A12: E c= J and
A13: x = meet rng f by Def9;
reconsider Ee=E as Element of Fin E by FINSUB_1:def 5;
for B being Element of Fin E holds meet rng (f|B) in sigma (Union (F|J ))
proof
defpred P[set] means meet rng (f|$1) in sigma Union (F|J);
let B be Element of Fin E;
A14: for B9 being Element of Fin E, b being Element of E holds P[B9] &
not b in B9 implies P[B9 \/ {b}]
proof
let B9 be Element of Fin E, b be Element of E;
assume that
A15: meet rng (f|B9) in sigma (Union (F|J)) and
not b in B9;
reconsider rfb = rng (f|{b}) as set;
reconsider rfB9 = rng (f|B9) as set;
reconsider rfB9b = rng (f|(B9 \/ {b})) as set;
rng (f|(B9 \/ {b})) = rng ((f|B9) \/ (f|{b})) by RELAT_1:78;
then
A16: rng (f|(B9 \/ {b})) = (rng (f|B9)) \/ rng (f|{b}) by RELAT_1:12;
dom (F|J) = J by FUNCT_2:def 1;
then
A17: b in dom (F|J) by A12;
then (F|J).b in rng (F|J) by FUNCT_1:def 3;
then F.b in rng (F|J) by A17,FUNCT_1:47;
then
A18: F.b c= Union (F|J) by ZFMISC_1:74;
Union (F|J) c= sigma Union (F|J) by PROB_1:def 9;
then
A19: F.b c= sigma (Union (F|J)) by A18;
b is Element of dom f by FUNCT_2:def 1;
then
A20: {b} = dom f /\ {b} by ZFMISC_1:46
.= dom (f|{b}) by RELAT_1:61;
then
A21: b in dom (f|{b}) by TARSKI:def 1;
rng (f|{b}) = {(f|{b}).b} by A20,FUNCT_1:4
.= {f.b} by A21,FUNCT_1:47;
then meet rng (f|{b}) = f.b by SETFAM_1:10;
then
A22: meet rng (f|{b}) in F.b by Def4;
per cases;
suppose
rng (f|B9) = {};
hence thesis by A22,A19,A16;
end;
suppose
A23: not rng (f|B9) = {};
dom f = E & b in {b} by FUNCT_2:def 1,TARSKI:def 1;
then rfb <> {} by FUNCT_1:50;
then meet rfB9b = (meet rfB9) /\ meet rfb by A16,A23,SETFAM_1:9;
then meet rng (f|(B9 \/ {b})) is Event of sigma Union (F|J) by A15
,A22,A19,PROB_1:19;
hence thesis;
end;
end;
meet rng (f|{}) = {} by SETFAM_1:def 1;
then
A24: P[{}.E] by PROB_1:4;
for B1 being Element of Fin E holds P[B1] from SETWISEO:sch 2( A24,
A14);
hence thesis;
end;
then meet rng (f|Ee) in sigma (Union (F|J));
hence thesis by A13;
end;
hence sigma MeetSections(J,F) c= sigUn(F,J) by PROB_1:def 9;
MeetSections(J,F) c= sigma MeetSections(J,F) by PROB_1:def 9;
then Union (F|J) c= sigma MeetSections(J,F) by A1;
hence thesis by PROB_1:def 9;
end;
theorem Th12:
for F being ManySortedSigmaField of I, Sigma, J,K being non
empty Subset of I st F is_independent_wrt P & J misses K holds for a,c being
Subset of Omega st a in MeetSections(J,F) & c in MeetSections(K,F) holds P.(a
/\ c) = P.a * P.c
proof
let F be ManySortedSigmaField of I, Sigma, J,K be non empty Subset of I;
assume
A1: F is_independent_wrt P;
reconsider Si=Sigma as set;
assume
A2: J misses K;
let a,c be Subset of Omega;
assume that
A3: a in MeetSections(J,F) and
A4: c in MeetSections(K,F);
consider E1 being non empty finite Subset of I, f1 being SigmaSection of E1,
F such that
A5: E1 c= J and
A6: a = meet rng f1 by A3,Def9;
A7: f1 is_independent_wrt P by A1;
consider E2 being non empty finite Subset of I, f2 being SigmaSection of E2,
F such that
A8: E2 c= K and
A9: c = meet rng f2 by A4,Def9;
A10: f2 is_independent_wrt P by A1;
reconsider rngf1 = rng f1, rngf2 = rng f2 as set;
reconsider f1 as Function of E1, rngf1 by FUNCT_2:6;
reconsider f2 as Function of E2, rngf2 by FUNCT_2:6;
consider m being Nat such that
A11: E2,Seg m are_equipotent by FINSEQ_1:56;
consider e2 be Function such that
A12: e2 is one-to-one and
A13: dom e2 = Seg m and
A14: rng e2 = E2 by A11,WELLORD2:def 4;
A15: e2 <> {} by A14;
reconsider e2 as Function of Seg m, E2 by A13,A14,FUNCT_2:1;
A16: e2 is FinSequence by A13,FINSEQ_1:def 2;
A17: rng(f2*e2)= rng f2 by A14,FUNCT_2:14;
reconsider e2 as one-to-one FinSequence of E2 by A12,A14,A16,FINSEQ_1:def 4;
reconsider f2 as Function of E2, Si;
deffunc B(object) = f2.$1;
reconsider fe2=f2*e2 as FinSequence of Si;
rng e2 = dom f2 by A14,FUNCT_2:def 1;
then
A18: len fe2 = len e2 by FINSEQ_2:29;
E2 c= E1 \/ E2 by XBOOLE_1:7;
then
A19: rng e2 c= E1 \/ E2;
defpred C[object] means $1 in E1;
consider n being Nat such that
A20: E1,Seg n are_equipotent by FINSEQ_1:56;
consider e1 be Function such that
A21: e1 is one-to-one and
A22: dom e1 = Seg n and
A23: rng e1 = E1 by A20,WELLORD2:def 4;
A24: e1 <> {} by A23;
reconsider e1 as Function of Seg n, E1 by A22,A23,FUNCT_2:1;
A25: e1 is FinSequence by A22,FINSEQ_1:def 2;
A26: rng(f1*e1)= rng f1 by A23,FUNCT_2:14;
reconsider e1 as one-to-one FinSequence of E1 by A21,A23,A25,FINSEQ_1:def 4;
reconsider f1 as Function of E1, Si;
deffunc D(object) = f1.$1;
reconsider fe1=f1*e1 as FinSequence of Si;
rng e1 = dom f1 by A23,FUNCT_2:def 1;
then
A27: len fe1 = len e1 by FINSEQ_2:29;
consider h being Function such that
A28: dom h = E1 \/ E2 &
for i being object st i in E1 \/ E2 holds (C[i] implies h.i =
D(i)) & (not C[i] implies h.i = B(i)) from PARTFUN1:sch 1;
::: set h = f2 +* f1; ??? !!!
for x being object holds x in dom (e1^e2) implies x in dom (h*(e1^e2))
proof let x be object;
assume
A29: x in dom (e1^e2);
rng (e1^e2) = dom h by A23,A14,A28,FINSEQ_1:31;
then (e1^e2).x in dom h by A29,FUNCT_1:3;
hence thesis by A29,FUNCT_1:11;
end;
then
A30: dom (e1^e2) c= dom (h*(e1^e2));
for x being object holds
x in dom (h*(e1^e2)) implies x in dom (e1^e2) by FUNCT_1:11;
then
A31: dom (h*(e1^e2)) c= dom (e1^e2);
A32: dom (fe1^fe2) = Seg (len fe1 + len fe2) by FINSEQ_1:def 7
.= dom (e1^e2) by A27,A18,FINSEQ_1:def 7
.= dom (h*(e1^e2)) by A31,A30;
for x being object st x in dom (fe1^fe2) holds (fe1^fe2).x = (h*(e1^e2)).x
proof
let x be object;
assume
A33: x in dom (fe1^fe2);
then reconsider x as Element of NAT;
per cases;
suppose
A34: x in dom fe1;
then
A35: (fe1^fe2).x = fe1.x by FINSEQ_1:def 7;
A36: E1 c= E1 \/ E2 by XBOOLE_1:7;
A37: x in dom e1 by A34,FUNCT_1:11;
then e1.x in E1 by A23,FUNCT_1:3;
then h.(e1.x) = f1.(e1.x) by A28,A36;
then
A38: (fe1^fe2).x = h.(e1.x) by A34,A35,FUNCT_1:12;
(e1^e2).x = e1.x by A37,FINSEQ_1:def 7;
hence thesis by A32,A33,A38,FUNCT_1:12;
end;
suppose
not x in dom fe1;
then consider n be Nat such that
A39: n in dom fe2 and
A40: x = len fe1 + n by A33,FINSEQ_1:25;
A41: n in dom e2 by A39,FUNCT_1:11;
then
A42: e2.n in E2 by A14,FUNCT_1:3;
E1 /\ E2 c= J /\ K by A5,A8,XBOOLE_1:27;
then E1 /\ E2 c= {} by A2;
then E1 /\ E2 = {};
then E2 = E2\E1 \/ {} by XBOOLE_1:51;
then
A43: not e2.n in E1 by A42,XBOOLE_0:def 5;
A44: E2 c= E1 \/ E2 by XBOOLE_1:7;
(fe1^fe2).x = fe2.n by A39,A40,FINSEQ_1:def 7
.= f2.(e2.n) by A39,FUNCT_1:12
.= h.(e2.n) by A28,A42,A43,A44
.= h.((e1^e2).x) by A27,A40,A41,FINSEQ_1:def 7;
hence thesis by A32,A33,FUNCT_1:12;
end;
end;
then
A45: fe1^fe2 = h*(e1^e2) by A32,FUNCT_1:def 11;
for i being object st i in E1 \/ E2 holds h.i in Sigma
proof
let i be object;
assume
A46: i in E1 \/ E2;
per cases;
suppose
A47: i in E1;
then h.i = f1.i by A28,A46;
hence thesis by A47,FUNCT_2:5;
end;
suppose
not i in E1;
then h.i = f2.i & i in E2 by A28,A46,XBOOLE_0:def 3;
hence thesis by FUNCT_2:5;
end;
end;
then reconsider h as Function of E1 \/ E2, Sigma by A28,FUNCT_2:3;
for i st i in E1 \/ E2 holds h.i in F.i
proof
let i;
assume
A48: i in E1 \/ E2;
per cases;
suppose
A49: i in E1;
then f1.i in F.i by Def4;
hence thesis by A28,A48,A49;
end;
suppose
A50: not i in E1;
then i in E2 by A48,XBOOLE_0:def 3;
then f2.i in F.i by Def4;
hence thesis by A28,A48,A50;
end;
end;
then reconsider h as SigmaSection of E1 \/ E2, F by Def4;
A51: h is_independent_wrt P by A1;
E1 c= E1 \/ E2 by XBOOLE_1:7;
then
A52: rng e1 c= E1 \/ E2;
reconsider Pfe1=P*f1*e1, Pfe2=P*f2*e2 as FinSequence of REAL by FINSEQ_2:32;
reconsider e2 as FinSequence of E1 \/ E2 by A19,FINSEQ_1:def 4;
reconsider e1 as FinSequence of E1 \/ E2 by A52,FINSEQ_1:def 4;
E1 /\ E2 c= J /\ K by A5,A8,XBOOLE_1:27;
then E1 /\ E2 c= {} by A2;
then E1 /\ E2 = {};
then rng e1 misses rng e2 by A23,A14;
then reconsider e12 = e1^e2 as one-to-one FinSequence of E1 \/ E2 by
FINSEQ_3:91;
reconsider e1 as one-to-one FinSequence of E1;
reconsider fe1 as FinSequence of Si;
reconsider e2 as FinSequence of E2;
reconsider fe2 as FinSequence of Si;
reconsider f1 as Function of E1, Sigma;
reconsider f2 as Function of E2, Sigma;
reconsider P as Function of Si, REAL;
A53: P*h*e12 = P*(h*(e1^e2)) by RELAT_1:36
.=(P*fe1)^(P*fe2) by A45,FINSEQOP:9;
A54: P*fe1 = Pfe1 & P*fe2 = Pfe2 by RELAT_1:36;
reconsider P as Function of Sigma, REAL;
A55: Product(P*f1*e1) = P.meet rng (f1*e1) by A24,A7;
P.(a /\ c) = P.meet(rng f1 \/ rng f2) by A6,A9,SETFAM_1:9
.=P.meet rng(fe1 ^ fe2) by A26,A17,FINSEQ_1:31
.=Product(Pfe1 ^ Pfe2) by A24,A45,A51,A53,A54
.=Product(Pfe1) * Product(Pfe2) by RVSUM_1:97
.=P.a * P.c by A6,A9,A15,A10,A26,A17,A55;
hence thesis;
end;
theorem Th13:
for F being ManySortedSigmaField of I,Sigma, J being non empty
Subset of I holds MeetSections(J,F) is non empty Subset of Sigma
proof
let F be ManySortedSigmaField of I,Sigma, J be non empty Subset of I;
A1: MeetSections(J,F) c= Sigma
proof
let X be object;
assume X in MeetSections(J,F);
then consider
E being non empty finite Subset of I, f being SigmaSection of E,F
such that
E c= J and
A2: X = meet rng f by Def9;
reconsider Ee=E as Element of Fin E by FINSUB_1:def 5;
for B being Element of Fin E holds meet rng (f|B) in Sigma
proof
defpred P[set] means meet rng (f|$1) in Sigma;
let B be Element of Fin E;
A3: for B9 being (Element of Fin E), b being Element of E holds P[B9] &
not b in B9 implies P[B9 \/ {b}]
proof
let B9 be (Element of Fin E), b be Element of E;
assume that
A4: meet rng (f|B9) in Sigma and
not b in B9;
A5: rng (f|(B9 \/ {b})) = rng ((f|B9) \/ f|{b}) by RELAT_1:78
.= (rng (f|B9)) \/ rng (f|{b}) by RELAT_1:12;
dom f = E & b in {b} by FUNCT_2:def 1,TARSKI:def 1;
then
A6: f.b in rng(f|{b}) by FUNCT_1:50;
A7: b is Element of dom f by FUNCT_2:def 1;
then dom f /\ {b} = {b} by ZFMISC_1:46;
then dom (f|{b}) = {b} by RELAT_1:61;
then
A8: rng (f|{b}) = {(f|{b}).b} by FUNCT_1:4;
b in {b} by TARSKI:def 1;
then b in dom (f|{b}) by A7,RELAT_1:57;
then rng (f|{b}) = {f.b} by A8,FUNCT_1:47;
then
A9: meet rng (f|{b}) is Event of Sigma by SETFAM_1:10;
per cases;
suppose
rng (f|B9) = {};
hence thesis by A9,A5;
end;
suppose
not rng (f|B9) = {};
then meet rng (f|(B9 \/ {b}))= meet rng (f|B9) /\ meet rng (f|{b})
by A5,A6,SETFAM_1:9;
then meet rng (f|(B9 \/ {b})) is Event of Sigma by A4,A9,PROB_1:19;
hence thesis;
end;
end;
meet rng (f|{}) = {} by SETFAM_1:def 1;
then
A10: P[{}.E] by PROB_1:4;
for B1 being Element of Fin E holds P[B1] from SETWISEO:sch 2 ( A10
,A3);
hence thesis;
end;
then meet rng (f|Ee) in Sigma;
hence thesis by A2;
end;
MeetSections(J,F) is non empty set
proof
set E = the non empty finite Subset of J;
consider f being Function such that
A11: dom f = E and
A12: rng f = {{}} by FUNCT_1:5;
reconsider E as non empty finite Subset of I by XBOOLE_1:1;
A13: meet rng f = {} by A12,SETFAM_1:10;
rng f c= Sigma
proof
let y be object;
assume y in rng f;
then y={} by A12,TARSKI:def 1;
hence thesis by PROB_1:4;
end;
then reconsider f as Function of E, Sigma by A11,FUNCT_2:2;
for i st i in E holds f.i in F.i
proof
let i;
assume
A14: i in E;
then reconsider Fi=F.i as SigmaField of Omega by Def2;
f.i in rng f by A11,A14,FUNCT_1:def 3;
then f.i = {} by A12,TARSKI:def 1;
then f.i in Fi by PROB_1:4;
hence thesis;
end;
then reconsider f as SigmaSection of E,F by Def4;
reconsider mrf=meet rng f as Subset of Omega by A13,XBOOLE_1:2;
mrf in MeetSections(J,F) by Def9;
hence thesis;
end;
hence thesis by A1;
end;
registration
let I,Omega,Sigma;
let F be ManySortedSigmaField of I,Sigma, J be non empty Subset of I;
cluster MeetSections(J,F) -> intersection_stable;
coherence
proof
for x,X st x in MeetSections(J,F) & X in MeetSections(J,F) holds x /\
X in MeetSections(J,F)
proof
let x,X;
assume that
A1: x in MeetSections(J,F) and
A2: X in MeetSections(J,F);
consider E being non empty finite Subset of I, f being SigmaSection of E
,F such that
A3: E c= J and
A4: x = meet rng f by A1,Def9;
defpred C[object] means $1 in E;
deffunc D(object)= f.$1;
consider E9 being non empty finite Subset of I, f9 being SigmaSection of
E9,F such that
A5: E9 c= J and
A6: X = meet rng f9 by A2,Def9;
deffunc B(object)= f9.$1;
defpred P[object] means $1 in (E\E9) \/ (E9\E);
deffunc G(object) = (f.$1) /\ (f9.$1);
consider h being Function such that
A7: dom h = E \/ E9 &
for i being object st i in E \/ E9 holds (C[i] implies h.i
= D(i)) & (not C[i] implies h.i = B(i)) from PARTFUN1:sch 1;
deffunc F(object) = h.$1;
consider g being Function such that
A8: dom g = E \/ E9 &
for i being object st i in E \/ E9 holds (P[i] implies g.i
= F(i)) & (not P[i] implies g.i = G(i)) from PARTFUN1:sch 1;
A9: for i st i in E \/ E9 holds g.i in F.i
proof
let i;
assume
A10: i in E \/ E9;
per cases;
suppose
A11: i in (E\E9) \/ (E9\E);
h.i in F.i
proof
per cases;
suppose
A12: i in E;
then h.i = f.i by A7,A10;
hence thesis by A12,Def4;
end;
suppose
not i in E;
then i in E9 & h.i = f9.i by A7,A10,XBOOLE_0:def 3;
hence thesis by Def4;
end;
end;
hence thesis by A8,A10,A11;
end;
suppose
A13: not i in (E\E9) \/ (E9\E);
reconsider Fi=F.i as SigmaField of Omega by A10,Def2;
not i in E \+\ E9 by A13;
then i in E iff i in E9 by XBOOLE_0:1;
then f.i in F.i & f9.i in F.i by A10,Def4,XBOOLE_0:def 3;
then
A14: (f.i) /\ f9.i is Event of Fi by PROB_1:19;
g.i = (f.i) /\ f9.i by A8,A10,A13;
hence thesis by A14;
end;
end;
rng g c= Sigma
proof
let y be object;
assume y in rng g;
then consider i being object such that
A15: i in dom g & y=g.i by FUNCT_1:def 3;
y in F.i & F.i in bool Sigma by A8,A9,A15,FUNCT_2:5;
hence thesis;
end;
then g is Function of E \/ E9, Sigma by A8,FUNCT_2:2;
then reconsider g as SigmaSection of E \/ E9,F by A9,Def4;
A16: x /\ X = meet rng g
proof
A17: meet rng (g|(E /\ E9)) = (meet rng (f|(E /\ E9))) /\ meet rng (f9
|(E/\E9))
proof
per cases;
suppose
A18: E /\ E9 = {};
then
A19: meet rng (f|(E /\ E9)) = meet rng {} & meet rng (f9|(E /\ E9)
) = meet rng {};
meet rng (g|(E /\ E9)) = meet rng {} by A18
.= {} by SETFAM_1:def 1;
hence thesis by A19,SETFAM_1:def 1;
end;
suppose
not E /\ E9 = {};
then reconsider EnE9 = E /\ E9 as non empty set;
reconsider EE9=EnE9 as Element of Fin EnE9 by FINSUB_1:def 5;
for B being Element of Fin EnE9 holds meet rng (g|B) = (meet
rng (f|B)) /\ (meet rng (f9|B))
proof
defpred P[set] means meet rng (g|$1) = (meet rng (f|$1)) /\ meet
rng (f9|$1);
let B be Element of Fin EnE9;
A20: for B9 being (Element of Fin EnE9), b being Element of EnE9
holds P[B9] & not b in B9 implies P[B9 \/ {b}]
proof
let B9 be Element of Fin EnE9, b be Element of EnE9;
assume that
A21: meet rng (g|B9) = (meet rng (f|B9)) /\ meet rng (f9| B9) and
not b in B9;
A22: dom (f|{b}) = (dom f) /\ {b} by RELAT_1:61;
dom f = E by FUNCT_2:def 1;
then
A23: E /\ E9 c= dom f by XBOOLE_1:17;
then b in dom f;
then
A24: rng (f|{b}) = {(f|{b}).b} by A22,FUNCT_1:4,ZFMISC_1:46;
b in E\(E \/ E9) \/ (E /\ E /\ E9) by XBOOLE_0:def 3;
then b in E\(E \+\ E9) by XBOOLE_1:102;
then
A25: not b in E \+\ E9 by XBOOLE_0:def 5;
A26: b in {b} by TARSKI:def 1;
b in dom f by A23;
then b in dom (f|{b}) by A26,RELAT_1:57;
then
A27: rng (f|{b}) = {f.b} by A24,FUNCT_1:47;
then
A28: meet rng (f|{b}) = f.b by SETFAM_1:10;
A29: E /\ E9 c= E by XBOOLE_1:17;
A30: dom (f9|{b}) = (dom f9) /\ {b} by RELAT_1:61;
dom f9 = E9 by FUNCT_2:def 1;
then
A31: E /\ E9 c= dom f9 by XBOOLE_1:17;
then b in dom f9;
then
A32: rng (f9|{b}) = {(f9|{b}).b} by A30,FUNCT_1:4,ZFMISC_1:46;
b in dom f9 by A31;
then b in dom (f9|{b}) by A26,RELAT_1:57;
then
A33: rng (f9|{b}) = {f9.b} by A32,FUNCT_1:47;
then
A34: meet rng (f9|{b}) = f9.b by SETFAM_1:10;
A35: for g being Function, B9,b being set holds meet rng (g|(
B9 \/ {b})) = meet ((rng (g|B9)) \/ rng (g|{b}))
proof
let g be Function, B9,b be set;
rng (g|(B9 \/ {b})) = rng ((g|B9) \/ (g|{b})) by RELAT_1:78;
hence thesis by RELAT_1:12;
end;
E c= dom g by A8,XBOOLE_1:7;
then
A36: E /\ E9 c= dom g by A29;
then b is Element of dom g;
then dom g /\ {b} = {b} by ZFMISC_1:46;
then dom (g|{b}) = {b} by RELAT_1:61;
then
A37: rng (g|{b}) = {(g|{b}).b} by FUNCT_1:4;
b in {b} & b in dom g by A36,TARSKI:def 1;
then b in dom (g|{b}) by RELAT_1:57;
then
A38: rng (g|{b}) = {g.b} by A37,FUNCT_1:47;
then
A39: meet rng (g|{b}) = g.b by SETFAM_1:10;
E c= E \/ E9 by XBOOLE_1:7;
then
A40: E /\ E9 c= E \/ E9 by A29;
then b in E\/E9;
then
A41: g.b = (f.b) /\ f9.b by A8,A25;
per cases;
suppose
B9 = {};
hence thesis by A28,A34,A41,A38,SETFAM_1:10;
end;
suppose
A42: B9 <> {};
set z = the Element of B9;
B9 c= E /\ E9 by FINSUB_1:def 5;
then
A43: B9 c= E \/ E9 by A40;
z in B9 by A42;
then dom(g|B9) <> {} by A8,A43;
then rng(g|B9) <> {} by RELAT_1:42;
then meet ((rng (g|B9)) \/ rng (g|{b})) = (meet rng (g|B9))
/\ meet rng (g|{b}) by A37,SETFAM_1:9;
then
A44: meet rng (g|(B9 \/ {b})) = (meet rng (f|B9)) /\ (meet
rng (f9|B9)) /\ g.b by A21,A35,A39
.= (meet rng (f|B9)) /\ ((meet rng (f9|B9)) /\ ((f.b) /\
f9.b)) by A41,XBOOLE_1:16
.= (meet rng (f|B9)) /\ ((f.b) /\ ((meet rng (f9|B9)) /\
f9.b)) by XBOOLE_1:16
.= ((meet rng (f|B9)) /\ f.b) /\ (((meet rng (f9|B9)) /\
f9.b)) by XBOOLE_1:16;
B9 c= E /\ E9 & E /\ E9 c= E9 by FINSUB_1:def 5,XBOOLE_1:17;
then B9 c= E9;
then
A45: B9 c= dom f9 by FUNCT_2:def 1;
B9 c= E /\ E9 & E /\ E9 c= E by FINSUB_1:def 5,XBOOLE_1:17;
then B9 c= E;
then
A46: B9 c= dom f by FUNCT_2:def 1;
meet rng (f|(B9 \/ {b})) = meet ((rng (f|B9)) \/ rng (f
|{b})) by A35
.= (meet rng (f|B9)) /\ meet rng (f|{b}) by A24,A42,A46,
SETFAM_1:9;
then
A47: (meet rng (f|B9)) /\ f.b = meet rng (f|(B9 \/ {b})) by A27,
SETFAM_1:10;
meet rng (f9|(B9 \/ {b})) = meet ((rng (f9|B9)) \/ rng
(f9|{b})) by A35
.= (meet rng (f9|B9)) /\ meet rng (f9|{b}) by A32,A42,A45,
SETFAM_1:9;
hence thesis by A33,A44,A47,SETFAM_1:10;
end;
end;
A48: P[{}.(EnE9)];
for B1 being Element of Fin EnE9 holds P[B1] from SETWISEO:
sch 2(A48,A20);
hence thesis;
end;
then meet rng (g|EE9) = (meet rng (f|EE9)) /\ meet rng (f9|EE9);
hence thesis;
end;
end;
A49: for E,E9 being set, g being Function st dom g = E \/ E9 holds
rng g = (rng (g|(E /\ E9))) \/ (rng (g|(E\E9))) \/ rng (g|(E9\E))
proof
let E,E9 be set, g be Function;
rng (g|(E /\ E9)) c= rng g & rng (g|(E\E9)) c= rng g by RELAT_1:70;
then
A50: (rng (g|(E /\ E9))) \/ (rng (g|(E\E9))) c= rng g by XBOOLE_1:8;
assume
A51: dom g = E \/ E9;
thus rng g c= (rng (g|(E /\ E9))) \/ (rng (g|(E\E9))) \/ rng (g|(E9\
E))
proof
let y be object;
assume y in rng g;
then consider i being object such that
A52: i in dom g and
A53: y=g.i by FUNCT_1:def 3;
per cases;
suppose
A54: i in (E\E9) \/ (E9\E);
y in (rng (g|(E/\E9))) \/ (rng (g|(E\E9))) \/ rng (g|(E9\E ))
proof
per cases;
suppose
A55: i in E;
A56: E /\ E9 c= E by XBOOLE_1:17;
E /\ ((E\E9) \/ (E9\E)) = E /\ (E\E9) \/ E /\ (E9\E)
by XBOOLE_1:23
.= (E\E9) \/ E /\ (E9\E) by XBOOLE_1:28
.= (E\E9) \/ ((E /\ E9) \ E) by XBOOLE_1:49
.= (E\E9) \/ {} by A56,XBOOLE_1:37;
then i in E\E9 by A54,A55,XBOOLE_0:def 4;
then i in dom g /\ (E\E9) by A52,XBOOLE_0:def 4;
then
A57: i in dom (g|(E\E9)) by RELAT_1:61;
then (g|(E\E9)).i = y by A53,FUNCT_1:47;
then y in rng (g|(E\E9)) by A57,FUNCT_1:def 3;
then y in (rng (g|(E/\E9))) \/ rng (g|(E\E9)) by
XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
suppose
A58: not i in E;
((E\E9) \/ (E9\E)) \ E = ((E\E9) \ E) \/ ((E9\E) \ E)
by XBOOLE_1:42
.= {} \/ ((E9\E) \ E) by XBOOLE_1:37
.= E9 \ (E \/ E) by XBOOLE_1:41;
then i in E9 \ (E \/ E) by A54,A58,XBOOLE_0:def 5;
then i in dom g /\ (E9\E) by A52,XBOOLE_0:def 4;
then
A59: i in dom (g|(E9\E)) by RELAT_1:61;
then (g|(E9\E)).i = y by A53,FUNCT_1:47;
then y in rng (g|(E9\E)) by A59,FUNCT_1:def 3;
then y in (rng (g|(E\E9))) \/ rng (g|(E9\E)) by
XBOOLE_0:def 3;
then y in (rng (g|(E/\E9))) \/ ((rng (g|(E\E9))) \/ rng (g|
(E9\E))) by XBOOLE_0:def 3;
hence thesis by XBOOLE_1:4;
end;
end;
hence thesis;
end;
suppose
A60: not i in (E\E9) \/ (E9\E);
A61: (E \/ E9) \ (E \+\ E9) = (E \/ E9) \ (E \/ E9) \/ (E \/ E9
) /\ E /\ E9 by XBOOLE_1:102
.= {} \/ (E \/ E9) /\ E /\ E9 by XBOOLE_1:37
.= (E \/ E9) /\ (E /\ E9) by XBOOLE_1:16;
i in (E \/ E9) \ (E \+\ E9) by A51,A52,A60,XBOOLE_0:def 5;
then
A62: i in dom (g|(E /\ E9)) by A51,A61,RELAT_1:61;
then (g|(E /\ E9)).i = y by A53,FUNCT_1:47;
then y in rng (g|(E /\ E9)) by A62,FUNCT_1:def 3;
then y in (rng (g|(E /\ E9))) \/ rng (g|(E\E9)) by XBOOLE_0:def 3
;
hence thesis by XBOOLE_0:def 3;
end;
end;
rng (g|(E9\E)) c= rng g by RELAT_1:70;
hence thesis by A50,XBOOLE_1:8;
end;
then
A63: rng g = (rng (g|(E /\ E9))) \/ (rng (g|(E\E9))) \/ rng (g|(E9\E)
) by A8;
A64: dom (g|(E9\E)) = dom g /\ (E9\E) by RELAT_1:61
.= (E \/ E9) /\ (E9\E) by FUNCT_2:def 1
.= ((E \/ E9) /\ E9) \ E by XBOOLE_1:49
.= E9\E by XBOOLE_1:21;
A65: for i being object st i in dom (g|(E9\E)) holds (g|(E9\E)).i = f9.i
proof
let i be object;
assume
A66: i in dom (g|(E9\E));
then
A67: i in (E\E9) \/ (E9\E) by A64,XBOOLE_0:def 3;
not i in E by A64,A66,XBOOLE_0:def 5;
then f9.i = h.i by A7,A66
.= g.i by A8,A66,A67;
hence thesis by A66,FUNCT_1:47;
end;
dom (g|(E9\E)) = (E9 /\ E9)\E by A64
.= E9 /\ (E9\E) by XBOOLE_1:49
.= dom f9 /\ (E9\E) by FUNCT_2:def 1;
then
A68: meet rng (g|(E9\E)) = meet rng (f9|(E9\E)) by A65,FUNCT_1:46;
A69: dom (g|(E\E9)) = dom g /\ (E\E9) by RELAT_1:61
.= (E \/ E9) /\ (E\E9) by FUNCT_2:def 1
.= ((E \/ E9) /\ E) \ E9 by XBOOLE_1:49
.= E\E9 by XBOOLE_1:21;
A70: for i being object st i in dom(g|(E\E9)) holds (g|(E\E9)).i = f.i
proof
let i be object;
A71: E\E9 c= E by XBOOLE_1:36;
assume
A72: i in dom(g|(E\E9));
then i in (E\E9) \/ (E9\E) by A69,XBOOLE_0:def 3;
then g.i = h.i by A8,A72
.= f.i by A7,A69,A72,A71;
hence thesis by A72,FUNCT_1:47;
end;
dom (g|(E\E9)) = (E /\ E) \ E9 by A69
.= E /\ (E\E9) by XBOOLE_1:49
.= dom f /\ (E\E9) by FUNCT_2:def 1;
then
A73: meet rng (g|(E\E9)) = meet rng (f|(E\E9)) by A70,FUNCT_1:46;
per cases;
suppose
A74: E /\ E9 = {};
A75: E\E9 c= E by XBOOLE_1:36;
A76: E9 c= dom g & E c= dom g by A8,XBOOLE_1:7;
A77: E9\E c= E9 by XBOOLE_1:36;
A78: E misses E9 by A74;
E c= E\E9 by A78,XBOOLE_1:86;
then
A79: E = E\E9 by A75;
E9 c= E9\E by A78,XBOOLE_1:86;
then
A80: E9 = E9\E by A77;
rng (g|(E /\ E9)) = {} by A74;
hence thesis by A4,A6,A73,A68,A63,A80,A79,A76,SETFAM_1:9;
end;
suppose
A81: not E /\ E9 = {};
meet rng g = (meet rng f) /\ meet rng f9
proof
per cases;
suppose
A82: E\E9 = {};
then
A83: rng (g|(E\E9)) = {};
A84: E c= E9 by A82,XBOOLE_1:37;
A85: E /\ E9 c= dom g by A8,XBOOLE_1:29;
meet rng g = (meet rng f) /\ meet rng f9
proof
per cases;
suppose
E9\E = {};
then E9 c= E by XBOOLE_1:37;
then
A86: E=E9 by A84;
thus thesis by A17,A86;
end;
suppose
A87: E9\E <> {};
E9\E c= E9 & E9 c= E9 \/ E by XBOOLE_1:7,36;
then E9\E c= dom g by A8;
then meet rng g = (meet rng (g|(E /\ E9))) /\ meet rng (g|(
E9\E)) by A63,A81,A83,A85,A87,SETFAM_1:9;
then
A88: meet rng g = (meet rng f) /\ (meet rng (f9|(E/\E9)))
/\ meet rng (f9|(E9\E)) by A17,A68,A84,RELSET_1:19,XBOOLE_1:19;
A89: rng (f9|(E\E9)) = {} by A82;
E9\E c= E9 by XBOOLE_1:36;
then
A90: E9\E c= dom f9 by FUNCT_2:def 1;
E /\ E9 c= E9 by XBOOLE_1:17;
then
A91: E /\ E9 c= dom f9 by FUNCT_2:def 1;
E9 \/ E = E9 & dom f9 = E9 by A84,FUNCT_2:def 1,XBOOLE_1:12;
then rng f9= (rng (f9|(E /\ E9))) \/ (rng (f9|(E\E9))) \/
rng (f9|(E9\E)) by A49
.= (rng (f9|(E /\ E9))) \/ rng (f9|(E9\E)) by A89;
then meet rng f9 = (meet rng (f9|(E /\ E9))) /\ meet rng (
f9|(E9\E)) by A81,A87,A91,A90,SETFAM_1:9;
hence thesis by A88,XBOOLE_1:16;
end;
end;
hence thesis;
end;
suppose
A92: not E\E9 = {};
meet rng g = (meet rng f) /\ meet rng f9
proof
E\E9 c= E & E c= dom g by A8,XBOOLE_1:7,36;
then
A93: rng (g|(E\E9)) <> {} by A92,Th1,XBOOLE_1:1;
A94: E /\ E9 c= E \/ E9 by XBOOLE_1:29;
per cases;
suppose
A95: E9\E = {};
then
A96: rng (f|(E9\E)) = {};
E9 c= E by A95,XBOOLE_1:37;
then E = E \/ E9 by XBOOLE_1:12;
then dom f = E \/ E9 by FUNCT_2:def 1;
then
A97: rng f = rng (f|(E /\ E9)) \/ rng (f|(E\E9)) \/ rng (f|
(E9\E)) by A49
.= rng (f|(E /\ E9)) \/ rng (f|(E\E9)) by A96;
E\E9 c= E by XBOOLE_1:36;
then
A98: E\E9 c= dom f by FUNCT_2:def 1;
E9 c= E by A95,XBOOLE_1:37;
then
A99: f9|(E /\ E9) = f9 by RELSET_1:19,XBOOLE_1:19;
dom f = E by FUNCT_2:def 1;
then
A100: rng (f|(E /\ E9)) <> {} by A81,Th1,XBOOLE_1:17;
rng (g|(E9\E)) = {} by A95;
then meet rng g = (meet rng (g|(E /\ E9))) /\ meet rng (g|(
E\E9)) by A8,A63,A81,A94,A93,SETFAM_1:9
.= ((meet rng (f|(E /\ E9))) /\ (meet rng (f|(E\E9))))
/\ meet rng (f9|(E /\ E9)) by A17,A73,XBOOLE_1:16;
hence thesis by A92,A99,A97,A100,A98,SETFAM_1:9;
end;
suppose
A101: not E9\E = {};
E9\E c= E9 & E9 c= E \/ E9 by XBOOLE_1:7,36;
then E9\E c= dom g by A8;
then meet rng g = (meet (rng (g|(E /\ E9)) \/ rng (g|(E\E9)
))) /\ meet rng (g|(E9\E)) by A8,A63,A81,A94,A101,SETFAM_1:9
.= meet rng (g|(E /\ E9)) /\ meet rng (g|(E\E9)) /\ meet
rng (g|(E9\E)) by A8,A81,A94,A93,SETFAM_1:9;
then
A102: meet rng g = meet rng (f|(E /\ E9)) /\ meet rng (f|(E\
E9)) /\ meet rng (f9|(E /\ E9)) /\ meet rng (f9|(E9\E)) by A17,A73,A68,
XBOOLE_1:16;
E /\ E9 c= E by XBOOLE_1:17;
then
A103: E /\ E9 c= dom f by FUNCT_2:def 1;
E \/ (E /\ E9) = E by XBOOLE_1:12,17;
then dom f = E \/ (E /\ E9) by FUNCT_2:def 1;
then
A104: rng f = (rng (f|(E /\ (E /\ E9))) \/ rng (f|(E \ (E /\
E9)))) \/ rng (f|((E /\ E9) \ E)) by A49;
E /\ E9 c= E by XBOOLE_1:17;
then (E /\ E9) \ E = {} by XBOOLE_1:37;
then
A105: rng (f|((E /\ E9) \ E)) = {};
E9\E c= E9 by XBOOLE_1:36;
then
A106: E9\E c= dom f9 by FUNCT_2:def 1;
E /\ E9 c= E9 by XBOOLE_1:17;
then
A107: E /\ E9 c= dom f9 by FUNCT_2:def 1;
E /\ E9 c= E9 by XBOOLE_1:17;
then
A108: E9\E = E9 \ (E /\ E9) & (E /\ E9) \ E9 = {} by XBOOLE_1:37,47
;
E9 \/ (E /\ E9) = E9 by XBOOLE_1:12,17;
then
A109: dom f9 = E9 \/ (E /\ E9) by FUNCT_2:def 1;
E9 /\ (E /\ E9) = (E9 /\ E9) /\ E by XBOOLE_1:16
.= E /\ E9;
then rng f9 = (rng (f9|(E /\ E9)) \/ rng (f9|(E9\E))) \/
rng (f9|{}) by A49,A109,A108;
then
A110: meet rng f9 = meet rng (f9|(E /\ E9)) /\ meet rng (f9|
(E9\E)) by A81,A101,A107,A106,SETFAM_1:9;
E\E9 c= E by XBOOLE_1:36;
then
A111: E\E9 c= dom f by FUNCT_2:def 1;
E /\ (E /\ E9) = (E /\ E) /\ E9 by XBOOLE_1:16
.= E /\ E9;
then rng f = rng (f|(E /\ E9)) \/ rng (f|(E\E9)) by A104,A105
,XBOOLE_1:47;
then meet rng f = meet rng (f|(E /\ E9)) /\ meet rng (f|(E\
E9)) by A81,A92,A103,A111,SETFAM_1:9;
hence thesis by A110,A102,XBOOLE_1:16;
end;
end;
hence thesis;
end;
end;
hence thesis by A4,A6;
end;
end;
for y being object
holds y in (meet rng f /\ meet rng f9) implies y in Omega
proof let y be object;
consider S being object such that
A112: S in rng f by XBOOLE_0:def 1;
consider S9 being object such that
A113: S9 in rng f9 by XBOOLE_0:def 1;
assume
A114: y in meet rng f /\ meet rng f9;
reconsider S,S9 as set by TARSKI:1;
y in meet rng f9 by XBOOLE_0:def 4,A114;
then
A115: y in S9 by A113,SETFAM_1:def 1;
y in meet rng f by A114,XBOOLE_0:def 4;
then y in S by A112,SETFAM_1:def 1;
then
A116: y in S /\ S9 by A115,XBOOLE_0:def 4;
S /\ S9 is Event of Sigma by A112,A113,PROB_1:19;
hence thesis by A116;
end;
then reconsider xX = x /\ X as Subset of Omega by A4,A6,TARSKI:def 3;
E \/ E9 c= J by A3,A5,XBOOLE_1:8;
then xX in MeetSections(J,F) by A16,Def9;
hence thesis;
end;
hence thesis by FINSUB_1:def 2;
end;
end;
theorem Th14:
for F being ManySortedSigmaField of I,Sigma, J,K being non empty
Subset of I st F is_independent_wrt P & J misses K holds for u,v st u in sigUn(
F,J) & v in sigUn(F,K) holds P.(u /\ v) = P.u * P.v
proof
let F be ManySortedSigmaField of I,Sigma, J,K be non empty Subset of I;
A1: MeetSections(J,F) is non empty Subset of Sigma & MeetSections(K,F) is
non empty Subset of Sigma by Th13;
assume
A2: F is_independent_wrt P & J misses K;
A3: for p,q st p in MeetSections(J,F) & q in MeetSections(K,F) holds p,q
are_independent_respect_to P
proof
let p,q;
assume
A4: p in MeetSections(J,F) & q in MeetSections(K,F);
reconsider p,q as Subset of Omega;
P.(p /\ q) = P.p * P.q by A2,A4,Th12;
hence thesis by PROB_2:def 4;
end;
let u,v;
assume u in sigUn(F,J) & v in sigUn(F,K);
then u in sigma(MeetSections(J,F)) & v in sigma(MeetSections (K,F)) by Th11;
then u,v are_independent_respect_to P by A1,A3,Th10;
hence thesis by PROB_2:def 4;
end;
definition
let I be set, Omega be non empty set, Sigma be SigmaField of Omega, F be
ManySortedSigmaField of I, Sigma;
func finSigmaFields(F,I) -> Subset-Family of Omega means
:Def10:
for S being
Subset of Omega holds S in it iff ex E being finite Subset of I st S in sigUn(F
,E);
existence
proof
defpred P[object] means ex E being finite Subset of I st $1 in sigUn(F,E);
consider X such that
A1: for x being object holds
x in X iff x in bool Omega & P[x] from XBOOLE_0:sch 1;
for x being object holds x in X implies x in bool Omega by A1;
then reconsider X as Subset-Family of Omega by TARSKI:def 3;
take X;
let S be Subset of Omega;
thus thesis by A1;
end;
uniqueness
proof
let X1,X2 be Subset-Family of Omega;
assume
A2: for S being Subset of Omega holds S in X1 iff ex E being finite
Subset of I st S in sigUn(F,E);
assume
A3: for S being Subset of Omega holds S in X2 iff ex E being finite
Subset of I st S in sigUn(F,E);
now
let S be Subset of Omega;
S in X1 iff ex E being finite Subset of I st S in sigUn(F,E) by A2;
hence S in X1 iff S in X2 by A3;
end;
hence thesis by SUBSET_1:3;
end;
end;
theorem Th15:
for F being ManySortedSigmaField of I, Sigma holds
tailSigmaField(F,I) is SigmaField of Omega
proof
let F be ManySortedSigmaField of I, Sigma;
A1: for A1 being SetSequence of Omega st rng A1 c= tailSigmaField(F,I) holds
Intersection A1 in tailSigmaField(F,I)
proof
let A1 be SetSequence of Omega;
assume
A2: rng A1 c= tailSigmaField(F,I);
A3: for n holds for S holds S in futSigmaFields(F,I) implies A1.n in S
proof
let n, S;
A4: A1.n in rng A1 by NAT_1:51;
assume S in futSigmaFields(F,I);
hence thesis by A2,A4,SETFAM_1:def 1;
end;
for S st S in futSigmaFields(F,I) holds (Union Complement A1)` in S
proof
let S;
assume
A5: S in futSigmaFields(F,I);
then ex E being finite Subset of I st S = sigUn(F,I\E) by Def7;
then reconsider S as SigmaField of Omega;
for n being Nat holds (Complement A1).n in S
proof
let n be Nat;
reconsider n as Element of NAT by ORDINAL1:def 12;
A1.n in S by A3,A5;
then (A1.n)` is Event of S by PROB_1:20;
then (A1.n)` in S;
hence thesis by PROB_1:def 2;
end;
then rng Complement A1 c= S by NAT_1:52;
then reconsider CA1= Complement A1 as SetSequence of S by RELAT_1:def 19;
Union CA1 in S by PROB_1:17;
then (Union Complement A1)` is Event of S by PROB_1:20;
hence thesis;
end;
hence thesis by SETFAM_1:def 1;
end;
for A being Subset of Omega st A in tailSigmaField(F,I) holds A` in
tailSigmaField(F,I)
proof
let A be Subset of Omega;
assume
A6: A in tailSigmaField(F,I);
for S holds S in futSigmaFields(F,I) implies A` in S
proof
let S;
assume
A7: S in futSigmaFields(F,I);
then consider E being finite Subset of I such that
A8: S=sigUn(F,I\E) by Def7;
A in S by A6,A7,SETFAM_1:def 1;
then A` is Event of sigma (Union (F|(I\E))) by A8,PROB_1:20;
hence thesis by A8;
end;
hence thesis by SETFAM_1:def 1;
end;
hence thesis by A1,PROB_1:15;
end;
::$N Koenig Lemma
theorem
for F being ManySortedSigmaField of I,Sigma st F is_independent_wrt P
& a in tailSigmaField(F,I) holds P.a=0 or P.a=1
proof
let F be ManySortedSigmaField of I,Sigma;
reconsider T=tailSigmaField(F,I) as SigmaField of Omega by Th15;
set Ie=I\{}I;
A1: a in tailSigmaField(F,I) implies a in sigUn(F,Ie)
proof
assume
A2: a in tailSigmaField(F,I);
sigUn(F,Ie) in futSigmaFields(F,I) by Def7;
hence thesis by A2,SETFAM_1:def 1;
end;
assume
A3: F is_independent_wrt P;
A4: for E being finite Subset of I for p,q st p in sigUn(F,E) & q in
tailSigmaField(F,I) holds p,q are_independent_respect_to P
proof
let E be finite Subset of I;
let p,q;
assume that
A5: p in sigUn(F,E) and
A6: q in tailSigmaField(F,I);
for E being finite Subset of I holds q in sigUn(F,I\E)
proof
let E be finite Subset of I;
sigUn(F,I\E) in futSigmaFields(F,I) by Def7;
hence thesis by A6,SETFAM_1:def 1;
end;
then
A7: q in sigUn(F,I\E);
per cases;
suppose
A8: E <> {} & I\E <> {};
then reconsider E as non empty Subset of I;
reconsider IE=I\E as non empty Subset of I by A8;
E misses IE by XBOOLE_1:79;
then P.(p /\ q) = P.p * P.q by A3,A5,A7,Th14;
hence thesis by PROB_2:def 4;
end;
suppose
A9: not (E <> {} & I\E <> {});
reconsider e={} as Subset of I by XBOOLE_1:2;
A10: for u,v st u in {{},Omega} holds u,v are_independent_respect_to P
proof
let u,v;
assume
A11: u in {{},Omega};
per cases;
suppose
u={};
hence thesis by PROB_2:19,23;
end;
suppose
u<>{};
then u=[#]Sigma by A11,TARSKI:def 2;
hence thesis by PROB_2:19,24;
end;
end;
Union (F|{}) = {} by ZFMISC_1:2;
then
A12: sigUn(F,e) = {{},Omega} by Th3;
p,q are_independent_respect_to P
proof
per cases;
suppose
E={};
hence thesis by A5,A12,A10;
end;
suppose
E<>{};
hence thesis by A7,A9,A12,A10,PROB_2:19;
end;
end;
hence thesis;
end;
end;
A13: for p,q st p in finSigmaFields(F,I) & q in tailSigmaField(F,I) holds p,
q are_independent_respect_to P
proof
let p,q;
assume that
A14: p in finSigmaFields(F,I) and
A15: q in tailSigmaField(F,I);
ex E being finite Subset of I st p in sigUn(F,E) by A14,Def10;
hence thesis by A4,A15;
end;
Union (F|Ie) c= sigma finSigmaFields(F,I)
proof
let x be object;
assume x in Union (F|Ie);
then x in union rng F;
then consider y such that
A16: x in y and
A17: y in rng F by TARSKI:def 4;
consider i being object such that
A18: i in dom F and
A19: y=F.i by A17,FUNCT_1:def 3;
A20: x in finSigmaFields(F,I)
proof
reconsider Fi=F.i as SigmaField of Omega by A18,Def2;
A21: sigma(Fi) c= Fi & Fi c= sigma(Fi) by PROB_1:def 9;
i in I by A18;
then for z being object holds
z in {i} implies z in I by TARSKI:def 1;
then reconsider E={i} as finite Subset of I by TARSKI:def 3;
A22: dom (F|{i}) = dom F /\ {i} by RELAT_1:61
.= {i} by A18,ZFMISC_1:46;
then rng (F|{i}) = {(F|{i}).i} by FUNCT_1:4;
then
A23: union rng (F|{i}) = (F|{i}).i by ZFMISC_1:25;
i in dom (F|{i}) by A22,TARSKI:def 1;
then Union F|{i} = F.i by A23,FUNCT_1:47;
then sigUn(F,E) = F.i by A21;
hence thesis by A16,A19,Def10;
end;
finSigmaFields(F,I) c= sigma finSigmaFields(F,I) by PROB_1:def 9;
hence thesis by A20;
end;
then
A24: T c= sigma(T) & sigUn(F,Ie) c= sigma finSigmaFields(F,I) by PROB_1:def 9;
A25: for u,v st u in sigUn(F,Ie) & v in tailSigmaField(F,I) holds u,v
are_independent_respect_to P
proof
for x,y st x in finSigmaFields(F,I) & y in finSigmaFields(F,I) holds
x /\ y in finSigmaFields(F,I)
proof
let x,y;
assume that
A26: x in finSigmaFields(F,I) and
A27: y in finSigmaFields(F,I);
consider E1 being finite Subset of I such that
A28: x in sigUn(F,E1) by A26,Def10;
consider E2 being finite Subset of I such that
A29: y in sigUn(F,E2) by A27,Def10;
A30: for E1,E2 being finite Subset of I holds z in sigUn(F,E1) implies z
in sigUn(F,E1 \/ E2)
proof
let E1,E2 be finite Subset of I;
reconsider E3 = E1 \/ E2 as finite Subset of I;
A31: Union (F|E1) c= Union (F|E3)
proof
let X be object;
assume X in Union (F|E1);
then consider S such that
A32: X in S and
A33: S in rng (F|E1) by TARSKI:def 4;
F|(E3) = (F|E1) \/ (F|E2) by RELAT_1:78;
then rng (F|E3) = rng (F|E1) \/ rng(F|E2) by RELAT_1:12;
then S in rng (F|E3) by A33,XBOOLE_0:def 3;
hence thesis by A32,TARSKI:def 4;
end;
Union (F|E3) c= sigma Union(F|E3) by PROB_1:def 9;
then Union (F|E1) c= sigma Union(F|E3) by A31;
then
A34: sigma Union(F|E1) c= sigma Union(F|E3) by PROB_1:def 9;
assume z in sigUn(F,E1);
hence thesis by A34;
end;
then
A35: y in sigUn(F,E2 \/ E1) by A29;
x in sigUn(F,E1 \/ E2) by A28,A30;
then x /\ y in sigUn(F,E1 \/ E2) by A35,FINSUB_1:def 2;
hence thesis by Def10;
end;
then
A36: finSigmaFields(F,I) is intersection_stable by FINSUB_1:def 2;
let u,v;
A37: finSigmaFields(F,I) is non empty
proof
set E = the finite Subset of I;
{} in sigUn(F,E) by PROB_1:4;
hence thesis by Def10;
end;
A38: tailSigmaField(F,I) c= Sigma
proof
set Ie=I\{}I;
let x be object;
assume
A39: x in tailSigmaField(F,I);
Union (F|Ie) c= Sigma
proof
let y be object;
assume y in Union (F|Ie);
then ex S st y in S & S in rng (F|Ie) by TARSKI:def 4;
hence thesis;
end;
then
A40: sigma Union (F|Ie) c= Sigma by PROB_1:def 9;
sigUn(F,Ie) in futSigmaFields(F,I) by Def7;
then x in sigma Union (F|Ie) by A39,SETFAM_1:def 1;
hence thesis by A40;
end;
A41: finSigmaFields(F,I) c= Sigma
proof
let x be object;
assume x in finSigmaFields(F,I);
then consider E being finite Subset of I such that
A42: x in sigUn(F,E) by Def10;
Union (F|E) c= Sigma
proof
let y be object;
assume y in Union (F|E);
then ex S st y in S & S in rng (F|E) by TARSKI:def 4;
hence thesis;
end;
then sigma Union (F|E) c= Sigma by PROB_1:def 9;
hence thesis by A42;
end;
assume u in sigUn(F,Ie) & v in tailSigmaField(F,I);
hence thesis by A13,A24,A37,A41,A36,A38,Th10;
end;
assume a in tailSigmaField(F,I);
then a,a are_independent_respect_to P by A1,A25;
then P.(a /\ a) = P.a * P.a by PROB_2:def 4;
hence thesis by Th2;
end;