:: Probability. Independence of Events and Conditional Probability
:: by Andrzej N\c{e}dzusiak
::
:: Received June 1, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

theorem Th1: :: PROB_2:1
for r, r1, r2, r3 being Real st r <> 0 &amp; r1 <> 0 holds
( r3 / r1 = r2 / r iff r3 * r = r2 * r1 )
proofend;

theorem Th2: :: PROB_2:2
for r being Real
for seq, seq1 being Real_Sequence st seq is convergent &amp; ( for n being Element of NAT holds seq1 . n = r - (seq . n) ) holds
( seq1 is convergent &amp; lim seq1 = r - (lim seq) )
proofend;

definition
let Omega be set ;
let Sigma be SigmaField of Omega;
let ASeq be SetSequence of Sigma;
let n be Element of NAT ;
:: original:.
redefine funcASeq . n ->  Event of Sigma;
coherence
 ASeq . n is Event of Sigma by PROB_1:25;
end;

definition
let Omega be set ;
let Sigma be SigmaField of Omega;
let ASeq be SetSequence of Sigma;
:: nie mozna zastapic przez redefinicje - przeplot
func @Intersection ASeq ->  Event of Sigma equals :: PROB_2:def 1
 Intersection ASeq;
coherence
 Intersection ASeq is Event of Sigma
proofend;
end;

:: deftheorem  defines @Intersection PROB_2:def_1_:_
 for Omega being set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma holds @Intersection ASeq = Intersection ASeq;

theorem Th3: :: PROB_2:3
for Omega being set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for B being Event of Sigma ex BSeq being SetSequence of Sigma st
for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B
proofend;

theorem Th4: :: PROB_2:4
for Omega being set
for Sigma being SigmaField of Omega
for ASeq, BSeq being SetSequence of Sigma
for B being Event of Sigma st ASeq is non-ascending &amp; ( for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B ) holds
BSeq is non-ascending
proofend;

theorem Th5: :: PROB_2:5
for Omega being set
for Sigma being SigmaField of Omega
for BSeq, ASeq being SetSequence of Sigma
for B being Event of Sigma st ( for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B ) holds
(Intersection ASeq) /\ B = Intersection BSeq
proofend;

registration
let Omega be set ;
let Sigma be SigmaField of Omega;
let ASeq be SetSequence of Sigma;
cluster Complement ASeq -> Sigma -valued ;
coherence
 Complement ASeq is Sigma -valued
proofend;
end;

theorem :: PROB_2:6
for X being set
for S being SetSequence of X holds
( S is non-ascending iff for n being Element of NAT holds S . (n + 1) c= S . n )
proofend;

theorem :: PROB_2:7
for X being set
for S being SetSequence of X holds
( S is non-descending iff for n being Element of NAT holds S . n c= S . (n + 1) )
proofend;

theorem Th8: :: PROB_2:8
for Omega being set
for ASeq being SetSequence of Omega holds
( ASeq is non-ascending iff Complement ASeq is non-descending )
proofend;

Lm1:  for Omega being set
for ASeq being SetSequence of Omega holds
( ASeq is non-descending iff Complement ASeq is non-ascending )
proofend;

definition
let F be Function;
attrF is disjoint_valued  means :Def2: :: PROB_2:def 2
 for x, y being set st x <> y holds
F . x misses F . y;
end;

:: deftheorem Def2 defines disjoint_valued PROB_2:def_2_:_
 for F being Function holds
( F is disjoint_valued iff for x, y being set st x <> y holds
F . x misses F . y );

definition
let Omega be set ;
let Sigma be SigmaField of Omega;
let ASeq be SetSequence of Sigma;
:: original:disjoint_valued
redefine attrASeq is disjoint_valued  means :: PROB_2:def 3
 for m, n being Element of NAT st m <> n holds
ASeq . m misses ASeq . n;
compatibility
 ( ASeq is disjoint_valued iff for m, n being Element of NAT st m <> n holds
ASeq . m misses ASeq . n )
proofend;
end;

:: deftheorem  defines disjoint_valued PROB_2:def_3_:_
 for Omega being 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 &amp; lim (P * ASeq) = P . (Union ASeq) )
proofend;

theorem Th9: :: PROB_2:9
for Omega being non empty set
for Sigma being SigmaField of Omega
for P, P1 being Probability of Sigma st ( for A being Event of Sigma holds P . A = P1 . A ) holds
P = P1
proofend;

theorem :: PROB_2:10
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Function of Sigma,REAL holds
( P is Probability of Sigma iff ( ( for A being Event of Sigma holds 0 <= P . A ) &amp; P . Omega = 1 &amp; ( for A, B being Event of Sigma st A misses B holds
P . (A \/ B) = (P . A) + (P . B) ) &amp; ( for ASeq being SetSequence of Sigma st ASeq is non-descending holds
( P * ASeq is convergent &amp; lim (P * ASeq) = P . (Union ASeq) ) ) ) )
proofend;

