:: Kolmogorov's Zero-one Law
:: by Agnes Doll
::
:: Received November 4, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users


begin

theorem Th1: :: KOLMOG01:1
for f being Function
for X being set st X c= dom f &amp; X <> {} holds
rng (f | X) <> {}
proofend;

theorem Th2: :: KOLMOG01:2
for r being Real holds
( not r * r = r or r = 0 or r = 1 )
proofend;

theorem Th3: :: KOLMOG01:3
for Omega being non empty set
for X being Subset-Family of Omega st X = {} holds
sigma X = {{},Omega}
proofend;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let B be Subset of Sigma;
let P be Probability of Sigma;
func Indep (B,P) ->  Subset of Sigma means :Def1: :: KOLMOG01:def 1
 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
 ex b1 being Subset of Sigma st
for a being Element of Sigma holds
( a in b1 iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) )
proofend;
uniqueness
 for b1, b2 being Subset of Sigma st ( for a being Element of Sigma holds
( a in b1 iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) ) ) &amp; ( for a being Element of Sigma holds
( a in b2 iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines Indep KOLMOG01:def_1_:_
 for Omega being non empty set
for Sigma being SigmaField of Omega
for B being Subset of Sigma
for P being Probability of Sigma
for b5 being Subset of Sigma holds
( b5 = Indep (B,P) iff for a being Element of Sigma holds
( a in b5 iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) ) );

theorem Th4: :: KOLMOG01:4
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for B being non empty Subset of Sigma
for b being Element of B
for f being SetSequence of Sigma st ( for n being Element of NAT
for b being Element of B holds P . ((f . n) /\ b) = (P . (f . n)) * (P . b) ) &amp; f is V65() holds
P . (b /\ (Union f)) = (P . b) * (P . (Union f))
proofend;

theorem Th5: :: KOLMOG01:5
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for B being non empty Subset of Sigma holds Indep (B,P) is Dynkin_System of Omega
proofend;

theorem Th6: :: KOLMOG01:6
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for B being non empty Subset of Sigma
for A being Subset-Family of Omega st A is intersection_stable &amp; A c= Indep (B,P) holds
sigma A c= Indep (B,P)
proofend;

theorem Th7: :: KOLMOG01:7
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B being non empty Subset of Sigma holds
( A c= Indep (B,P) iff for p, q being Event of Sigma st p in A &amp; q in B holds
p,q are_independent_respect_to P )
proofend;

theorem Th8: :: KOLMOG01:8
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B being non empty Subset of Sigma st A c= Indep (B,P) holds
B c= Indep (A,P)
proofend;

theorem Th9: :: KOLMOG01:9
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Subset-Family of Omega st A is non empty Subset of Sigma &amp; A is intersection_stable holds
for B being non empty Subset of Sigma st B is intersection_stable &amp; A c= Indep (B,P) holds
for D being Subset-Family of Omega
for sB being non empty Subset of Sigma st D = B &amp; sigma D = sB holds
sigma A c= Indep (sB,P)
proofend;

theorem Th10: :: KOLMOG01:10
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for E, F being Subset-Family of Omega st E is non empty Subset of Sigma &amp; E is intersection_stable &amp; F is non empty Subset of Sigma &amp; F is intersection_stable &amp; ( for p, q being Event of Sigma st p in E &amp; q in F holds
p,q are_independent_respect_to P ) holds
for u, v being Event of Sigma st u in sigma E &amp; v in sigma F holds
u,v are_independent_respect_to P
proofend;

definition
let I be set ;
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
mode ManySortedSigmaField of I,Sigma ->  Function of I,(bool Sigma) means :Def2: :: KOLMOG01:def 2
 for i being set st i in I holds
it . i is SigmaField of Omega;
existence
 ex b1 being Function of I,(bool Sigma) st
for i being set st i in I holds
b1 . i is SigmaField of Omega
proofend;
end;

:: deftheorem Def2 defines ManySortedSigmaField KOLMOG01:def_2_:_
 for I being set
for Omega being non empty set
for Sigma being SigmaField of Omega
for b4 being Function of I,(bool Sigma) holds
( b4 is ManySortedSigmaField of I,Sigma iff for i being set st i in I holds
b4 . i is SigmaField of Omega );

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
let I be set ;
let A be Function of I,Sigma;
predA is_independent_wrt P means :Def3: :: KOLMOG01:def 3
 for e being one-to-one FinSequence of I st e <> {} holds
Product ((P * A) * e) = P . (meet (rng (A * e)));
end;

:: deftheorem Def3 defines is_independent_wrt KOLMOG01:def_3_:_
 for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for I being set
for A being Function of I,Sigma holds
( A is_independent_wrt P iff for e being one-to-one FinSequence of I st e <> {} holds
Product ((P * A) * e) = P . (meet (rng (A * e))) );

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let I be set ;
let J be Subset of I;
let F be ManySortedSigmaField of I,Sigma;
mode SigmaSection of J,F ->  Function of J,Sigma means :Def4: :: KOLMOG01:def 4
 for i being set st i in J holds
it . i in F . i;
existence
 ex b1 being Function of J,Sigma st
for i being set st i in J holds
b1 . i in F . i
proofend;
end;

:: deftheorem Def4 defines SigmaSection KOLMOG01:def_4_:_
 for Omega being non empty set
for Sigma being SigmaField of Omega
for I being set
for J being Subset of I
for F being ManySortedSigmaField of I,Sigma
for b6 being Function of J,Sigma holds
( b6 is SigmaSection of J,F iff for i being set st i in J holds
b6 . i in F . i );

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
let I be set ;
let F be ManySortedSigmaField of I,Sigma;
predF is_independent_wrt P means :Def5: :: KOLMOG01:def 5
 for E being finite Subset of I
for A being SigmaSection of E,F holds A is_independent_wrt P;
end;

:: deftheorem Def5 defines is_independent_wrt KOLMOG01:def_5_:_
 for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for I being set
for F being ManySortedSigmaField of I,Sigma holds
( F is_independent_wrt P iff for E being finite Subset of I
for A being SigmaSection of E,F holds A is_independent_wrt P );

definition
let I be set ;
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let F be ManySortedSigmaField of I,Sigma;
let J be Subset of I;
:: original:|
redefine funcF | J ->  Function of J,(bool Sigma);
coherence
 F | J is Function of J,(bool Sigma) by FUNCT_2:32;
end;

definition
let I be set ;
let J be Subset of I;
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let F be Function of J,(bool Sigma);
:: original:Union
redefine func Union F ->  Subset-Family of Omega;
coherence
 Union F is Subset-Family of Omega
proofend;
end;

definition
let I be set ;
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let F be ManySortedSigmaField of I,Sigma;
let J be Subset of I;
func sigUn (F,J) ->  SigmaField of Omega equals :: KOLMOG01:def 6
 sigma (Union (F | J));
coherence
 sigma (Union (F | J)) is SigmaField of Omega ;
end;

:: deftheorem  defines sigUn KOLMOG01:def_6_:_
 for I being set
for Omega being non empty set
for Sigma being SigmaField of Omega
for F being ManySortedSigmaField of I,Sigma
for J being Subset of I holds sigUn (F,J) = sigma (Union (F | J));

definition
let I be set ;
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let F be ManySortedSigmaField of I,Sigma;
func futSigmaFields (F,I) ->  Subset-Family of (bool Omega) means :Def7: :: KOLMOG01:def 7
 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
 ex b1 being Subset-Family of (bool Omega) st
for S being Subset-Family of Omega holds
( S in b1 iff ex E being finite Subset of I st S = sigUn (F,(I \ E)) )
proofend;
uniqueness
 for b1, b2 being Subset-Family of (bool Omega) st ( for S being Subset-Family of Omega holds
( S in b1 iff ex E being finite Subset of I st S = sigUn (F,(I \ E)) ) ) &amp; ( for S being Subset-Family of Omega holds
( S in b2 iff ex E being finite Subset of I st S = sigUn (F,(I \ E)) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines futSigmaFields KOLMOG01:def_7_:_
 for I being set
for Omega being non empty set
for Sigma being SigmaField of Omega
for F being ManySortedSigmaField of I,Sigma
for b5 being Subset-Family of (bool Omega) holds
( b5 = futSigmaFields (F,I) iff for S being Subset-Family of Omega holds
( S in b5 iff ex E being finite Subset of I st S = sigUn (F,(I \ E)) ) );

registration
let I be set ;
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let F be ManySortedSigmaField of I,Sigma;
cluster futSigmaFields (F,I) ->  non empty ;
coherence
 not futSigmaFields (F,I) is empty
proofend;
end;

definition
let I be set ;
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let F be ManySortedSigmaField of I,Sigma;
func tailSigmaField (F,I) ->  Subset-Family of Omega equals :: KOLMOG01:def 8
 meet (futSigmaFields (F,I));
coherence
 meet (futSigmaFields (F,I)) is Subset-Family of Omega ;
end;

:: deftheorem  defines tailSigmaField KOLMOG01:def_8_:_
 for I being set
for Omega being non empty set
for Sigma being SigmaField of Omega
for F being ManySortedSigmaField of I,Sigma holds tailSigmaField (F,I) = meet (futSigmaFields (F,I));

registration
let I be set ;
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let F be ManySortedSigmaField of I,Sigma;
cluster tailSigmaField (F,I) ->  non empty ;
coherence
 not tailSigmaField (F,I) is empty
proofend;
end;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let I be non empty set ;
let J be non empty Subset of I;
let F be ManySortedSigmaField of I,Sigma;
func MeetSections (J,F) ->  Subset-Family of Omega means :Def9: :: KOLMOG01:def 9
 for x being Subset of Omega holds
( x in it iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J &amp; x = meet (rng f) ) );
existence
 ex b1 being Subset-Family of Omega st
for x being Subset of Omega holds
( x in b1 iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J &amp; x = meet (rng f) ) )
proofend;
uniqueness
 for b1, b2 being Subset-Family of Omega st ( for x being Subset of Omega holds
( x in b1 iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J &amp; x = meet (rng f) ) ) ) &amp; ( for x being Subset of Omega holds
( x in b2 iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J &amp; x = meet (rng f) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines MeetSections KOLMOG01:def_9_:_
 for Omega being non empty set
for Sigma being SigmaField of Omega
for I being non empty set
for J being non empty Subset of I
for F being ManySortedSigmaField of I,Sigma
for b6 being Subset-Family of Omega holds
( b6 = MeetSections (J,F) iff for x being Subset of Omega holds
( x in b6 iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J &amp; x = meet (rng f) ) ) );

theorem Th11: :: KOLMOG01:11
for Omega, I being non empty set
for Sigma being SigmaField of Omega
for F being ManySortedSigmaField of I,Sigma
for J being non empty Subset of I holds sigma (MeetSections (J,F)) = sigUn (F,J)
proofend;

theorem Th12: :: KOLMOG01:12
for I, Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for F being ManySortedSigmaField of I,Sigma
for J, K being non empty Subset of I st F is_independent_wrt P &amp; J misses K holds
for a, c being Subset of Omega st a in MeetSections (J,F) &amp; c in MeetSections (K,F) holds
P . (a /\ c) = (P . a) * (P . c)
proofend;

theorem Th13: :: KOLMOG01:13
for Omega, I being non empty set
for Sigma being SigmaField of Omega
for F being ManySortedSigmaField of I,Sigma
for J being non empty Subset of I holds MeetSections (J,F) is non empty Subset of Sigma
proofend;

registration
let I, Omega be non empty set ;
let Sigma be SigmaField of Omega;
let F be ManySortedSigmaField of I,Sigma;
let J be non empty Subset of I;
cluster MeetSections (J,F) ->  intersection_stable ;
coherence
 MeetSections (J,F) is intersection_stable
proofend;
end;

theorem Th14: :: KOLMOG01:14
for I, Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for F being ManySortedSigmaField of I,Sigma
for J, K being non empty Subset of I st F is_independent_wrt P &amp; J misses K holds
for u, v being Event of Sigma st u in sigUn (F,J) &amp; v in sigUn (F,K) holds
P . (u /\ v) = (P . u) * (P . v)
proofend;

definition
let I be set ;
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let F be ManySortedSigmaField of I,Sigma;
func finSigmaFields (F,I) ->  Subset-Family of Omega means :Def10: :: KOLMOG01:def 10
 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
 ex b1 being Subset-Family of Omega st
for S being Subset of Omega holds
( S in b1 iff ex E being finite Subset of I st S in sigUn (F,E) )
proofend;
uniqueness
 for b1, b2 being Subset-Family of Omega st ( for S being Subset of Omega holds
( S in b1 iff ex E being finite Subset of I st S in sigUn (F,E) ) ) &amp; ( for S being Subset of Omega holds
( S in b2 iff ex E being finite Subset of I st S in sigUn (F,E) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines finSigmaFields KOLMOG01:def_10_:_
 for I being set
for Omega being non empty set
for Sigma being SigmaField of Omega
for F being ManySortedSigmaField of I,Sigma
for b5 being Subset-Family of Omega holds
( b5 = finSigmaFields (F,I) iff for S being Subset of Omega holds
( S in b5 iff ex E being finite Subset of I st S in sigUn (F,E) ) );

theorem Th15: :: KOLMOG01:15
for I, Omega being non empty set
for Sigma being SigmaField of Omega
for F being ManySortedSigmaField of I,Sigma holds tailSigmaField (F,I) is SigmaField of Omega
proofend;

:: [WP: ] Koenig_Lemma
theorem :: KOLMOG01:16
for Omega, I being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for a being Element of Sigma
for F being ManySortedSigmaField of I,Sigma st F is_independent_wrt P &amp; a in tailSigmaField (F,I) &amp; not P . a = 0 holds
P . a = 1
proofend;