:: 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; definitions PROB_1; equalities PROB_1, SUBSET_1; expansions PROB_1; theorems FUNCT_1, FUNCT_2, SEQ_2, SUBSET_1, PROB_1, NAT_1, TARSKI, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, COMPLEX1, XREAL_1, ORDINAL1, VALUED_1, VALUED_0, RELAT_1; schemes FUNCT_1, FUNCT_2, NAT_1; 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 Th1: for r,r1,r2,r3 st r <> 0 & r1 <> 0 holds (r3/r1 = r2/r iff r3 * r = r2 * r1) proof let r,r1,r2,r3; assume that A1: r <> 0 and A2: r1 <> 0; thus r3/r1 = r2/r implies r3 * r = r2 * r1 proof assume A3: r3/r1 = r2/r; r3 * r = r3/r1 * r1 * r by A2,XCMPLX_1:87 .= r2/r * r * r1 by A3 .= r2 * r1 by A1,XCMPLX_1:87; hence thesis; end; assume A4: r3 * r = r2 * r1; r3/r1 = (r3 * 1)/r1 .= (r3 * (r * r"))/r1 by A1,XCMPLX_0:def 7 .= (r2 * r1 * r")/r1 by A4,XCMPLX_1:4 .= (r2 * r" * r1)/r1 .= (r2/r * r1)/r1 by XCMPLX_0:def 9 .= (r2/r * r1) * r1" by XCMPLX_0:def 9 .= r2/r * (r1 * r1") .= r2/r * 1 by A2,XCMPLX_0:def 7 .= r2/r; hence thesis; end; theorem Th2: (seq is convergent & for n holds seq1.n = r - seq.n) implies seq1 is convergent & lim seq1 = r - lim seq proof assume that A1: seq is convergent and A2: for n holds seq1.n = r - seq.n; consider r1 be Real such that A3: for r2 be Real st 0 Event of Sigma; coherence by PROB_1:25; end; definition let Omega,Sigma,ASeq; func @Intersection ASeq -> Event of Sigma equals :: nie mozna zastapic przez redefinicje - przeplot Intersection ASeq; coherence proof rng ASeq c= Sigma by RELAT_1:def 19; hence thesis by PROB_1:def 6; end; end; theorem Th3: ex BSeq st for n holds BSeq.n = ASeq.n /\ B proof deffunc F(Element of NAT) = ASeq.\$1 /\ B; consider f being Function such that A1: dom f = NAT & for n being Element of NAT holds f.n = F(n) from FUNCT_1:sch 4; now let m; reconsider mm=m as Element of NAT by ORDINAL1:def 12; ASeq.m /\ B in bool Omega; then f.mm in bool Omega by A1; hence f.m in bool Omega; end; then for x being object st x in NAT holds f.x in bool Omega; then reconsider f as SetSequence of Omega by A1,FUNCT_2:3; now let m be Nat; reconsider m1 = m as Element of NAT by ORDINAL1:def 12; ASeq.m1 /\ B in Sigma; hence f.m in Sigma by A1; end; then rng f c= Sigma by NAT_1:52; then reconsider f as SetSequence of Sigma by RELAT_1:def 19; take f; let n; reconsider n as Element of NAT by ORDINAL1:def 12; f.n = F(n) by A1; hence thesis; end; theorem Th4: (ASeq is non-ascending & for n holds BSeq.n = ASeq.n /\ B) implies BSeq is non-ascending proof assume that A1: ASeq is non-ascending and A2: for n holds BSeq.n = ASeq.n /\ B; thus BSeq qua Function is non-ascending proof let m,n; assume m<=n; then ASeq.n c= ASeq.m by A1; then ASeq.n /\ B c= ASeq.m /\ B by XBOOLE_1:26; then BSeq.n c= ASeq.m /\ B by A2; hence BSeq.n c= BSeq.m by A2; end; end; theorem Th5: (for n holds BSeq.n = ASeq.n /\ B) implies (Intersection ASeq) /\ B = Intersection BSeq proof assume A1: for n holds BSeq.n = ASeq.n /\ B; A2: now let x be object; assume A3: x in (Intersection BSeq); A4: for n holds x in ASeq.n /\ B proof let n; x in BSeq.n by A3,PROB_1:13; hence thesis by A1; end; A5: for n holds x in ASeq.n & x in B proof let n; x in ASeq.n /\ B by A4; hence thesis by XBOOLE_0:def 4; end; then x in (Intersection ASeq) by PROB_1:13; hence x in (Intersection ASeq) /\ B by A5,XBOOLE_0:def 4; end; now let x be object; assume A6: x in (Intersection ASeq) /\ B; then A7: x in (Intersection ASeq) by XBOOLE_0:def 4; A8: for n holds x in ASeq.n /\ B proof let n; x in ASeq.n & x in B by A6,A7,PROB_1:13,XBOOLE_0:def 4; hence thesis by XBOOLE_0:def 4; end; for n holds x in BSeq.n proof let n; x in ASeq.n /\ B by A8; hence thesis by A1; end; hence x in (Intersection BSeq) by PROB_1:13; end; hence thesis by A2,TARSKI:2; end; registration let Omega,Sigma,ASeq; cluster Complement ASeq -> Sigma-valued; coherence proof now let n be Nat; reconsider n1=n as Element of NAT by ORDINAL1:def 12; (Complement ASeq).n1 = (ASeq.n1)` by PROB_1:def 2; then (Complement ASeq).n1 is Event of Sigma by PROB_1:20; hence (Complement ASeq).n in Sigma; end; then rng Complement ASeq c= Sigma by NAT_1:52; hence thesis by RELAT_1:def 19; end; end; theorem for X being set, S being SetSequence of X holds S is non-ascending iff for n holds S.(n+1) c= S.n proof let X be set, S be SetSequence of X; thus S is non-ascending implies for n holds S.(n+1) c= S.n by NAT_1:11; assume A1: for n holds S.(n+1) c= S.n; now let n,m such that A2: n <= m; A3: now defpred P[Nat] means S.(n+\$1) c= S.n; A4: for k st P[k] holds P[k+1] proof let k such that A5: S.(n+k) c= S.n; S.(n+k+1) c= S.(n+k) by A1; hence thesis by A5,XBOOLE_1:1; end; A6: P[0]; thus for k holds P[k] from NAT_1:sch 2(A6,A4); end; consider k being Nat such that A7: m = n + k by A2,NAT_1:10; thus S.m c= S.n by A3,A7; end; hence thesis; end; theorem for X being set, S being SetSequence of X holds S is non-descending iff for n holds S.n c= S.(n+1) proof let X be set, S be SetSequence of X; thus S is non-descending implies for n holds S.n c= S.(n+1) by NAT_1:11; assume A1: for n holds S.n c= S.(n+1); now let n,m such that A2: n <= m; A3: now defpred P[Nat] means S.n c= S.(n+\$1); A4: for k st P[k] holds P[k+1] proof let k such that A5: S.n c= S.(n+k); S.(n+k) c= S.(n+k+1) by A1; hence thesis by A5,XBOOLE_1:1; end; A6: P[0]; thus for k holds P[k] from NAT_1:sch 2(A6,A4); end; consider k being Nat such that A7: m = n + k by A2,NAT_1:10; thus S.n c= S.m by A3,A7; end; hence thesis; end; theorem Th8: for ASeq being SetSequence of Omega holds (ASeq is non-ascending iff Complement ASeq is non-descending) proof let ASeq be SetSequence of Omega; thus ASeq is non-ascending implies Complement ASeq is non-descending proof assume A1: ASeq is non-ascending; now let n,m; assume n <= m; then ASeq.m c= ASeq.n by A1; then (ASeq.n)` c= (ASeq.m)` by SUBSET_1:12; then (Complement ASeq).n c= (ASeq.m)` by PROB_1:def 2; hence (Complement ASeq).n c= (Complement ASeq).m by PROB_1:def 2; end; hence thesis; end; assume A2: Complement ASeq is non-descending; now let n,m; assume n <= m; then (Complement ASeq).n c= (Complement ASeq).m by A2; then (ASeq.n)` c= (Complement ASeq).m by PROB_1:def 2; then (ASeq.n)` c= (ASeq.m)` by PROB_1:def 2; hence ASeq.m c= ASeq.n by SUBSET_1:12; end; hence thesis; end; Lm1: for ASeq being SetSequence of Omega holds (ASeq is non-descending iff Complement ASeq is non-ascending) proof let ASeq be SetSequence of Omega; thus ASeq is non-descending implies Complement ASeq is non-ascending proof assume A1: ASeq is non-descending; now let n,m; assume n <= m; then ASeq.n c= ASeq.m by A1; then (ASeq.m)` c= (ASeq.n)` by SUBSET_1:12; then (Complement ASeq).m c= (ASeq.n)` by PROB_1:def 2; hence (Complement ASeq).m c= (Complement ASeq).n by PROB_1:def 2; end; hence thesis; end; assume A2: Complement ASeq is non-ascending; now let n,m; assume n <= m; then (Complement ASeq).m c= (Complement ASeq).n by A2; then (ASeq.m)` c= (Complement ASeq).n by PROB_1:def 2; then (ASeq.m)` c= (ASeq.n)` by PROB_1:def 2; hence ASeq.n c= ASeq.m by SUBSET_1:12; end; hence thesis; end; definition let F be Function; attr F is disjoint_valued means x <> y implies F.x misses F.y; end; definition let Omega,Sigma,ASeq; redefine attr ASeq is disjoint_valued means for m,n st m <> n holds ASeq.m misses ASeq.n; compatibility proof thus ASeq is disjoint_valued implies for m,n st m <> n holds ASeq.m misses ASeq.n; A1: dom ASeq = NAT by FUNCT_2:def 1; assume A2: for m,n st m <> n holds ASeq.m misses ASeq.n; let x,y; assume A3: x <> y; per cases; suppose x in dom ASeq & y in dom ASeq; hence thesis by A1,A2,A3; end; suppose not (x in dom ASeq & y in dom ASeq); then ASeq.x = {} or ASeq.y = {} by FUNCT_1:def 2; hence thesis by XBOOLE_1:65; end; end; 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; Lm2: for P,ASeq st ASeq is non-descending holds P * ASeq is convergent & lim ( P * ASeq) = P.Union ASeq proof let P,ASeq such that A1: ASeq is non-descending; set BSeq = Complement ASeq; A2: BSeq is non-ascending by A1,Lm1; then A3: P * BSeq is convergent by PROB_1:def 8; A4: now let n; reconsider nn=n as Element of NAT by ORDINAL1:def 12; (P * BSeq).n = P.(BSeq.nn) by FUNCT_2:15 .= P.((ASeq.n)`) by PROB_1:def 2 .= P.([#] Sigma \ ASeq.n) .= 1 - P.(ASeq.n) by PROB_1:32 .= 1 - (P * ASeq).nn by FUNCT_2:15 .= 1 + - (P * ASeq).n; hence (P * ASeq).n = 1 - (P * BSeq).n; end; hence P * ASeq is convergent by A3,Th2; reconsider V = Union ASeq as Event of Sigma by PROB_1:26; Intersection BSeq = [#] Sigma \ Union ASeq; then A5: P.Intersection BSeq = 1 - P.V by PROB_1:32; thus lim (P * ASeq) = 1 - lim (P * BSeq) by A3,A4,Th2 .= 1 - (1 - P.V) by A2,A5,PROB_1:def 8 .= P.(Union ASeq); end; theorem Th9: (for A holds P.A = P1.A) implies P = P1 proof assume for A holds P.A = P1.A; then for x being object st x in Sigma holds P.x = P1.x; hence thesis by FUNCT_2:12; end; theorem :: 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 proof let P be Function of Sigma,REAL; thus P is Probability of Sigma implies (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 by Lm2,PROB_1:def 8; assume that A1: for A holds 0 <= P.A and A2: P.Omega = 1 and A3: for A,B st A misses B holds P.(A \/ B) = P.A + P.B and A4: for ASeq st ASeq is non-descending holds P * ASeq is convergent & lim (P * ASeq) = P.Union ASeq; for ASeq st ASeq is non-ascending holds P * ASeq is convergent & lim (P * ASeq) = P.Intersection ASeq proof let ASeq such that A5: ASeq is non-ascending; Intersection ASeq = @Intersection ASeq; then reconsider V = Intersection ASeq as Event of Sigma; set BSeq = Complement ASeq; A6: for A holds P.(A`) = 1 - P.A proof let A; reconsider B = A` as Event of Sigma by PROB_1:20; A7: A misses B by SUBSET_1:24; 1 = P.[#]Omega by A2 .= P.(A \/ B) by SUBSET_1:10 .= P.A + P.B by A3,A7; hence thesis; end; A8: now let n; reconsider nn=n as Element of NAT by ORDINAL1:def 12; (P * BSeq).n = P.(BSeq.nn) by FUNCT_2:15 .= P.((ASeq.n)`) by PROB_1:def 2 .= 1 - P.(ASeq.n) by A6 .= 1 - (P * ASeq).nn by FUNCT_2:15 .= 1 + - (P * ASeq).n; hence (P * ASeq).n = 1 - (P * BSeq).n; end; Union BSeq = (Intersection ASeq)`; then A9: P.Union BSeq = 1 - P.V by A6; A10: BSeq is non-descending by A5,Th8; then A11: P * BSeq is convergent by A4; hence P * ASeq is convergent by A8,Th2; thus lim (P * ASeq) = 1 - lim (P * BSeq) by A11,A8,Th2 .= 1 - (1 - P.V) by A4,A10,A9 .= P.(Intersection ASeq); end; hence thesis by A1,A2,A3,PROB_1:def 8; end; theorem P.(A \/ B \/ C) = P.A + P.B + P.C - (P.(A /\ B) + P.(B /\ C) + P.(A /\ C)) + P.(A /\ B /\ C) proof A1: P.((A \/ B) /\ C) = P.((A /\ C) \/ (B /\ C)) by XBOOLE_1:23 .= P.(A /\ C) + P.(B /\ C) - P.((A /\ C) /\ (B /\ C)) by PROB_1:38 .= P.(A /\ C) + P.(B /\ C) - P.(A /\ ((B /\ C) /\ C)) by XBOOLE_1:16 .= P.(A /\ C) + P.(B /\ C) - P.(A /\ (B /\ (C /\ C))) by XBOOLE_1:16 .= P.(B /\ C) + P.(A /\ C) - P.(A /\ B /\ C) by XBOOLE_1:16; P.(A \/ B \/ C) = P.(A \/ B) + P.C - P.((A \/ B) /\ C) by PROB_1:38 .= P.A + P.B - P.(A /\ B) + P.C - P.((A \/ B) /\ C) by PROB_1:38 .= P.A + P.B + P.C - (P.(A /\ B) + P.((A \/ B) /\ C)); hence thesis by A1; end; theorem P.(A \ (A /\ B)) = P.A - P.(A /\ B) by PROB_1:33,XBOOLE_1:17; theorem P.(A /\ B) <= P.B & P.(A /\ B) <= P.A by PROB_1:34,XBOOLE_1:17; theorem Th14: C = B` implies P.A = P.(A /\ B) + P.(A /\ C) proof assume A1: C = B`; then B misses C by SUBSET_1:24; then A /\ C misses B by XBOOLE_1:74; then A2: A /\ B misses A /\ C by XBOOLE_1:74; P.A = P.(A /\ [#]Omega) by XBOOLE_1:28 .= P.(A /\ (B \/ C)) by A1,SUBSET_1:10 .= P.(A /\ B \/ A /\ C) by XBOOLE_1:23 .= P.(A /\ B) + P.(A /\ C) by A2,PROB_1:def 8; hence thesis; end; theorem Th15: P.A + P.B - 1 <= P.(A /\ B) proof P.A + P.B - P.(A /\ B) = P.(A \/ B) by PROB_1:38; then P.A + P.B - P.(A /\ B) <= 1 by PROB_1:35; then P.A + P.B <= P.(A /\ B) + 1 by XREAL_1:20; hence thesis by XREAL_1:20; end; theorem Th16: P.A = 1 - P.([#] Sigma \ A) proof P.([#] Sigma \ A) + P.A = 1 by PROB_1:31; hence thesis; end; theorem Th17: P.A < 1 iff 0 < P.([#] Sigma \ A) proof thus P.A < 1 implies 0 < P.([#] Sigma \ A) proof assume P.A < 1; then 1 - P.([#] Sigma \ A) < 1 by Th16; then 1 + - P.([#] Sigma \ A) < 1; then - P.([#] Sigma \ A) < 1 - 1 by XREAL_1:20; hence thesis; end; assume 0 < P.([#] Sigma \ A); then 0 < 1 - P.A by PROB_1:32; then P.A + 0 < 1 by XREAL_1:20; hence thesis; end; theorem P.([#] Sigma \ A) < 1 iff 0 < P.A proof thus P.([#] Sigma \ A) < 1 implies 0 < P.A proof assume P.([#] Sigma \ A) < 1; then 1 - P.A < 1 by PROB_1:32; then 1 + - P.A < 1; then - P.A < 1 - 1 by XREAL_1:20; hence thesis; end; assume 0 < P.A; then 0 < 1 - P.([#] Sigma \ A) by Th16; then P.([#] Sigma \ A) + 0 < 1 by XREAL_1:20; hence thesis; end; :: :: INDEPENDENCE OF EVENTS :: definition let Omega, Sigma, P, A, B; pred A,B are_independent_respect_to P means P.(A /\ B) = P.A * P.B; let C; pred A,B,C are_independent_respect_to P means 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 A,B are_independent_respect_to P implies B,A are_independent_respect_to P; theorem 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 A,B,C are_independent_respect_to P implies B,A,C are_independent_respect_to P ; theorem A,B,C are_independent_respect_to P implies A,C,B are_independent_respect_to P by XBOOLE_1:16; theorem for E being Event of Sigma st E = {} holds A, E are_independent_respect_to P proof let E be Event of Sigma; A1: P.(A /\ ({} Sigma)) = P.A * 0 by VALUED_0:def 19 .= P.A * P.({} Sigma) by VALUED_0:def 19; assume E = {}; hence thesis by A1; end; theorem A, [#] Sigma are_independent_respect_to P proof P.(A /\ ([#] Sigma)) = P.A * 1 by XBOOLE_1:28 .= P.A * P.([#] Sigma) by PROB_1:30; hence thesis; end; theorem Th25: for A,B,P st A,B are_independent_respect_to P holds A,([#] Sigma \ B) are_independent_respect_to P proof let A,B,P; assume A,B are_independent_respect_to P; then A1: P.(A /\ B) = P.A * P.B; P.(A /\ ([#] Sigma \ B)) = P.(A /\ B`) .= P.(A \ B) by SUBSET_1:13 .= P.(A \ (A /\ B)) by XBOOLE_1:47 .= P.A * 1 - P.A * P.B by A1,PROB_1:33,XBOOLE_1:17 .= P.A * (1 - P.B) .= P.A * P.([#] Sigma \ B) by PROB_1:32; hence thesis; end; theorem Th26: A,B are_independent_respect_to P implies ([#] Sigma \ A),([#] Sigma \ B) are_independent_respect_to P proof assume A,B are_independent_respect_to P; then A,([#] Sigma \ B) are_independent_respect_to P by Th25; then ([#] Sigma \ B),A are_independent_respect_to P; then ([#] Sigma \ B),([#] Sigma \ A) are_independent_respect_to P by Th25; hence thesis; end; theorem 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 proof let A,B,C,P; assume that A1: A,B are_independent_respect_to P and A2: A,C are_independent_respect_to P and A3: B misses C; A4: (A /\ B) misses (A /\ C) by A3,XBOOLE_1:76; P.(A /\ (B \/ C)) = P.((A /\ B) \/ (A /\ C)) by XBOOLE_1:23 .= P.(A /\ B) + P.(A /\ C) by A4,PROB_1:def 8 .= P.A * P.B + P.(A /\ C) by A1 .= P.A * P.B + P.A * P.C by A2 .= P.A * (P.B + P.C) .= P.A * P.(B \/ C) by A3,PROB_1:def 8; hence thesis; end; theorem for P,A,B st A,B are_independent_respect_to P & P.A < 1 & P.B < 1 holds P.(A \/ B) < 1 proof A1: now let r,r1; assume 0 < r1; then - r1 < -0 by XREAL_1:24; then r + - r1 < r + 0 by XREAL_1:6; hence r - r1 < r; end; let P,A,B; assume that A2: A,B are_independent_respect_to P and A3: P.A < 1 & P.B < 1; A4: ([#] Sigma \ A),([#] Sigma \ B) are_independent_respect_to P by A2,Th26; A5: 0 < P.([#] Sigma \ A) & 0 < P.([#] Sigma \ B) by A3,Th17; P.(A \/ B) = 1 - P.([#] Sigma \ (A \/ B)) by Th16 .= 1 - P.(([#] Sigma \ A) /\ ([#] Sigma \ B)) by XBOOLE_1:53 .= 1 - P.([#] Sigma \ A) * P.([#] Sigma \ B) by A4; hence thesis by A5,A1,XREAL_1:129; end; :: :: CONDITIONAL PROBABILITY :: definition let Omega,Sigma,P,B; assume A1: 0 < P.B; func P.|.B -> Probability of Sigma means :Def6: for A holds it.A = P.(A /\ B )/P.B; existence proof defpred P[object,object] means ex A,r st (A = \$1 & r = \$2) & r = P.(A /\ B)/P.B; A2: for x being object st x in Sigma ex y being object st y in REAL & P[x,y] proof let x be object; assume x in Sigma; then reconsider x as Event of Sigma; consider y such that A3: y = P.(x /\ B)/P.B; take y; thus thesis by A3; end; consider f being Function of Sigma,REAL such that A4: for x being object st x in Sigma holds P[x,f.x] from FUNCT_2:sch 1(A2); A5: for A holds f.A = P.(A /\ B)/P.B proof let A; ex C,r1 st C = A & r1 = f.A & r1 = P.(C /\ B)/P.B by A4; hence thesis; end; then A6: f.Omega = P.(([#] Sigma) /\ B)/P.B .= P.B/P.B by XBOOLE_1:28 .= 1 by A1,XCMPLX_1:60; A7: for A,C st A misses C holds f.(A \/ C) = f.A + f.C proof let A,C; assume A misses C; then A8: A /\ B misses C /\ B by XBOOLE_1:76; thus f.(A \/ C) = P.((A \/ C) /\ B)/P.B by A5 .= P.((A /\ B) \/ (C /\ B))/P.B by XBOOLE_1:23 .= (P.(A /\ B) + P.(C /\ B))/P.B by A8,PROB_1:def 8 .= P.(A /\ B)/P.B + P.(C /\ B)/P.B by XCMPLX_1:62 .= P.(A /\ B)/P.B + f.C by A5 .= f.A + f.C by A5; end; A9: for A holds 0 <= f.A proof let A; 0 <= P.(A /\ B) by PROB_1:def 8; then 0 <= P.(A /\ B)/P.B by A1; hence thesis by A5; end; for ASeq st ASeq is non-ascending holds f*ASeq is convergent & lim (f *ASeq) = f.(Intersection ASeq) proof let ASeq such that A10: ASeq is non-ascending; consider BSeq such that A11: for n holds BSeq.n = ASeq.n /\ B by Th3; A12: dom(f*ASeq) = NAT by FUNCT_2:def 1; A13: now let n be object; assume A14: n in dom(f*ASeq); then reconsider n1 = n as Element of NAT by FUNCT_2:def 1; thus (f*ASeq).n = f.(ASeq.n) by A12,A14,FUNCT_2:15 .= P.(ASeq.n1 /\ B)/P.B by A5 .= P.(BSeq.n)/P.B by A11 .= (P*BSeq).n/P.B by A12,A14,FUNCT_2:15 .= (P.B)" * (P*BSeq).n by XCMPLX_0:def 9; end; A15: BSeq is non-ascending by A10,A11,Th4; then A16: P*BSeq is convergent by PROB_1:def 8; dom(P*BSeq) = NAT by FUNCT_2:def 1; then A17: f*ASeq = (P.B)" (#) (P*BSeq) by A12,A13,VALUED_1:def 5; hence f*ASeq is convergent by A16,SEQ_2:7; lim (P*BSeq) = P.(Intersection BSeq) by A15,PROB_1:def 8; hence lim (f*ASeq) = (P.B)" * P.(@Intersection BSeq) by A17,A16,SEQ_2:8 .= (P.(@Intersection BSeq))/P.B by XCMPLX_0:def 9 .= (P.((@Intersection ASeq) /\ B))/P.B by A11,Th5 .= f.(Intersection ASeq) by A5; end; then reconsider f as Probability of Sigma by A9,A6,A7,PROB_1:def 8; take f; thus thesis by A5; end; uniqueness proof let P1,P2; assume that A18: for A holds P1.A = P.(A /\ B)/P.B and A19: for A holds P2.A = P.(A /\ B)/P.B; now let A; thus P1.A = P.(A /\ B)/P.B by A18 .= P2.A by A19; end; hence thesis by Th9; end; end; theorem Th29: for P,B,A st 0 < P.B holds P.(A /\ B) = P.|.B.A * P.B proof let P,B,A; assume A1: 0 < P.B; then P.|.B.A * P.B = (P.(A /\ B)/P.B) * P.B by Def6 .= P.(A /\ B) * (P.B)" * P.B by XCMPLX_0:def 9 .= P.(A /\ B) * ((P.B)" * P.B) .= P.(A /\ B) * 1 by A1,XCMPLX_0:def 7 .= P.(A /\ B); hence thesis; end; theorem for P,A,B,C st 0 < P.(A /\ B) holds P.(A /\ B /\ C) = P.A * P.|.A.B * P.|.(A /\ B).C proof let P,A,B,C; assume A1: 0 < P.(A /\ B); then A2: 0 < P.A by PROB_1:34,XBOOLE_1:17; P.(A /\ B /\ C) = P.(B /\ A) * P.|.(A /\ B).C by A1,Th29 .= P.A * P.|.A.B * P.|.(A /\ B).C by A2,Th29; hence thesis; end; theorem Th31: 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 proof let P,A,B,C; assume that A1: C = B` and A2: 0 < P.B and A3: 0 < P.C; P.A = P.(A /\ B) + P.(A /\ C) by A1,Th14 .= P.|.B.A * P.B + P.(A /\ C) by A2,Th29 .= P.|.B.A * P.B + P.|.C.A * P.C by A3,Th29; hence thesis; end; theorem Th32: 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) proof let P,A,A1,A2,A3; assume that A1: A1 misses A2 and A2: A3 = (A1 \/ A2)` and A3: 0 < P.A1 and A4: 0 < P.A2 and A5: 0 < P.A3; A6: A /\ A1 misses A /\ A2 by A1,XBOOLE_1:76; (A1 \/ A2) misses A3 by A2,SUBSET_1:24; then A7: A /\ (A1 \/ A2) misses A /\ A3 by XBOOLE_1:76; A8: A1 \/ A2 \/ A3 = [#]Omega by A2,SUBSET_1:10 .= Omega; (P.|.A1.A * P.A1) + (P.|.A2.A * P.A2) + (P.|.A3.A * P.A3) = P.(A /\ A1) + (P.|.A2.A * P.A2) + (P.|.A3.A * P.A3) by A3,Th29 .= P.(A /\ A1) + P.(A /\ A2) + (P.|.A3.A * P.A3) by A4,Th29 .= P.(A /\ A1) + P.(A /\ A2) + P.(A /\ A3) by A5,Th29 .= P.((A /\ A1) \/ (A /\ A2)) + P.(A /\ A3) by A6,PROB_1:def 8 .= P.(A /\ (A1 \/ A2)) + P.(A /\ A3) by XBOOLE_1:23 .= P.((A /\ (A1 \/ A2)) \/ (A /\ A3)) by A7,PROB_1:def 8 .= P.(A /\ Omega) by A8,XBOOLE_1:23 .= P.A by XBOOLE_1:28; hence thesis; end; theorem for P,A,B st 0 < P.B holds (P.|.B.A = P.A iff A,B are_independent_respect_to P) proof let P,A,B; assume A1: 0 < P.B; thus P.|.B.A = P.A implies A,B are_independent_respect_to P proof assume P.|.B.A = P.A; then P.(A /\ B)/P.B * P.B = P.A * P.B by A1,Def6; then P.(A /\ B) = P.A * P.B by A1,XCMPLX_1:87; hence thesis; end; assume A,B are_independent_respect_to P; then P.(A /\ B) * (P.B)" = P.A * P.B * (P.B)"; then P.(A /\ B) * (P.B)" = P.A * (P.B * (P.B)"); then P.(A /\ B) * (P.B)" = P.A * 1 by A1,XCMPLX_0:def 7; then P.(A /\ B)/P.B = P.A by XCMPLX_0:def 9; hence thesis by A1,Def6; end; theorem 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 proof let P,A,B; assume that A1: 0 < P.B and A2: P.B < 1 and A3: P.|.B.A = P.|.([#] Sigma \B).A; 0 < P.([#] Sigma \ B) & P.(A /\ B)/P.B = P.|.([#] Sigma \B).A by A1,A2,A3 ,Def6,Th17; then A4: P.(A /\ B)/P.B = P.(A /\ ([#] Sigma \B))/P.([#] Sigma \ B) by Def6; A5: B`= ([#] Sigma \ B); P.([#] Sigma \ B) <> 0 by A2,Th17; then P.(A /\ B) * P.([#] Sigma \ B) = P.(A /\ ([#] Sigma \B)) * P.B by A1,A4,Th1; then P.(A /\ B) * (1 - P.B) = P.(A /\ ([#] Sigma \B)) * P.B by PROB_1:32; then P.(A /\ B) = (P.(A /\ ([#] Sigma \B)) + P.(A /\ B)) * P.B .= P.A * P.B by A5,Th14; hence thesis; end; theorem for P,A,B st 0 < P.B holds (P.A + P.B - 1)/ P.B <= P.|.B.A proof let P,A,B such that A1: 0 < P.B; (P.A + P.B - 1)/P.B <= P.(A /\ B)/P.B by A1,Th15,XREAL_1:72; hence thesis by A1,Def6; end; theorem Th36: for A,B,P st 0 < P.A & 0 < P.B holds P.|.B.A = P.|.A.B * P.A / P .B proof let A,B,P; assume that A1: 0 < P.A and A2: 0 < P.B; thus P.|.A.B * P.A / P.B = P.(A /\ B) / P.B by A1,Th29 .= P.|.B.A by A2,Def6; end; theorem ::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) proof let B,A1,A2,P; assume that A1: 0 < P.B and A2: A2 = A1` and A3: 0 < P.A1 and A4: 0 < P.A2; thus P.|.A1.B * P.A1 / (P.|.A1.B * P.A1 + P.|.A2.B * P.A2) = P.|.A1.B * P.A1 / P.B by A2,A3,A4,Th31 .= P.|.B.A1 by A1,A3,Th36; thus P.|.A2.B * P.A2 / (P.|.A1.B * P.A1 + P.|.A2.B * P.A2) = P.|.A2.B * P.A2 / P.B by A2,A3,A4,Th31 .= P.|.B.A2 by A1,A4,Th36; end; theorem ::Bayes' Theorem for Two Events for B,A1,A2,A3,P st 0