Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### Introduction to Probability

**by****Jan Popiolek**- Received June 13, 1990
- MML identifier: RPR_1

- [ Mizar article, MML identifier index ]

environ vocabulary FINSEQ_1, FINSET_1, BOOLE, RELAT_1, PROB_1, SUBSET_1, CARD_1, ARYTM_3, ARYTM_1, RPR_1, REALSET1; notation TARSKI, XBOOLE_0, SUBSET_1, XREAL_0, FUNCT_1, DOMAIN_1, REAL_1, FINSEQ_1, FINSET_1, CARD_1, REALSET1; constructors DOMAIN_1, REAL_1, NAT_1, REALSET1, XREAL_0, MEMBERED, XBOOLE_0; clusters FINSET_1, RELSET_1, XREAL_0, MEMBERED, ZFMISC_1, XBOOLE_0; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve E for non empty set; reserve a for Element of E; reserve A, B for Subset of E; reserve Y for set; reserve p for FinSequence; definition let E be non empty set; cluster non empty trivial Subset of E; end; definition let E; mode El_ev of E is non empty trivial Subset of E; end; theorem :: RPR_1:1 for e being non empty Subset of E holds e is El_ev of E iff for Y holds (Y c= e iff Y = {} or Y = e); definition let E; cluster -> finite El_ev of E; end; reserve e, e1, e2 for El_ev of E; canceled 3; theorem :: RPR_1:5 e = A \/ B & A <> B implies A = {} & B = e or A = e & B = {}; theorem :: RPR_1:6 e = A \/ B implies A = e & B = e or A = e & B = {} or A = {} & B = e; theorem :: RPR_1:7 {a} is El_ev of E; canceled 2; theorem :: RPR_1:10 e1 c= e2 implies e1 = e2; theorem :: RPR_1:11 ex a st a in E & e = {a}; theorem :: RPR_1:12 ex e st e is El_ev of E; canceled; theorem :: RPR_1:14 ex p st p is FinSequence of E & rng p = e & len p = 1; definition let E be set; mode Event of E is Subset of E; end; canceled 7; theorem :: RPR_1:22 for E being non empty set, e being El_ev of E, A being Event of E holds e misses A or e /\ A = e; canceled 2; theorem :: RPR_1:25 for E being non empty set, A being Event of E st A <> {} ex e being El_ev of E st e c= A; theorem :: RPR_1:26 for E being non empty set, e being El_ev of E, A being Event of E st e c= A \/ A` holds e c= A or e c= A`; theorem :: RPR_1:27 e1 = e2 or e1 misses e2; canceled 6; theorem :: RPR_1:34 A /\ B misses A /\ B`; definition let E be finite non empty set; let A be Event of E; canceled 3; func prob(A) -> Real equals :: RPR_1:def 4 card A / card E; end; canceled 3; theorem :: RPR_1:38 for E being finite non empty set, e being El_ev of E holds prob(e) = 1 / card E; theorem :: RPR_1:39 for E being finite non empty set holds prob([#] E) = 1; theorem :: RPR_1:40 for E being finite non empty set holds prob({} E) = 0; theorem :: RPR_1:41 for E being finite non empty set, A,B being Event of E st A misses B holds prob(A /\ B) = 0; theorem :: RPR_1:42 for E being finite non empty set, A being Event of E holds prob(A) <= 1; theorem :: RPR_1:43 for E being finite non empty set, A being Event of E holds 0 <= prob(A); theorem :: RPR_1:44 for E being finite non empty set, A,B being Event of E st A c= B holds prob(A) <= prob(B); canceled; theorem :: RPR_1:46 for E being finite non empty set, A,B being Event of E holds prob(A \/ B) = prob(A) + prob(B) - prob(A /\ B); theorem :: RPR_1:47 for E being finite non empty set, A,B being Event of E st A misses B holds prob(A \/ B) = prob(A) + prob(B); theorem :: RPR_1:48 for E being finite non empty set, A being Event of E holds prob(A) = 1 - prob(A`) & prob(A`) = 1 - prob(A); theorem :: RPR_1:49 for E being finite non empty set, A,B being Event of E holds prob(A \ B) = prob(A) - prob(A /\ B); theorem :: RPR_1:50 for E being finite non empty set, A,B being Event of E st B c= A holds prob(A \ B) = prob(A) - prob(B); theorem :: RPR_1:51 for E being finite non empty set, A,B being Event of E holds prob(A \/ B) <= prob(A) + prob(B); canceled; theorem :: RPR_1:53 for E being finite non empty set, A,B being Event of E holds prob(A) = prob(A /\ B) + prob(A /\ B`); theorem :: RPR_1:54 for E being finite non empty set, A,B being Event of E holds prob(A) = prob(A \/ B) - prob(B \ A); theorem :: RPR_1:55 for E being finite non empty set, A,B being Event of E holds prob(A) + prob(A` /\ B) = prob(B) + prob(B` /\ A); theorem :: RPR_1:56 for E being finite non empty set, A,B,C being Event of E holds prob(A \/ B \/ C) = ( prob(A) + prob(B) + prob(C) ) - ( prob(A /\ B) + prob(A /\ C) + prob(B /\ C) ) + prob(A /\ B /\ C); theorem :: RPR_1:57 for E being finite non empty set, A,B,C being Event of E st A misses B & A misses C & B misses C holds prob(A \/ B \/ C) = prob(A) + prob(B) + prob(C); theorem :: RPR_1:58 for E being finite non empty set, A,B being Event of E holds prob(A) - prob(B) <= prob(A \ B); definition let E be finite non empty set; let B,A be Event of E; func prob(A , B) -> Real equals :: RPR_1:def 5 prob(A /\ B) / prob(B); end; canceled; theorem :: RPR_1:60 for E being finite non empty set, A,B being Event of E st 0 < prob(B) holds prob(A /\ B) = prob(A , B) * prob(B); theorem :: RPR_1:61 for E being finite non empty set, A being Event of E holds prob(A , [#] E ) = prob(A); theorem :: RPR_1:62 for E being finite non empty set holds prob([#] E , [#] E) = 1; theorem :: RPR_1:63 for E being finite non empty set holds prob({} E , [#] E) = 0; theorem :: RPR_1:64 for E being finite non empty set, A,B being Event of E st 0 < prob(B) holds prob(A , B) <= 1; theorem :: RPR_1:65 for E being finite non empty set, A,B being Event of E st 0 < prob(B) holds 0 <= prob(A , B); theorem :: RPR_1:66 for E being finite non empty set, A,B being Event of E st 0 < prob(B) holds prob(A , B) = 1 - prob(B \ A) / prob(B); theorem :: RPR_1:67 for E being finite non empty set, A,B being Event of E st 0 < prob(B) & A c= B holds prob(A , B) = prob(A) / prob(B); theorem :: RPR_1:68 for E being finite non empty set, A,B being Event of E st A misses B holds prob(A , B) = 0; theorem :: RPR_1:69 for E being finite non empty set, A,B being Event of E st 0 < prob(A) & 0 < prob(B) holds prob(A) * prob(B , A) = prob(B) * prob(A , B); theorem :: RPR_1:70 for E being finite non empty set, A,B being Event of E st 0 < prob B holds prob(A , B) = 1 - prob(A` , B) & prob(A` , B) = 1 - prob(A , B); theorem :: RPR_1:71 for E being finite non empty set, A,B being Event of E st 0 < prob(B) & B c= A holds prob(A , B) = 1; theorem :: RPR_1:72 for E being finite non empty set, B being Event of E st 0 < prob(B) holds prob([#] E , B) = 1; theorem :: RPR_1:73 for E being finite non empty set, A being Event of E st 0 < prob(A) holds prob(A` , A) = 0; theorem :: RPR_1:74 for E being finite non empty set, A being Event of E st prob(A) < 1 holds prob(A , A`) = 0; theorem :: RPR_1:75 for E being finite non empty set, A,B being Event of E st 0 < prob(B) & A misses B holds prob(A` , B) = 1; theorem :: RPR_1:76 for E being finite non empty set, A,B being Event of E st 0 < prob(A) & prob(B) < 1 & A misses B holds prob(A , B`) = prob(A) / (1 - prob(B)); theorem :: RPR_1:77 for E being finite non empty set, A,B being Event of E st 0 < prob(A) & prob(B) < 1 & A misses B holds prob(A` , B`) = 1 - prob(A) / (1 - prob(B)); theorem :: RPR_1:78 for E being finite non empty set, A,B,C being Event of E st 0 < prob(B /\ C) & 0 < prob(C) holds prob(A /\ B /\ C) = prob(A , B /\ C) * prob(B , C) * prob(C); theorem :: RPR_1:79 for E being finite non empty set, A,B being Event of E st 0 < prob(B) & prob(B) < 1 holds prob(A) = prob(A , B) * prob(B) + prob(A , B`) * prob(B`); theorem :: RPR_1:80 for E being finite non empty set, A,B1,B2 being Event of E st 0 < prob(B1) & 0 < prob(B2) & B1 \/ B2 = E & B1 misses B2 holds prob(A) = prob(A , B1) * prob(B1) + prob(A , B2) * prob(B2); theorem :: RPR_1:81 for E being finite non empty set, A,B1,B2,B3 being Event of E st 0 < prob(B1) & 0 < prob(B2) & 0 < prob(B3) & B1 \/ B2 \/ B3 = E & B1 misses B2 & B1 misses B3 & B2 misses B3 holds prob(A) = ( prob(A , B1) * prob(B1) + prob(A , B2) * prob(B2) ) + prob(A , B3) * prob(B3); theorem :: RPR_1:82 for E being finite non empty set, A,B1,B2 being Event of E st 0 < prob(B1) & 0 < prob(B2) & B1 \/ B2 = E & B1 misses B2 holds prob(B1 , A) = ( prob(A , B1) * prob(B1) ) / ( prob(A , B1) * prob(B1) + prob(A , B2) * prob(B2) ); theorem :: RPR_1:83 for E being finite non empty set, A,B1,B2,B3 being Event of E st 0 < prob(B1) & 0 < prob(B2) & 0 < prob(B3) & B1 \/ B2 \/ B3 = E & B1 misses B2 & B1 misses B3 & B2 misses B3 holds prob(B1 , A) = ( prob(A , B1) * prob(B1) ) / ( ( prob(A , B1) * prob(B1) + prob(A , B2) * prob(B2) ) + prob(A , B3) * prob(B3) ); definition let E be finite non empty set; let A, B be Event of E; pred A, B are_independent means :: RPR_1:def 6 prob(A /\ B) = prob(A) * prob(B); symmetry; end; canceled 2; theorem :: RPR_1:86 for E being finite non empty set, A,B being Event of E st 0 < prob(B) & A, B are_independent holds prob(A , B) = prob(A); theorem :: RPR_1:87 for E being finite non empty set, A,B being Event of E st prob(B) = 0 holds A , B are_independent; theorem :: RPR_1:88 for E being finite non empty set, A,B being Event of E st A , B are_independent holds A` , B are_independent; theorem :: RPR_1:89 for E being finite non empty set, A,B being Event of E st A misses B & A, B are_independent holds prob(A) = 0 or prob(B) = 0;

Back to top