:: Probability. Independence of Events and Conditional Probability
:: by Andrzej N\c{e}dzusiak
::
:: Received June 1, 1990
:: Copyright (c) 1990-2026 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;
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<r2 ex n st for m st n<=m
holds |.seq.m-r1.|<r2 by A1,SEQ_2:def 6;
A4: now
let r2 be Real;
assume 0 < r2;
then consider n such that
A5: for m st n <= m holds |.seq.m - r1.| < r2 by A3;
take n;
now
let m such that
A6: n <= m;
|.seq.m - r1.| = |.-(seq.m - r1).| by COMPLEX1:52
.= |.r1 - r + (r - seq.m).|
.= |.seq1.m + - (-(r1 - r)).| by A2
.= |.seq1.m - (r - r1).|;
hence |.seq1.m - (r - r1).| < r2 by A5,A6;
end;
hence for m st n <= m holds |.seq1.m - (r - r1).| < r2;
end;
hence
A7: seq1 is convergent by SEQ_2:def 6;
lim seq = r1 by A1,A3,SEQ_2:def 7;
hence thesis by A4,A7,SEQ_2:def 7;
end;
definition
let Omega,Sigma,ASeq,n;
redefine func ASeq.n -> Event of Sigma; :: redefines . (FUNCT_1, definition)
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 :: redefines disjoint_valued (PROB_2, definition)
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;
::$N Bayes' theorem
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 Three Events
for B,A1,A2,A3,P 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
let B,A1,A2,A3,P;
assume that
A1: 0<P.B and
A2: 0<P.A1 and
A3: 0<P.A2 and
A4: 0<P.A3 and
A5: A1 misses A2 & A3=(A1 \/ A2)`;
thus (P.|.A1.B * P.A1)/((P.|.A1.B * P.A1 + P.|.A2.B * P.A2) + P.|. A3.B * P.
A3) = (P.|.A1.B * P.A1)/P.B by A2,A3,A4,A5,Th32
.= P.|.B.A1 by A1,A2,Th36;
thus (P.|.A2.B * P.A2)/((P.|.A1.B * P.A1 + P.|.A2.B * P.A2) + P.|. A3.B * P.
A3) = (P.|.A2.B * P.A2)/P.B by A2,A3,A4,A5,Th32
.= P.|.B.A2 by A1,A3,Th36;
thus (P.|.A3.B * P.A3)/((P.|.A1.B * P.A1 + P.|.A2.B * P.A2) + P.|. A3.B * P.
A3) = (P.|.A3.B * P.A3)/P.B by A2,A3,A4,A5,Th32
.= P.|.B.A3 by A1,A4,Th36;
end;
theorem
for A,B,P st 0 < P.B holds 1 - P.([#] Sigma \ A)/P.B <= P.|.B.A
proof
let A,B,P;
assume
A1: 0 < P.B;
P.B + P.A - 1 <= P.(A /\ B) by Th15;
then P.B + -(1 - P.A) <= P.(A /\ B);
then P.B + -P.([#] Sigma \ A) <= P.(A /\ B) by PROB_1:32;
then (P.B + -P.([#] Sigma \ A))/P.B <= P.(A /\ B)/P.B by A1,XREAL_1:72;
then (P.B - P.([#] Sigma \ A))/P.B <= P.|.B.A by A1,Def6;
then P.B/P.B - P.([#] Sigma \ A)/P.B <= P.|.B.A by XCMPLX_1:120;
hence thesis by A1,XCMPLX_1:60;
end;