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


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

theorem Th2: :: PROB_2:2
for r being Real
for seq, seq1 being Real_Sequence st seq is convergent & ( for n being Nat holds seq1 . n = r - (seq . n) ) holds
( seq1 is convergent & lim seq1 = r - (lim seq) )
proof end;

definition
let Omega be set ;
let Sigma be SigmaField of Omega;
let ASeq be SetSequence of Sigma;
let n be Nat;
:: original: .
redefine func ASeq . 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
proof end;
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 Nat holds BSeq . n = (ASeq . n) /\ B
proof end;

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 & ( for n being Nat holds BSeq . n = (ASeq . n) /\ B ) holds
BSeq is non-ascending
proof end;

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

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
proof end;
end;

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

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

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 )
proof end;

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

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

:: deftheorem defines disjoint_valued PROB_2:def 2 :
for F being Function holds
( F is disjoint_valued iff for x, y being object 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 attr ASeq is disjoint_valued means :: PROB_2:def 3
 for m, n being Nat st m <> n holds
ASeq . m misses ASeq . n;
compatibility
( ASeq is disjoint_valued iff for m, n being Nat st m <> n holds
ASeq . m misses ASeq . n )
proof end;
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 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) )
proof end;

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
proof end;

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 ) & P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds
P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-descending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) ) ) )
proof end;

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))
proof end;

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 & 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 A, B, C being Event of Sigma
for P being Probability of Sigma st C = B ` holds
P . A = (P . (A /\ B)) + (P . (A /\ C))
proof end;

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)
proof end;

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))
proof end;

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) )
proof end;

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 )
proof end;

::
:: 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;
pred A,B are_independent_respect_to P means :: PROB_2:def 4
P . (A /\ B) = (P . A) * (P . B);
let C be Event of Sigma;
pred A,B,C are_independent_respect_to P means :: PROB_2:def 5
( 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) );
end;

:: deftheorem 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 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) & P . (A /\ B) = (P . A) * (P . B) & P . (A /\ C) = (P . A) * (P . C) & P . (B /\ C) = (P . B) * (P . C) ) );

theorem :: 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 ;

theorem :: 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) & A,B are_independent_respect_to P & B,C are_independent_respect_to P & A,C are_independent_respect_to P ) ) ;

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 ;

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 by XBOOLE_1:16;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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 & A,C are_independent_respect_to P & B misses C holds
A,B \/ C are_independent_respect_to P
proof end;

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 & P . A < 1 & P . B < 1 holds
P . (A \/ B) < 1
proof end;

::
:: 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 ;
func P .|. 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)
proof end;
uniqueness
for b1, b2 being Probability of Sigma st ( for A being Event of Sigma holds b1 . A = (P . (A /\ B)) / (P . B) ) & ( for A being Event of Sigma holds b2 . A = (P . (A /\ B)) / (P . B) ) holds
b1 = b2
proof end;
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)
proof end;

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)
proof end;

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 ` & 0 < P . B & 0 < P . C holds
P . A = (((P .|. B) . A) * (P . B)) + (((P .|. C) . A) * (P . C))
proof end;

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 & A3 = (A1 \/ A2) ` & 0 < P . A1 & 0 < P . A2 & 0 < P . A3 holds
P . A = ((((P .|. A1) . A) * (P . A1)) + (((P .|. A2) . A) * (P . A2))) + (((P .|. A3) . A) * (P . A3))
proof end;

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 )
proof end;

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 & P . B < 1 & (P .|. B) . A = (P .|. (([#] Sigma) \ B)) . A holds
A,B are_independent_respect_to P
proof end;

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
proof end;

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 & 0 < P . B holds
(P .|. B) . A = (((P .|. A) . B) * (P . A)) / (P . B)
proof end;

:: WP: Bayes' theorem
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 & A2 = A1 ` & 0 < P . A1 & 0 < P . A2 holds
( (P .|. B) . A1 = (((P .|. A1) . B) * (P . A1)) / ((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) & (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / ((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) )
proof end;

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 & 0 < P . A1 & 0 < P . A2 & 0 < P . A3 & A1 misses A2 & 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))) & (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A3 = (((P .|. A3) . B) * (P . A3)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) )
proof end;

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
proof end;