:: Kolmogorov's Zero-one Law :: by Agnes Doll :: :: Received November 4, 2008 :: Copyright (c) 2008-2021 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; 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 :: KOLMOG01:1 for f being Function, X being set st X c= dom f holds X <> {} implies rng (f|X) <> {}; theorem :: KOLMOG01:2 for r being Real st r*r=r holds r=0 or r=1; theorem :: KOLMOG01:3 for X being Subset-Family of Omega st X={} holds sigma(X) = {{}, Omega}; 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 :: 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; end; theorem :: KOLMOG01:4 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; theorem :: KOLMOG01:5 Indep(B,P) is Dynkin_System of Omega; theorem :: KOLMOG01:6 for A being Subset-Family of Omega st A is intersection_stable & A c= Indep(B,P) holds sigma(A) c= Indep(B,P); theorem :: KOLMOG01:7 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; theorem :: KOLMOG01:8 for A,B being non empty Subset of Sigma st A c= Indep(B,P) holds B c= Indep(A,P); theorem :: KOLMOG01:9 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); theorem :: KOLMOG01:10 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; 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 :: KOLMOG01:def 2 for i st i in I holds it.i is SigmaField of Omega; 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 :: 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; 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 :: KOLMOG01:def 4 for i st i in J holds it.i in F.i; 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 :: KOLMOG01:def 5 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; 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; 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 :: KOLMOG01:def 6 sigma Union (F|J); 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 :: 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); 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; 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 :: KOLMOG01:def 8 meet futSigmaFields(F,I); 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; 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 :: KOLMOG01:def 9 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; end; theorem :: KOLMOG01:11 for F being ManySortedSigmaField of I, Sigma, J being non empty Subset of I holds sigma MeetSections(J,F) = sigUn(F,J); theorem :: KOLMOG01:12 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; theorem :: KOLMOG01:13 for F being ManySortedSigmaField of I,Sigma, J being non empty Subset of I holds MeetSections(J,F) is non empty Subset of Sigma; 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; end; theorem :: KOLMOG01:14 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; 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 :: 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); end; theorem :: KOLMOG01:15 for F being ManySortedSigmaField of I, Sigma holds tailSigmaField(F,I) is SigmaField of Omega; ::$N Koenig Lemma theorem :: KOLMOG01:16 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;