:: 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 :: (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, SETFAM_1; 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, SETFAM_1; 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; ::$N Bayes' theorem 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 Three Events for B,A1,A2,A3,P st 0