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

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

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

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

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) )
proof end;
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) ) ) & ( 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
proof end;
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) ) & f is V71() holds
P . (b /\ ()) = (P . b) * (P . ())
proof end;

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
proof end;

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 & A c= Indep (B,P) holds
sigma A c= Indep (B,P)
proof end;

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 & q in B holds
p,q are_independent_respect_to P )
proof end;

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)
proof end;

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 & A is intersection_stable holds
for B being non empty Subset of Sigma st B is intersection_stable & A c= Indep (B,P) holds
for D being Subset-Family of Omega
for sB being non empty Subset of Sigma st D = B & sigma D = sB holds
sigma A c= Indep (sB,P)
proof end;

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 & E is intersection_stable & F is non empty Subset of Sigma & F is intersection_stable & ( for p, q being Event of Sigma st p in E & q in F holds
p,q are_independent_respect_to P ) holds
for u, v being Event of Sigma st u in sigma E & v in sigma F holds
u,v are_independent_respect_to P
proof end;

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
proof end;
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;
pred A is_independent_wrt P means :: 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 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
proof end;
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;
pred F is_independent_wrt P means :: 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 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 func F | 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
proof end;
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)) )
proof end;
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)) ) ) & ( 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
proof end;
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
proof end;
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
proof end;
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 & 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 & x = meet (rng f) ) )
proof end;
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 & x = meet (rng f) ) ) ) & ( 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 & x = meet (rng f) ) ) ) holds
b1 = b2
proof end;
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 & 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)
proof end;

theorem Th12: :: KOLMOG01:12
for Omega, I 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 & 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 end;

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
proof end;

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;
coherence
MeetSections (J,F) is intersection_stable
proof end;
end;

theorem Th14: :: KOLMOG01:14
for Omega, I 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 & J misses K holds
for u, v being Event of Sigma st u in sigUn (F,J) & v in sigUn (F,K) holds
P . (u /\ v) = (P . u) * (P . v)
proof 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 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) )
proof end;
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) ) ) & ( 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
proof end;
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 Omega, I 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
proof end;

:: 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 & a in tailSigmaField (F,I) & not P . a = 0 holds
P . a = 1
proof end;