:: Probability. Independence of Events and Conditional Probability
:: by Andrzej N\c{e}dzusiak
::
:: Received June 1, 1990
:: Copyright (c) 1990-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, SUBSET_1, REAL_1, SEQ_1, PROB_1, RPR_1,
CARD_1, ARYTM_3, RELAT_1, SEQ_2, FUNCT_1, ARYTM_1, ORDINAL2, XXREAL_0,
COMPLEX1, EQREL_1, TARSKI, ZFMISC_1, NAT_1, CARD_3, VALUED_1, PROB_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, COMPLEX1, RELAT_1, REAL_1, FUNCT_1, FUNCT_2, VALUED_1, SEQ_1,
COMSEQ_2, SEQ_2, PROB_1, NAT_1, XXREAL_0;
constructors XXREAL_0, REAL_1, NAT_1, COMPLEX1, VALUED_1, SEQ_2, PROB_1,
XXREAL_1, RELSET_1, COMSEQ_2;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XREAL_0,
VALUED_0, PROB_1, NAT_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin
reserve Omega for set;
reserve m,n,k for Nat;
reserve x,y for object;
reserve r,r1,r2,r3 for Real;
reserve seq,seq1 for Real_Sequence;
reserve Sigma for SigmaField of Omega;
reserve ASeq,BSeq for SetSequence of Sigma;
reserve A, B, C, A1, A2, A3 for Event of Sigma;
theorem :: PROB_2:1
for r,r1,r2,r3 st r <> 0 & r1 <> 0 holds (r3/r1 = r2/r iff r3 * r = r2 * r1);
theorem :: PROB_2:2
(seq is convergent & for n holds seq1.n = r - seq.n) implies seq1
is convergent & lim seq1 = r - lim seq;
definition
let Omega,Sigma,ASeq,n;
redefine func ASeq.n -> Event of Sigma;
end;
definition
let Omega,Sigma,ASeq;
func @Intersection ASeq -> Event of Sigma equals
:: PROB_2:def 1
:: nie mozna zastapic przez redefinicje - przeplot
Intersection ASeq;
end;
theorem :: PROB_2:3
ex BSeq st for n holds BSeq.n = ASeq.n /\ B;
theorem :: PROB_2:4
(ASeq is non-ascending & for n holds BSeq.n = ASeq.n /\ B)
implies BSeq is non-ascending;
theorem :: PROB_2:5
(for n holds BSeq.n = ASeq.n /\ B) implies (Intersection ASeq)
/\ B = Intersection BSeq;
registration
let Omega,Sigma,ASeq;
cluster Complement ASeq -> Sigma-valued;
end;
theorem :: PROB_2:6
for X being set, S being SetSequence of X holds S is non-ascending iff
for n holds S.(n+1) c= S.n;
theorem :: PROB_2:7
for X being set, S being SetSequence of X holds S is non-descending
iff for n holds S.n c= S.(n+1);
theorem :: PROB_2:8
for ASeq being SetSequence of Omega holds (ASeq is non-ascending
iff Complement ASeq is non-descending);
definition
let F be Function;
attr F is disjoint_valued means
:: PROB_2:def 2
x <> y implies F.x misses F.y;
end;
definition
let Omega,Sigma,ASeq;
redefine attr ASeq is disjoint_valued means
:: PROB_2:def 3
for m,n st m <> n holds ASeq.m misses ASeq.n;
end;
::
:: THEOREMS CONCERNED PROBABILITY
::
reserve Omega for non empty set;
reserve Sigma for SigmaField of Omega;
reserve A, B, C, A1, A2, A3 for Event of Sigma;
reserve ASeq,BSeq for SetSequence of Sigma;
reserve P,P1,P2 for Probability of Sigma;
theorem :: PROB_2:9
(for A holds P.A = P1.A) implies P = P1;
theorem :: PROB_2:10
:: Equivalent Definition of Probability
for P being Function of Sigma,REAL holds P is Probability of Sigma iff
(for A holds 0 <= P.A) & P.Omega = 1 & (for A,B st A misses B holds P.(A \/ B)
= P.A + P.B) & for ASeq st ASeq is non-descending holds P * ASeq is convergent
& lim (P * ASeq) = P.Union ASeq;
theorem :: PROB_2:11
P.(A \/ B \/ C) = P.A + P.B + P.C - (P.(A /\ B) + P.(B /\ C) + P.(A /\
C)) + P.(A /\ B /\ C);
theorem :: PROB_2:12
P.(A \ (A /\ B)) = P.A - P.(A /\ B);
theorem :: PROB_2:13
P.(A /\ B) <= P.B & P.(A /\ B) <= P.A;
theorem :: PROB_2:14
C = B` implies P.A = P.(A /\ B) + P.(A /\ C);
theorem :: PROB_2:15
P.A + P.B - 1 <= P.(A /\ B);
theorem :: PROB_2:16
P.A = 1 - P.([#] Sigma \ A);
theorem :: PROB_2:17
P.A < 1 iff 0 < P.([#] Sigma \ A);
theorem :: PROB_2:18
P.([#] Sigma \ A) < 1 iff 0 < P.A;
::
:: INDEPENDENCE OF EVENTS
::
definition
let Omega, Sigma, P, A, B;
pred A,B are_independent_respect_to P means
:: PROB_2:def 4
P.(A /\ B) = P.A * P.B;
let C;
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;
theorem :: PROB_2:19
A,B are_independent_respect_to P implies B,A are_independent_respect_to P;
theorem :: PROB_2:20
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
A,B,C are_independent_respect_to P implies B,A,C are_independent_respect_to P
;
theorem :: PROB_2:22
A,B,C are_independent_respect_to P implies A,C,B are_independent_respect_to P
;
theorem :: PROB_2:23
for E being Event of Sigma st E = {} holds A, E are_independent_respect_to P;
theorem :: PROB_2:24
A, [#] Sigma are_independent_respect_to P;
theorem :: PROB_2:25
for A,B,P st A,B are_independent_respect_to P holds A,([#] Sigma
\ B) are_independent_respect_to P;
theorem :: PROB_2:26
A,B are_independent_respect_to P implies ([#] Sigma \ A),([#]
Sigma \ B) are_independent_respect_to P;
theorem :: PROB_2:27
for A,B,C,P 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;
theorem :: PROB_2:28
for P,A,B st A,B are_independent_respect_to P & P.A < 1 & P.B < 1
holds P.(A \/ B) < 1;
::
:: CONDITIONAL PROBABILITY
::
definition
let Omega,Sigma,P,B;
assume
0 < P.B;
func P.|.B -> Probability of Sigma means
:: PROB_2:def 6
for A holds it.A = P.(A /\ B )/P.B;
end;
theorem :: PROB_2:29
for P,B,A st 0 < P.B holds P.(A /\ B) = P.|.B.A * P.B;
theorem :: PROB_2:30
for P,A,B,C st 0 < P.(A /\ B) holds P.(A /\ B /\ C) = P.A * P.|.A.B *
P.|.(A /\ B).C;
theorem :: PROB_2:31
for P,A,B,C st C = B` & 0 < P.B & 0 < P.C holds P.A = P.|.B.A *
P.B + P.|.C.A * P.C;
theorem :: PROB_2:32
for P,A,A1,A2,A3 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);
theorem :: PROB_2:33
for P,A,B st 0 < P.B holds (P.|.B.A = P.A iff A,B
are_independent_respect_to P);
theorem :: PROB_2:34
for P,A,B st 0 < P.B & P.B < 1 & P.|.B.A = P.|.([#] Sigma \ B).A holds
A,B are_independent_respect_to P;
theorem :: PROB_2:35
for P,A,B st 0 < P.B holds (P.A + P.B - 1)/ P.B <= P.|.B.A;
theorem :: PROB_2:36
for A,B,P st 0 < P.A & 0 < P.B holds P.|.B.A = P.|.A.B * P.A / P .B;
theorem :: PROB_2:37
::Bayes' Theorem for Two Events
for B,A1,A2,P 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);
theorem :: PROB_2:38
::Bayes' Theorem for Two Events
for B,A1,A2,A3,P st 0