begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th4:
for
r,
r1,
r2,
r3 being
Real st
r <> 0 &
r1 <> 0 holds
(
r3 / r1 = r2 / r iff
r3 * r = r2 * r1 )
theorem Th5:
:: deftheorem defines @Intersection PROB_2:def 1 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma holds @Intersection ASeq = Intersection ASeq;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th9:
theorem Th10:
theorem
canceled;
theorem Th12:
theorem Th13:
theorem
theorem
theorem
canceled;
theorem Th17:
Lm1:
for Omega being non empty set
for ASeq being SetSequence of Omega holds
( ASeq is non-descending iff Complement ASeq is non-ascending )
:: deftheorem defines @Complement PROB_2:def 2 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma holds @Complement ASeq = Complement ASeq;
:: deftheorem Def3 defines disjoint_valued PROB_2:def 3 :
for F being Function holds
( F is disjoint_valued iff for x, y being set st x <> y holds
F . x misses F . y );
:: deftheorem defines disjoint_valued PROB_2:def 4 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma holds
( ASeq is disjoint_valued iff for m, n being Element of NAT st m <> n holds
ASeq . m misses ASeq . n );
Lm2:
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for ASeq being SetSequence of Sigma st ASeq is non-descending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) )
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem
:: deftheorem Def5 defines are_independent_respect_to PROB_2:def 5 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B being Event of Sigma holds
( A,B are_independent_respect_to P iff P . (A /\ B) = (P . A) * (P . B) );
:: deftheorem Def6 defines are_independent_respect_to PROB_2:def 6 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B, C being Event of Sigma holds
( A,B,C are_independent_respect_to P iff ( P . ((A /\ B) /\ C) = ((P . A) * (P . B)) * (P . C) & P . (A /\ B) = (P . A) * (P . B) & P . (A /\ C) = (P . A) * (P . C) & P . (B /\ C) = (P . B) * (P . C) ) );
theorem
canceled;
theorem
canceled;
theorem Th31:
theorem Th32:
theorem
theorem
theorem
theorem
theorem Th37:
theorem Th38:
theorem
theorem
:: deftheorem Def7 defines .|. PROB_2:def 7 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for B being Event of Sigma st 0 < P . B holds
for b5 being Probability of Sigma holds
( b5 = P .|. B iff for A being Event of Sigma holds b5 . A = (P . (A /\ B)) / (P . B) );
theorem
canceled;
theorem Th42:
theorem
theorem Th44:
theorem Th45:
theorem
theorem
theorem
theorem Th49:
theorem
theorem
theorem