Copyright (c) 1990 Association of Mizar Users
environ
vocabulary SEQ_1, PROB_1, ARYTM_3, RELAT_1, SEQ_2, FUNCT_1, ARYTM_1, ORDINAL2,
ARYTM, ABSVALUE, BOOLE, SUBSET_1, PROB_2;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, RELAT_1, REAL_1, FUNCT_1, FUNCT_2, ABSVALUE, SEQ_1, SEQ_2,
PROB_1, NAT_1;
constructors REAL_1, ABSVALUE, SEQ_2, PROB_1, NAT_1, MEMBERED, XBOOLE_0;
clusters SUBSET_1, XREAL_0, RELSET_1, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0,
NUMBERS, ORDINAL2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions PROB_1;
theorems FUNCT_1, REAL_1, FUNCT_2, ABSVALUE, SEQ_1, SEQ_2, SUBSET_1, PROB_1,
SQUARE_1, NAT_1, TARSKI, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1;
schemes FUNCT_1, FUNCT_2, NAT_1;
begin
reserve Omega for non empty set;
reserve m,n,k for Nat;
reserve x,y,z for set;
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 P,P1,P2 for Probability of Sigma;
reserve A, B, C, A1, A2, A3 for Event of Sigma;
canceled 3;
theorem
Th4: 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:88
.= r2/r * r * r1 by A3,XCMPLX_1:4
.= r2 * r1 by A1,XCMPLX_1:88;
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 by XCMPLX_1:4
.= (r2/r * r1)/r1 by XCMPLX_0:def 9
.= (r2/r * r1) * r1" by XCMPLX_0:def 9
.= r2/r * (r1 * r1") by XCMPLX_1:4
.= r2/r * 1 by A2,XCMPLX_0:def 7
.= r2/r;
hence thesis;
end;
theorem
Th5: (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 number such that
A3: for r2 be real number st 0<r2
ex n st for m st n<=m holds abs(seq.m-r1)<r2 by A1,SEQ_2:def 6;
A4:now let r2 be real number; assume
0 < r2; then consider n such that
A5: for m st n <= m holds abs(seq.m - r1) < r2 by A3;
A6:now let m such that
A7: n <= m;
abs(seq.m - r1) = abs(-(seq.m - r1)) by ABSVALUE:17
.= abs(r1 + 0 - seq.m) by XCMPLX_1:143
.= abs(r1 + (-r + r) - seq.m) by XCMPLX_0:def 6
.= abs(r1 + -r + r - seq.m) by XCMPLX_1:1
.= abs(r1 - r + r - seq.m) by XCMPLX_0:def 8
.= abs(r1 - r + (r - seq.m)) by XCMPLX_1:29
.= abs(seq1.m + - (-(r1 - r))) by A2
.= abs(seq1.m - (-(r1 - r))) by XCMPLX_0:def 8
.= abs(seq1.m - (r - r1)) by XCMPLX_1:143;
hence abs(seq1.m - (r - r1)) < r2 by A5,A7;
end;
take n; thus
for m st n <= m holds abs(seq1.m - (r - r1)) < r2 by A6;
end;
hence A8: seq1 is convergent by SEQ_2:def 6;
lim seq = r1 by A1,A3,SEQ_2:def 7;
hence thesis by A4,A8,SEQ_2:def 7;
end;
::
:: THEOREMS CONCERNED EVENTS
::
theorem Th6:
A /\ Omega = A & A /\ ([#] Sigma) = A
proof
thus A /\ Omega = A by XBOOLE_1:28;
hence A /\ ([#] Sigma) = A by PROB_1:def 11;
end;
scheme SeqExProb{F(Nat) -> set}:
ex f being Function st dom f = NAT & for n holds f.n = F(n)
proof
defpred P[set,set] means ex n st $1 = n & $2 = F(n);
A1: for x,y,z st x in NAT & P[x,y] & P[x,z] holds y = z;
A2: for x st x in NAT ex y st P[x,y]
proof let x; assume x in NAT;
then reconsider x as Nat;
take F(x); thus thesis;
end;
consider f being Function such that
A3: dom f = NAT & for x st x in NAT holds P[x,f.x] from FuncEx(A1,A2);
take f;
now let n; ex m st n = m & f.n = F(m) by A3;
hence f.n = F(n);
end; hence thesis by A3;
end;
definition let Omega,Sigma,ASeq,n;
redefine func ASeq.n -> Event of Sigma;
coherence by PROB_1:57;
end;
definition let Omega,Sigma,ASeq;
func @Intersection ASeq -> Event of Sigma equals
:Def1: Intersection ASeq;
coherence
proof
for n holds ASeq.n in Sigma by PROB_1:def 9;
then Intersection ASeq in Sigma by PROB_1:def 8;
hence Intersection ASeq is Event of Sigma by PROB_1:def 10;
end;
end;
canceled 2;
theorem
Th9: ex BSeq st for n holds BSeq.n = ASeq.n /\ B
proof
deffunc F(Nat) = ASeq.$1 /\ B;
consider f being Function such that
A1: dom f = NAT & for n holds f.n = F(n) from SeqExProb;
now let m;
ASeq.m /\ B in bool Omega;
hence f.m in bool Omega by A1;
end;
then for x being set st x in NAT holds f.x in bool Omega;
then reconsider f as SetSequence of Omega by A1,FUNCT_2:5;
now let m; ASeq.m /\ B in Sigma by PROB_1:def 10;
hence f.m in Sigma by A1;
end;
then reconsider f as SetSequence of Sigma by PROB_1:def 9;
take f; thus thesis by A1;
end;
theorem
Th10: (ASeq is non-increasing &
for n holds BSeq.n = ASeq.n /\ B) implies BSeq is non-increasing
proof assume
A1: ASeq is non-increasing & for n holds BSeq.n = ASeq.n /\ B;
now let m,n; assume m<=n;
then ASeq.n c= ASeq.m by A1,PROB_1:def 6;
then ASeq.n /\ B c= ASeq.m /\ B by XBOOLE_1:26;
then BSeq.n c= ASeq.m /\ B by A1; hence
BSeq.n c= BSeq.m by A1;
end; hence thesis by PROB_1:def 6;
end;
theorem
Th11: for f being Function of Sigma,REAL holds
(f*ASeq).n = f.(ASeq.n)
proof let f be Function of Sigma,REAL;
n in NAT;
then n in dom ASeq by FUNCT_2:def 1;
hence (f*ASeq).n = f.(ASeq.n) by FUNCT_1:23;
end;
theorem
Th12: (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; assume x in (Intersection ASeq) /\ B;
then A3: x in (Intersection ASeq) & x in B by XBOOLE_0:def 3;
A4: for n holds x in ASeq.n /\ B
proof let n; x in ASeq.n & x in B by A3,PROB_1:29;
hence thesis by XBOOLE_0:def 3;
end;
for n holds x in BSeq.n
proof let n; x in ASeq.n /\ B by A4;
hence thesis by A1;
end;
hence x in (Intersection BSeq) by PROB_1:29;
end;
now let x;
assume A5: x in (Intersection BSeq);
A6: for n holds x in ASeq.n /\ B
proof let n; x in BSeq.n by A5,PROB_1:29;
hence thesis by A1;
end;
for n holds (x in ASeq.n & x in B)
proof let n; x in ASeq.n /\ B by A6;
hence thesis by XBOOLE_0:def 3;
end;
then x in (Intersection ASeq) & x in B by PROB_1:29;
hence x in (Intersection ASeq) /\ B by XBOOLE_0:def 3;
end;
hence thesis by A2,TARSKI:2;
end;
theorem
Th13: (for A holds P.A = P1.A) implies P = P1
proof assume
A1: for A holds P.A = P1.A;
for x st x in Sigma holds P.x = P1.x
proof let x; assume x in Sigma;
then reconsider x as Event of Sigma by PROB_1:48;
P.x = P1.x by A1;
hence thesis;
end;
hence thesis by FUNCT_2:18;
end;
theorem
for ASeq being SetSequence of Omega holds
ASeq is non-increasing iff for n holds ASeq.(n+1) c= ASeq.n
proof let ASeq be SetSequence of Omega;
thus ASeq is non-increasing implies for n holds ASeq.(n+1) c= ASeq.n
proof assume
A1: ASeq is non-increasing;
now let n;
n <= n+1 by NAT_1:29;
hence ASeq.(n+1) c= ASeq.n by A1,PROB_1:def 6;
end;
hence thesis;
end; assume
A2: for n holds ASeq.(n+1) c= ASeq.n;
now let n,m such that
A3: n <= m;
A4: now
defpred P[Nat] means ASeq.(n+$1) c= ASeq.n;
A5: P[0];
A6: for k st P[k] holds P[k+1]
proof let k such that
A7: ASeq.(n+k) c= ASeq.n;
ASeq.(n+k+1) c= ASeq.(n+k) by A2;
then ASeq.(n+(k+1)) c= ASeq.(n+k) by XCMPLX_1:1;
hence thesis by A7,XBOOLE_1:1;
end;
thus for k holds P[k] from Ind(A5,A6);
end;
ex k st m = n + k by A3,NAT_1:28;
hence ASeq.m c= ASeq.n by A4;
end;
hence thesis by PROB_1:def 6;
end;
theorem
for ASeq being SetSequence of Omega holds
ASeq is non-decreasing iff for n holds ASeq.n c= ASeq.(n+1)
proof let ASeq be SetSequence of Omega;
thus ASeq is non-decreasing implies for n holds ASeq.n c= ASeq.(n+1)
proof assume
A1: ASeq is non-decreasing;
now let n;
n <= n+1 by NAT_1:29;
hence ASeq.n c= ASeq.(n+1) by A1,PROB_1:def 7;
end;
hence thesis;
end; assume
A2: for n holds ASeq.n c= ASeq.(n+1);
now let n,m such that
A3: n <= m;
A4: now
defpred P[Nat] means ASeq.n c= ASeq.(n+$1);
A5: P[0];
A6: for k st P[k] holds P[k+1]
proof let k such that
A7: ASeq.n c= ASeq.(n+k);
ASeq.(n+k) c= ASeq.(n+k+1) by A2;
then ASeq.(n+k) c= ASeq.(n+(k+1)) by XCMPLX_1:1;
hence thesis by A7,XBOOLE_1:1;
end;
thus for k holds P[k] from Ind(A5,A6);
end;
ex k st m = n + k by A3,NAT_1:28;
hence ASeq.n c= ASeq.m by A4;
end;
hence thesis by PROB_1:def 7;
end;
theorem
for ASeq,BSeq being SetSequence of Omega
st (for n holds ASeq.n = BSeq.n) holds ASeq = BSeq
proof let ASeq,BSeq be SetSequence of Omega;
assume for n holds ASeq.n = BSeq.n;
then A1: for x holds
x in NAT implies ASeq.x = BSeq.x;
A2: dom ASeq = NAT by FUNCT_2:def 1;
dom BSeq = NAT by FUNCT_2:def 1;
hence thesis by A1,A2,FUNCT_1:9;
end;
theorem
Th17: for ASeq being SetSequence of Omega holds
(ASeq is non-increasing iff Complement ASeq is non-decreasing)
proof let ASeq be SetSequence of Omega;
thus ASeq is non-increasing implies Complement ASeq is non-decreasing
proof
assume A1: ASeq is non-increasing;
now let n,m; assume
n <= m;
then ASeq.m c= ASeq.n by A1,PROB_1:def 6;
then (ASeq.n)` c= (ASeq.m)` by SUBSET_1:31;
then (Complement ASeq).n c= (ASeq.m)` by PROB_1:def 4;
hence (Complement ASeq).n c= (Complement ASeq).m by PROB_1:def 4;
end;
hence thesis by PROB_1:def 7;
end; assume
A2: Complement ASeq is non-decreasing;
now let n,m; assume
n <= m;
then (Complement ASeq).n c= (Complement ASeq).m by A2,PROB_1:def 7;
then (ASeq.n)` c= (Complement ASeq).m by PROB_1:def 4;
then (ASeq.n)` c= (ASeq.m)` by PROB_1:def 4;
hence ASeq.m c= ASeq.n by SUBSET_1:31;
end;
hence thesis by PROB_1:def 6;
end;
Lm1: for ASeq being SetSequence of Omega holds
(ASeq is non-decreasing iff Complement ASeq is non-increasing)
proof let ASeq be SetSequence of Omega;
thus ASeq is non-decreasing implies Complement ASeq is non-increasing
proof
assume A1: ASeq is non-decreasing;
now let n,m; assume
n <= m;
then ASeq.n c= ASeq.m by A1,PROB_1:def 7;
then (ASeq.m)` c= (ASeq.n)` by SUBSET_1:31;
then (Complement ASeq).m c= (ASeq.n)` by PROB_1:def 4;
hence (Complement ASeq).m c= (Complement ASeq).n by PROB_1:def 4;
end;
hence thesis by PROB_1:def 6;
end; assume
A2: Complement ASeq is non-increasing;
now let n,m; assume
n <= m;
then (Complement ASeq).m c= (Complement ASeq).n by A2,PROB_1:def 6;
then (ASeq.m)` c= (Complement ASeq).n by PROB_1:def 4;
then (ASeq.m)` c= (ASeq.n)` by PROB_1:def 4;
hence ASeq.n c= ASeq.m by SUBSET_1:31;
end;
hence thesis by PROB_1:def 7;
end;
definition let Omega,Sigma,ASeq;
func @Complement ASeq -> SetSequence of Sigma equals
:Def2: Complement ASeq;
coherence
proof
now let n;
(Complement ASeq).n = (ASeq.n)` by PROB_1:def 4;
then (Complement ASeq).n is Event of Sigma by PROB_1:50;
hence (Complement ASeq).n in Sigma by PROB_1:def 10;
end; hence thesis by PROB_1:def 9;
end;
end;
definition let F be Function;
attr F is disjoint_valued means
:Def3: 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
A1: dom ASeq = NAT by FUNCT_2:def 1;
thus ASeq is disjoint_valued implies
for m,n st m <> n holds ASeq.m misses ASeq.n by Def3;
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 ASeq.x misses ASeq.y by A1,A2,A3;
suppose not (x in dom ASeq & y in dom ASeq);
then ASeq.x = {} or ASeq.y = {} by FUNCT_1:def 4;
hence ASeq.x misses ASeq.y by XBOOLE_1:65;
end;
end;
Lm2: for P,ASeq st ASeq is non-decreasing holds
(P * ASeq is convergent & lim (P * ASeq) = P.Union ASeq)
proof let P,ASeq such that
A1: ASeq is non-decreasing;
reconsider V = Union ASeq as Event of Sigma by PROB_1:58;
set BSeq = @Complement ASeq;
A2: BSeq = Complement ASeq by Def2;
then A3: BSeq is non-increasing by A1,Lm1;
then A4: P * BSeq is convergent by PROB_1:def 13;
Intersection BSeq = (Union Complement Complement ASeq)` by A2,PROB_1:def 5
.= (Union ASeq)` by PROB_1:31
.= Omega \ Union ASeq by SUBSET_1:def 5
.= [#] Sigma \ Union ASeq by PROB_1:def 11;
then A5: P.Intersection BSeq = 1 - P.V by PROB_1:68;
A6: now let n;
(P * BSeq).n = P.(BSeq.n) by Th11
.= P.((ASeq.n)`) by A2,PROB_1:def 4
.= P.(Omega \ ASeq.n) by SUBSET_1:def 5
.= P.([#] Sigma \ ASeq.n) by PROB_1:def 11
.= 1 - P.(ASeq.n) by PROB_1:68
.= 1 - (P * ASeq).n by Th11
.= 1 + - (P * ASeq).n by XCMPLX_0:def 8;
then - (P * ASeq).n = (P * BSeq).n - 1 by XCMPLX_1:26
.= - (1 - (P * BSeq).n) by XCMPLX_1:143;
hence (P * ASeq).n = -(- (1 - (P * BSeq).n))
.= 1 - (P * BSeq).n;
end;
hence P * ASeq is convergent by A4,Th5;
thus lim (P * ASeq) = 1 - lim (P * BSeq) by A4,A6,Th5
.= 1 - (1 - P.V) by A3,A5,PROB_1:def 13
.= 1 - 1 + P.V by XCMPLX_1:37
.= P.(Union ASeq);
end;
::
:: THEOREMS CONCERNED PROBABILITY
::
canceled 2;
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-decreasing 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-decreasing holds
(P * ASeq is convergent & lim (P * ASeq) = P.Union ASeq))
by Lm2,PROB_1:def 13;
assume that
A1: (for A holds 0 <= P.A) &
(P.Omega = 1) &
(for A,B st A misses B holds P.(A \/ B) = P.A + P.B) and
A2: (for ASeq st ASeq is non-decreasing holds
(P * ASeq is convergent & lim (P * ASeq) = P.Union ASeq));
(for ASeq st ASeq is non-increasing holds
(P * ASeq is convergent & lim (P * ASeq) = P.Intersection ASeq))
proof let ASeq such that
A3: ASeq is non-increasing;
A4: for A holds P.(A`) = 1 - P.A
proof let A;
reconsider B = A` as Event of Sigma by PROB_1:50;
A5:A misses B by SUBSET_1:44;
1 = P.[#]Omega by A1,SUBSET_1:def 4
.= P.(A \/ B) by SUBSET_1:25
.= P.A + P.B by A1,A5;
hence thesis by XCMPLX_1:26;
end;
Intersection ASeq = @Intersection ASeq by Def1;
then reconsider V = Intersection ASeq as Event of Sigma;
set BSeq = @Complement ASeq;
A6: BSeq = Complement ASeq by Def2;
then A7: BSeq is non-decreasing by A3,Th17;
then A8: P * BSeq is convergent by A2;
Union BSeq = (Union Complement ASeq)`` by Def2
.= (Intersection ASeq)` by PROB_1:def 5;
then A9: P.Union BSeq = 1 - P.V by A4;
A10: now let n;
(P * BSeq).n = P.(BSeq.n) by Th11
.= P.((ASeq.n)`) by A6,PROB_1:def 4
.= 1 - P.(ASeq.n) by A4
.= 1 - (P * ASeq).n by Th11
.= 1 + - (P * ASeq).n by XCMPLX_0:def 8;
then - (P * ASeq).n = (P * BSeq).n - 1 by XCMPLX_1:26
.= - (1 - (P * BSeq).n) by XCMPLX_1:143;
hence (P * ASeq).n = -(- (1 - (P * BSeq).n))
.= 1 - (P * BSeq).n;
end;
hence P * ASeq is convergent by A8,Th5;
thus lim (P * ASeq) = 1 - lim (P * BSeq) by A8,A10,Th5
.= 1 - (1 - P.V) by A2,A7,A9
.= 1 - 1 + P.V by XCMPLX_1:37
.= P.(Intersection ASeq);
end;
hence thesis by A1,PROB_1:def 13;
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 \/ B) + P.C - P.((A \/ B) /\ C) by PROB_1:74
.= P.A + P.B - P.(A /\ B) + P.C - P.((A \/ B) /\ C) by PROB_1:74
.= P.A + P.B + P.C - P.(A /\ B) - P.((A \/ B) /\ C) by XCMPLX_1:29
.= P.A + P.B + P.C - (P.(A /\ B) + P.((A \/ B) /\ C)) by XCMPLX_1:36;
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:74
.= 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;
then P.(A \/ B \/ C) =P.A + P.B + P.C - (P.(A /\ B) + (P.(B /\ C) + P.(A /\
C) +
- P.(A /\ B /\ C))) by A1,XCMPLX_0:def 8
.= P.A + P.B + P.C - (P.(A /\ B) + (P.(B /\ C) + P.(A /\ C)) +
- P.(A /\ B /\ C)) by XCMPLX_1:1
.= P.A + P.B + P.C - (P.(A /\ B) + P.(B /\ C) + P.(A /\ C) +
- P.(A /\ B /\ C)) by XCMPLX_1:1
.= P.A + P.B + P.C - (P.(A /\ B) + P.(B /\ C) + P.(A /\ C)
- P.(A /\ B /\ C)) by XCMPLX_0:def 8
.= P.A + P.B + P.C - (P.(A /\ B) + P.(B /\ C) + P.(A /\ C))
+ P.(A /\ B /\ C) by XCMPLX_1:37;
hence thesis;
end;
theorem
Th22: P.(A \ (A /\ B)) = P.A - P.(A /\ B)
proof A /\ B c= A by XBOOLE_1:17;
hence thesis by PROB_1:69;
end;
theorem
Th23: P.(A /\ B) <= P.B & P.(A /\ B) <= P.A
proof
A1: A /\ B c= B by XBOOLE_1:17;
A /\ B c= A by XBOOLE_1:17;
hence thesis by A1,PROB_1:70;
end;
theorem
Th24: C = B` implies P.A = P.(A /\ B) + P.(A /\ C)
proof
assume A1: C = B`;
then B misses C by SUBSET_1:44;
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 Th6
.= P.(A /\ [#]Omega) by SUBSET_1:def 4
.= P.(A /\ (B \/ C)) by A1,SUBSET_1:25
.= P.(A /\ B \/ A /\ C) by XBOOLE_1:23
.= P.(A /\ B) + P.(A /\ C) by A2,PROB_1:def 13;
hence thesis;
end;
theorem
Th25: P.A + P.B - 1 <= P.(A /\ B)
proof
P.A + P.B - P.(A /\ B) = P.(A \/ B) by PROB_1:74;
then P.A + P.B - P.(A /\ B) <= 1 by PROB_1:71;
then P.A + P.B <= P.(A /\ B) + 1 by REAL_1:86;
hence thesis by REAL_1:86;
end;
theorem
Th26: P.A = 1 - P.([#] Sigma \ A)
proof
P.([#] Sigma \ A) + P.A = 1 by PROB_1:67;
hence thesis by XCMPLX_1:26;
end;
theorem
Th27: 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 Th26;
then 1 + - P.([#] Sigma \ A) < 1 by XCMPLX_0:def 8;
then - P.([#] Sigma \ A) < 1 - 1 by REAL_1:86;
then 0 < - (- P.([#] Sigma \ A)) by REAL_1:66;
hence thesis;
end; assume
0 < P.([#] Sigma \ A);
then 0 < 1 - P.A by PROB_1:68;
then P.A + 0 < 1 by REAL_1:86;
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:68;
then 1 + - P.A < 1 by XCMPLX_0:def 8;
then - P.A < 1 - 1 by REAL_1:86;
then 0 < - (- P.A) by REAL_1:66;
hence thesis;
end; assume
0 < P.A;
then 0 < 1 - P.([#] Sigma \ A) by Th26;
then P.([#] Sigma \ A) + 0 < 1 by REAL_1:86;
hence thesis;
end;
::
:: INDEPENDENCE OF EVENTS
::
definition
let Omega, Sigma, P, A, B;
pred A,B are_independent_respect_to P means
:Def5: P.(A /\ B) = P.A * P.B;
let C;
pred A,B,C are_independent_respect_to P means
:Def6: 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;
Lm3:A,B are_independent_respect_to P implies
B,A are_independent_respect_to P
proof assume A,B are_independent_respect_to P;
then P.(B /\ A) = P.B * P.A by Def5;
hence thesis by Def5;
end;
canceled 2;
theorem
A,B are_independent_respect_to P iff
B,A are_independent_respect_to P by Lm3;
theorem
Th32: (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))
proof
thus A,B,C are_independent_respect_to P implies
(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)
proof assume A,B,C are_independent_respect_to P;
then 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 by Def6;
hence thesis by Def5;
end;
assume (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);
then (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) by Def5;
hence thesis by Def6;
end;
theorem
A,B,C are_independent_respect_to P
implies B,A,C are_independent_respect_to P
proof
assume A,B,C are_independent_respect_to P;
then A1: (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) by Th32;
then B,A are_independent_respect_to P by Lm3;
hence thesis by A1,Th32;
end;
theorem
A,B,C are_independent_respect_to P
implies A,C,B are_independent_respect_to P
proof
assume A,B,C are_independent_respect_to P;
then A1: (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) by Th32;
then A2: P.(A /\ C /\ B) = P.A * P.B * P.C by XBOOLE_1:16
.= P.A * P.C * P.B by XCMPLX_1:4;
C,B are_independent_respect_to P by A1,Lm3;
hence thesis by A1,A2,Th32;
end;
theorem
for E being Event of Sigma st E = {} holds
A, E are_independent_respect_to P
proof
let E be Event of Sigma;
assume A1: E = {};
P.(A /\ ({} Sigma)) = P.A * 0 by PROB_1:64
.= P.A * P.({} Sigma) by PROB_1:64;
hence thesis by A1,Def5;
end;
theorem
A, [#] Sigma are_independent_respect_to P
proof
P.(A /\ ([#] Sigma)) = P.A * 1 by Th6
.= P.A * P.([#] Sigma) by PROB_1:66;
hence thesis by Def5;
end;
theorem
Th37: 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 by Def5;
P.(A /\ ([#] Sigma \ B)) = P.(A /\ (Omega \ B)) by PROB_1:def 11
.= P.(A /\ B`) by SUBSET_1:def 5
.= P.(A \ B) by SUBSET_1:32
.= P.(A \ (A /\ B)) by XBOOLE_1:47
.= P.A * 1 - P.A * P.B by A1,Th22
.= P.A * (1 - P.B) by XCMPLX_1:40
.= P.A * P.([#] Sigma \ B) by PROB_1:68;
hence thesis by Def5;
end;
theorem
Th38: 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 Th37;
then ([#] Sigma \ B),A are_independent_respect_to P by Lm3;
then ([#] Sigma \ B),([#] Sigma \ A) are_independent_respect_to P by Th37;
hence thesis by Lm3;
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
A1: A,B are_independent_respect_to P &
A,C are_independent_respect_to P & B misses C;
then A2: (A /\ B) misses (A /\ C) by XBOOLE_1:76;
P.(A /\ (B \/ C)) = P.((A /\ B) \/ (A /\ C)) by XBOOLE_1:23
.= P.(A /\ B) + P.(A /\ C) by A2,PROB_1:def 13
.= P.A * P.B + P.(A /\ C) by A1,Def5
.= P.A * P.B + P.A * P.C by A1,Def5
.= P.A * (P.B + P.C) by XCMPLX_1:8
.= P.A * P.(B \/ C) by A1,PROB_1:def 13;
hence thesis by Def5;
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 let P,A,B; assume that
A1: A,B are_independent_respect_to P and
A2: P.A < 1 and
A3: P.B < 1;
A4: ([#] Sigma \ A),([#] Sigma \ B) are_independent_respect_to P by A1,Th38;
A5: 0 < P.([#] Sigma \ A) by A2,Th27;
0 < P.([#] Sigma \ B) by A3,Th27;
then A6: 0 < P.([#] Sigma \ A) * P.([#] Sigma \ B) by A5,SQUARE_1:21;
A7: now let r,r1; assume 0 < r1;
then - r1 < 0 by REAL_1:26,50;
then r + - r1 < r + 0 by REAL_1:53;
hence r - r1 < r by XCMPLX_0:def 8;
end;
P.(A \/ B) = 1 - P.([#] Sigma \ (A \/ B)) by Th26
.= 1 - P.(([#] Sigma \ A) /\ ([#] Sigma \ B)) by XBOOLE_1:53
.= 1 - P.([#] Sigma \ A) * P.([#] Sigma \ B) by A4,Def5;
hence thesis by A6,A7;
end;
::
:: CONDITIONAL PROBABILITY
::
definition let Omega,Sigma,P,B;
assume A1: 0 < P.B;
func P.|.B -> Probability of Sigma means
:Def7: for A holds it.A = P.(A /\ B)/P.B;
existence
proof
defpred P[set,set] means ex A,r st (A = $1 & r = $2) &
r = P.(A /\ B)/P.B;
A2: for x st x in Sigma ex y st y in REAL & P[x,y]
proof let x; assume x in Sigma;
then reconsider x as Event of Sigma by PROB_1:48;
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 st x in Sigma holds P[x,f.x] from FuncEx1(A2);
A5: for A holds f.A = P.(A /\ B)/P.B
proof let A; A in Sigma by PROB_1:def 10;
then ex C,r1 st C = A & r1 = f.A & r1 = P.(C /\ B)/P.B by A4;
hence thesis;
end;
f is Probability of Sigma
proof
thus for A holds 0 <= f.A
proof let A;
0 <= P.(A /\ B) by PROB_1:def 13;
then 0 <= P.(A /\ B)/P.B by A1,SQUARE_1:27;
hence thesis by A5;
end;
thus f.Omega = f.([#] Sigma) by PROB_1:def 11
.= P.(([#] Sigma) /\ B)/P.B by A5
.= P.B/P.B by Th6
.= 1 by A1,XCMPLX_1:60;
thus for A,C st A misses C holds f.(A \/ C) = f.A + f.C
proof let A,C; assume A misses C;
then A6: 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 A6,PROB_1:def 13
.= P.(A /\ B)/P.B + P.(C /\ B)/P.B by XCMPLX_1:63
.= P.(A /\ B)/P.B + f.C by A5
.= f.A + f.C by A5;
end;
thus for ASeq st ASeq is non-increasing holds
(f*ASeq is convergent & lim (f*ASeq) = f.(Intersection ASeq))
proof let ASeq such that
A7: ASeq is non-increasing;
consider BSeq such that
A8: for n holds BSeq.n = ASeq.n /\ B by Th9;
A9: BSeq is non-increasing by A7,A8,Th10;
A10: dom(f*ASeq) = NAT by FUNCT_2:def 1;
A11: dom(P*BSeq) = NAT by FUNCT_2:def 1;
now let n;
assume n in dom(f*ASeq);
thus (f*ASeq).n = f.(ASeq.n) by Th11
.= P.(ASeq.n /\ B)/P.B by A5
.= P.(BSeq.n)/P.B by A8
.= (P*BSeq).n/P.B by Th11
.= (P.B)" * (P*BSeq).n by XCMPLX_0:def 9;
end;
then A12: f*ASeq = (P.B)" (#) (P*BSeq) by A10,A11,SEQ_1:def 6;
A13: P*BSeq is convergent & lim (P*BSeq) = P.(Intersection BSeq)
by A9,PROB_1:def 13;
hence f*ASeq is convergent by A12,SEQ_2:21;
A14: Intersection BSeq = @Intersection BSeq by Def1;
A15: Intersection ASeq = @Intersection ASeq by Def1;
thus lim (f*ASeq) = (P.B)" * P.(@Intersection BSeq) by A12,A13,A14,SEQ_2:
22
.= (P.(@Intersection BSeq))/P.B by XCMPLX_0:def 9
.= (P.((@Intersection ASeq) /\ B))/P.B
by A8,A14,A15,Th12
.= f.(Intersection ASeq) by A5,A15;
end;
end;
then reconsider f as Probability of Sigma;
take f;
thus thesis by A5;
end;
uniqueness
proof let P1,P2; assume that
A16: for A holds P1.A = P.(A /\ B)/P.B and
A17: for A holds P2.A = P.(A /\ B)/P.B;
now let A;
thus P1.A = P.(A /\ B)/P.B by A16
.= P2.A by A17;
end;
hence thesis by Th13;
end;
end;
canceled;
theorem
Th42: 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 Def7
.= P.(A /\ B) * (P.B)" * P.B by XCMPLX_0:def 9
.= P.(A /\ B) * ((P.B)" * P.B) by XCMPLX_1:4
.= 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 Th23;
P.(A /\ B /\ C) = P.(B /\ A) * P.|.(A /\ B).C by A1,Th42
.= P.A * P.|.A.B * P.|.(A /\ B).C by A2,Th42;
hence thesis;
end;
theorem
:: Total Probability Rule for Two Events
Th44: 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,Th24
.= P.|.B.A * P.B + P.(A /\ C) by A2,Th42
.= P.|.B.A * P.B + P.|.C.A * P.C by A3,Th42;
hence thesis;
end;
theorem
:: Total Probability Rule for Three Events
Th45: 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:44;
then A7: A /\ (A1 \/ A2) misses A /\ A3 by XBOOLE_1:76;
A8: A1 \/ A2 \/ A3 = [#]Omega by A2,SUBSET_1:25
.= Omega by SUBSET_1:def 4;
(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,Th42
.= P.(A /\ A1) + P.(A /\ A2) + (P.|.A3.A * P.A3) by A4,Th42
.= P.(A /\ A1) + P.(A /\ A2) + P.(A /\ A3) by A5,Th42
.= P.((A /\ A1) \/ (A /\ A2)) + P.(A /\ A3) by A6,PROB_1:def 13
.= P.(A /\ (A1 \/ A2)) + P.(A /\ A3) by XBOOLE_1:23
.= P.((A /\ (A1 \/ A2)) \/ (A /\ A3)) by A7,PROB_1:def 13
.= P.(A /\ Omega) by A8,XBOOLE_1:23
.= P.A by Th6;
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,Def7;
then P.(A /\ B) = P.A * P.B by A1,XCMPLX_1:88;
hence thesis by Def5;
end; assume A,B are_independent_respect_to P;
then P.(A /\ B) * (P.B)" = P.A * P.B * (P.B)" by Def5;
then P.(A /\ B) * (P.B)" = P.A * (P.B * (P.B)") by XCMPLX_1:4;
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,Def7;
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;
A4: 0 < P.([#] Sigma \ B) by A2,Th27;
A5: P.([#] Sigma \ B) <> 0 by A2,Th27;
A6: B`= (Omega \ B) by SUBSET_1:def 5
.= ([#] Sigma \ B) by PROB_1:def 11;
P.(A /\ B)/P.B = P.|.([#] Sigma \B).A by A1,A3,Def7;
then P.(A /\ B)/P.B = P.(A /\ ([#] Sigma \B))/P.([#] Sigma \ B) by A4,Def7;
then P.(A /\ B) * P.([#] Sigma \ B) = P.(A /\ ([#] Sigma \B)) * P.B by A1,A5,
Th4;
then P.(A /\ B) * (1 - P.B) = P.(A /\ ([#] Sigma \B)) * P.B by PROB_1:68;
then P.(A /\ B) * 1 - P.(A /\ B) * P.B = P.(A /\ ([#] Sigma \B)) * P.B
by XCMPLX_1:40;
then P.(A /\ B) + - P.(A /\ B) * P.B = P.(A /\ ([#] Sigma \B)) * P.B
by XCMPLX_0:def 8;
then P.(A /\ B) = P.(A /\ ([#] Sigma \B)) * P.B -(- P.(A /\ B) * P.B)
by XCMPLX_1:26
.= P.(A /\ ([#] Sigma \B)) * P.B + -(- P.(A /\ B) * P.B) by XCMPLX_0:def 8
.= (P.(A /\ ([#] Sigma \B)) + P.(A /\ B)) * P.B by XCMPLX_1:8
.= P.A * P.B by A6,Th24;
hence thesis by Def5;
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.(A /\ B) by Th25;
then (P.A + P.B - 1)/P.B <= P.(A /\ B)/P.B by A1,REAL_1:73;
hence thesis by A1,Def7;
end;
theorem
Th49: 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
A1: 0 < P.A & 0 < P.B;
hence P.|.A.B * P.A / P.B = P.(A /\ B) / P.B by Th42
.= P.|.B.A by A1,Def7;
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,Th44
.= P.|.B.A1 by A1,A3,Th49;
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,Th44
.= P.|.B.A2 by A1,A4,Th49;
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 and
A6: 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,A6,Th45
.= P.|.B.A1 by A1,A2,Th49;
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,A6,Th45
.= P.|.B.A2 by A1,A3,Th49;
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,A6,Th45
.= P.|.B.A3 by A1,A4,Th49;
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 Th25;
then P.B + (P.A - 1) <= P.(A /\ B) by XCMPLX_1:29;
then P.B + -(1 - P.A) <= P.(A /\ B) by XCMPLX_1:143;
then P.B + -P.([#] Sigma \ A) <= P.(A /\ B) by PROB_1:68;
then (P.B + -P.([#] Sigma \ A))/P.B <= P.(A /\ B)/P.B by A1,REAL_1:73;
then (P.B + -P.([#] Sigma \ A))/P.B <= P.|.B.A by A1,Def7;
then (P.B - P.([#] Sigma \ A))/P.B <= P.|.B.A by XCMPLX_0:def 8;
then P.B/P.B - P.([#] Sigma \ A)/P.B <= P.|.B.A by XCMPLX_1:121;
hence thesis by A1,XCMPLX_1:60;
end;