:: 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 b₁ being Subset of Sigma st
for a being Element of Sigma holds
( a in b₁ iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) )

proof end;

uniqueness
for b₁, b₂ being Subset of Sigma st ( for a being Element of Sigma holds
( a in b₁ iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) ) ) & ( for a being Element of Sigma holds
( a in b₂ iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) ) ) holds
b₁ = b₂

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 b₅ being Subset of Sigma holds
( b₅ = Indep (B,P) iff for a being Element of Sigma holds
( a in b₅ 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 /\ (Union f)) = (P . b) * (P . (Union f))

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 b₁ being Function of I,(bool Sigma) st
for i being set st i in I holds
b₁ . 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 b₄ being Function of I,(bool Sigma) holds
( b₄ is ManySortedSigmaField of I,Sigma iff for i being set st i in I holds
b₄ . 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 b₁ being Function of J,Sigma st
for i being set st i in J holds
b₁ . 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 b₆ being Function of J,Sigma holds
( b₆ is SigmaSection of J,F iff for i being set st i in J holds
b₆ . 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 b₁ being Subset-Family of (bool Omega) st
for S being Subset-Family of Omega holds
( S in b₁ iff ex E being finite Subset of I st S = sigUn (F,(I \ E)) )

proof end;

uniqueness
for b₁, b₂ being Subset-Family of (bool Omega) st ( for S being Subset-Family of Omega holds
( S in b₁ iff ex E being finite Subset of I st S = sigUn (F,(I \ E)) ) ) & ( for S being Subset-Family of Omega holds
( S in b₂ iff ex E being finite Subset of I st S = sigUn (F,(I \ E)) ) ) holds
b₁ = b₂

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 b₅ being Subset-Family of (bool Omega) holds
( b₅ = futSigmaFields (F,I) iff for S being Subset-Family of Omega holds
( S in b₅ 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 b₁ being Subset-Family of Omega st
for x being Subset of Omega holds
( x in b₁ 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 b₁, b₂ being Subset-Family of Omega st ( for x being Subset of Omega holds
( x in b₁ 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 b₂ 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
b₁ = b₂

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 b₆ being Subset-Family of Omega holds
( b₆ = MeetSections (J,F) iff for x being Subset of Omega holds
( x in b₆ 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;

cluster MeetSections (J,F) -> intersection_stable ;

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 b₁ being Subset-Family of Omega st
for S being Subset of Omega holds
( S in b₁ iff ex E being finite Subset of I st S in sigUn (F,E) )

proof end;

uniqueness
for b₁, b₂ being Subset-Family of Omega st ( for S being Subset of Omega holds
( S in b₁ iff ex E being finite Subset of I st S in sigUn (F,E) ) ) & ( for S being Subset of Omega holds
( S in b₂ iff ex E being finite Subset of I st S in sigUn (F,E) ) ) holds
b₁ = b₂

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 b₅ being Subset-Family of Omega holds
( b₅ = finSigmaFields (F,I) iff for S being Subset of Omega holds
( S in b₅ 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;