begin
theorem Th1:
theorem Th2:
for
r being
Real holds
( not
r * r = r or
r = 0 or
r = 1 )
theorem Th3:
:: 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:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
:: 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 );
:: 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))) );
:: 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 );
:: 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 );
:: 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));
:: 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)) ) );
:: 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));
:: 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:
theorem Th12:
theorem Th13:
theorem Th14:
:: 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:
theorem