theorem :: PROB_2:11
for Omega being non empty set
for Sigma being SigmaField of Omega
for A, B, C being Event of Sigma
for P being Probability of Sigma holds P . ((A \/ B) \/ C) = ((((P . A) + (P . B)) + (P . C)) - (((P . (A /\ B)) + (P . (B /\ C))) + (P . (A /\ C)))) + (P . ((A /\ B) /\ C))
proofend;

theorem :: PROB_2:12
for Omega being non empty set
for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma holds P . (A \ (A /\ B)) = (P . A) - (P . (A /\ B)) by PROB_1:33, XBOOLE_1:17;

theorem :: PROB_2:13
for Omega being non empty set
for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma holds
( P . (A /\ B) <= P . B &amp; P . (A /\ B) <= P . A ) by PROB_1:34, XBOOLE_1:17;

theorem Th14: :: PROB_2:14
for Omega being non empty set
for Sigma being SigmaField of Omega
for C, B, A being Event of Sigma
for P being Probability of Sigma st C = B ` holds
P . A = (P . (A /\ B)) + (P . (A /\ C))
proofend;

theorem Th15: :: PROB_2:15
for Omega being non empty set
for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma holds ((P . A) + (P . B)) - 1 <= P . (A /\ B)
proofend;

theorem Th16: :: PROB_2:16
for Omega being non empty set
for Sigma being SigmaField of Omega
for A being Event of Sigma
for P being Probability of Sigma holds P . A = 1 - (P . (([#] Sigma) \ A))
proofend;

theorem Th17: :: PROB_2:17
for Omega being non empty set
for Sigma being SigmaField of Omega
for A being Event of Sigma
for P being Probability of Sigma holds
( P . A < 1 iff 0 < P . (([#] Sigma) \ A) )
proofend;

theorem :: PROB_2:18
for Omega being non empty set
for Sigma being SigmaField of Omega
for A being Event of Sigma
for P being Probability of Sigma holds
( P . (([#] Sigma) \ A) < 1 iff 0 < P . A )
proofend;

::
:: INDEPENDENCE OF EVENTS
::
definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
let A, B be Event of Sigma;
predA,B are_independent_respect_to P means :Def4: :: PROB_2:def 4
P . (A /\ B) = (P . A) * (P . B);
let C be Event of Sigma;
predA,B,C are_independent_respect_to P means :Def5: :: PROB_2:def 5
( P . ((A /\ B) /\ C) = ((P . A) * (P . B)) * (P . C) &amp; P . (A /\ B) = (P . A) * (P . B) &amp; P . (A /\ C) = (P . A) * (P . C) &amp; P . (B /\ C) = (P . B) * (P . C) );
end;

:: deftheorem Def4 defines are_independent_respect_to PROB_2:def_4_:_
 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 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, 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) &amp; P . (A /\ B) = (P . A) * (P . B) &amp; P . (A /\ C) = (P . A) * (P . C) &amp; P . (B /\ C) = (P . B) * (P . C) ) );

theorem Th19: :: PROB_2:19
for Omega being non empty set
for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma st A,B are_independent_respect_to P holds
B,A are_independent_respect_to P
proofend;

theorem Th20: :: PROB_2:20
for Omega being non empty set
for Sigma being SigmaField of Omega
for A, B, C being Event of Sigma
for P being Probability of Sigma holds
( A,B,C are_independent_respect_to P iff ( P . ((A /\ B) /\ C) = ((P . A) * (P . B)) * (P . C) &amp; A,B are_independent_respect_to P &amp; B,C are_independent_respect_to P &amp; A,C are_independent_respect_to P ) )
proofend;

theorem :: PROB_2:21
for Omega being non empty set
for Sigma being SigmaField of Omega
for A, B, C being Event of Sigma
for P being Probability of Sigma st A,B,C are_independent_respect_to P holds
B,A,C are_independent_respect_to P
proofend;

theorem :: PROB_2:22
for Omega being non empty set
for Sigma being SigmaField of Omega
for A, B, C being Event of Sigma
for P being Probability of Sigma st A,B,C are_independent_respect_to P holds
A,C,B are_independent_respect_to P
proofend;

theorem :: PROB_2:23
for Omega being non empty set
for Sigma being SigmaField of Omega
for A being Event of Sigma
for P being Probability of Sigma
for E being Event of Sigma st E = {} holds
A,E are_independent_respect_to P
proofend;

theorem :: PROB_2:24
for Omega being non empty set
for Sigma being SigmaField of Omega
for A being Event of Sigma
for P being Probability of Sigma holds A, [#] Sigma are_independent_respect_to P
proofend;

theorem Th25: :: PROB_2:25
for Omega being non empty set
for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma st A,B are_independent_respect_to P holds
A,([#] Sigma) \ B are_independent_respect_to P
proofend;

theorem Th26: :: PROB_2:26
for Omega being non empty set
for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma st A,B are_independent_respect_to P holds
([#] Sigma) \ A,([#] Sigma) \ B are_independent_respect_to P
proofend;

theorem :: PROB_2:27
for Omega being non empty set
for Sigma being SigmaField of Omega
for A, B, C being Event of Sigma
for P being Probability of Sigma st A,B are_independent_respect_to P &amp; A,C are_independent_respect_to P &amp; B misses C holds
A,B \/ C are_independent_respect_to P
proofend;

theorem :: PROB_2:28
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 st A,B are_independent_respect_to P &amp; P . A < 1 &amp; P . B < 1 holds
P . (A \/ B) < 1
proofend;

::
:: CONDITIONAL PROBABILITY
::
definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
let B be Event of Sigma;
assume A1: 0 < P . B ;
funcP .|. B ->  Probability of Sigma means :Def6: :: PROB_2:def 6
 for A being Event of Sigma holds it . A = (P . (A /\ B)) / (P . B);
existence
 ex b1 being Probability of Sigma st
for A being Event of Sigma holds b1 . A = (P . (A /\ B)) / (P . B)
proofend;
uniqueness
 for b1, b2 being Probability of Sigma st ( for A being Event of Sigma holds b1 . A = (P . (A /\ B)) / (P . B) ) &amp; ( for A being Event of Sigma holds b2 . A = (P . (A /\ B)) / (P . B) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines .|. PROB_2:def_6_:_
 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 Th29: :: PROB_2:29
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for B, A being Event of Sigma st 0 < P . B holds
P . (A /\ B) = ((P .|. B) . A) * (P . B)
proofend;

theorem :: PROB_2:30
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 st 0 < P . (A /\ B) holds
P . ((A /\ B) /\ C) = ((P . A) * ((P .|. A) . B)) * ((P .|. (A /\ B)) . C)
proofend;

theorem Th31: :: PROB_2:31
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 st C = B ` &amp; 0 < P . B &amp; 0 < P . C holds
P . A = (((P .|. B) . A) * (P . B)) + (((P .|. C) . A) * (P . C))
proofend;

