:: 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 b₁ being Probability of Sigma st
for A being Event of Sigma holds b₁ . A = (P . (A /\ B)) / (P . B)

proof end;

uniqueness
for b₁, b₂ being Probability of Sigma st ( for A being Event of Sigma holds b₁ . A = (P . (A /\ B)) / (P . B) ) & ( for A being Event of Sigma holds b₂ . A = (P . (A /\ B)) / (P . B) ) holds
b₁ = b₂

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 b₅ being Probability of Sigma holds
( b₅ = P .|. B iff for A being Event of Sigma holds b₅ . 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;

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