theorem Th32: :: PROB_2:32
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, A1, A2, A3 being Event of Sigma st A1 misses A2 &amp; A3 = (A1 \/ A2) ` &amp; 0 < P . A1 &amp; 0 < P . A2 &amp; 0 < P . A3 holds
P . A = ((((P .|. A1) . A) * (P . A1)) + (((P .|. A2) . A) * (P . A2))) + (((P .|. A3) . A) * (P . A3))
proofend;

theorem :: PROB_2:33
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 st 0 < P . B holds
( (P .|. B) . A = P . A iff A,B are_independent_respect_to P )
proofend;

theorem :: PROB_2:34
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 st 0 < P . B &amp; P . B < 1 &amp; (P .|. B) . A = (P .|. (([#] Sigma) \ B)) . A holds
A,B are_independent_respect_to P
proofend;

theorem :: PROB_2:35
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 st 0 < P . B holds
(((P . A) + (P . B)) - 1) / (P . B) <= (P .|. B) . A
proofend;

theorem Th36: :: PROB_2:36
for Omega being non empty set
for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma st 0 < P . A &amp; 0 < P . B holds
(P .|. B) . A = (((P .|. A) . B) * (P . A)) / (P . B)
proofend;

theorem :: PROB_2:37
for Omega being non empty set
for Sigma being SigmaField of Omega
for B, A1, A2 being Event of Sigma
for P being Probability of Sigma st 0 < P . B &amp; A2 = A1 ` &amp; 0 < P . A1 &amp; 0 < P . A2 holds
( (P .|. B) . A1 = (((P .|. A1) . B) * (P . A1)) / ((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) &amp; (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / ((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) )
proofend;

theorem :: PROB_2:38
for Omega being non empty set
for Sigma being SigmaField of Omega
for B, A1, A2, A3 being Event of Sigma
for P being Probability of Sigma st 0 < P . B &amp; 0 < P . A1 &amp; 0 < P . A2 &amp; 0 < P . A3 &amp; A1 misses A2 &amp; A3 = (A1 \/ A2) ` holds
( (P .|. B) . A1 = (((P .|. A1) . B) * (P . A1)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) &amp; (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) &amp; (P .|. B) . A3 = (((P .|. A3) . B) * (P . A3)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) )
proofend;

theorem :: PROB_2:39
for Omega being non empty set
for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma st 0 < P . B holds
1 - ((P . (([#] Sigma) \ A)) / (P . B)) <= (P .|. B) . A
proofend;