Copyright (c) 1990 Association of Mizar Users
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;
definitions XBOOLE_0;
theorems AXIOMS, TARSKI, SUBSET_1, ZFMISC_1, FINSEQ_1, REAL_1, CARD_1, CARD_2,
SQUARE_1, PROB_1, REALSET1, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1;
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;
existence
proof
consider x being set such that
A1: x in E by XBOOLE_0:def 1;
take {x};
thus thesis by A1,REALSET1:def 12,ZFMISC_1:37;
end;
end;
definition let E;
mode El_ev of E is non empty trivial Subset of E;
end;
theorem Th1:
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)
proof
let e be non empty Subset of E;
thus e is El_ev of E implies for Y holds (Y c= e iff Y = {} or Y = e)
proof
assume e is El_ev of E;
then consider x being set such that
A1: e = {x} by REALSET1:def 12;
let Y;
thus Y c= e iff Y = {} or Y = e by A1,ZFMISC_1:39;
end;
assume A2: for Y holds Y c= e iff Y = {} or Y = e;
consider x being set such that
A3:x in e by XBOOLE_0:def 1;
e is trivial
proof
{x} c= e by A3,ZFMISC_1:37;
then {x} = e by A2;
hence thesis by REALSET1:def 12;
end;
hence e is El_ev of E;
end;
definition let E;
cluster -> finite El_ev of E;
coherence
proof
let e be El_ev of E;
per cases by REALSET1:def 12;
suppose e is empty;
then reconsider T = e as empty set;
T is finite;
hence thesis;
suppose ex x being set st e = {x};
hence thesis;
end;
end;
reserve e, e1, e2 for El_ev of E;
canceled 3;
theorem
e = A \/ B & A <> B implies
A = {} & B = e or A = e & B = {}
proof
assume that
A1: e = A \/ B and
A2: A <> B;
A c= e & B c= e by A1,XBOOLE_1:7;
then ( A = {} or A = e ) & ( B = {} or B = e ) by Th1;
hence thesis by A2;
end;
theorem
e = A \/ B implies A = e & B = e or
A = e & B = {} or A = {} & B = e
proof
assume A1: e = A \/ B;
then A c= e & B c= e by XBOOLE_1:7;
then A = {} & B = e or A = e & B = {} or A = e & B = e or
A = {} & B = {} by Th1;
hence thesis by A1;
end;
theorem Th7:
{a} is El_ev of E
proof
set e = {a};
e c= E & e <> {} & ( Y c= e iff Y = {} or Y = e ) by ZFMISC_1:39;
hence thesis by Th1;
end;
canceled 2;
theorem
e1 c= e2 implies e1 = e2 by Th1;
theorem Th11:
ex a st a in E & e = {a}
proof
consider x being Element of e;
A1:{x} c= e;
reconsider x as Element of E;
x in E & {x} = e by A1,Th1;
hence thesis;
end;
theorem
ex e st e is El_ev of E
proof
consider a being Element of E;
{a} is El_ev of E by Th7;
hence thesis;
end;
canceled;
theorem
ex p st p is FinSequence of E & rng p = e & len p = 1
proof
consider a such that
A1: a in E & e = {a} by Th11;
reconsider p = <*a*> as FinSequence;
A2: rng p = {a} by FINSEQ_1:56;
len p = 1 by FINSEQ_1:56;
hence thesis by A1,A2;
end;
definition let E be set;
mode Event of E is Subset of E;
end;
canceled 7;
theorem
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
proof
let E be non empty set, e be El_ev of E, A be Event of E;
A1: e /\ E = e by XBOOLE_1:28;
A \/ A` = [#] E by SUBSET_1:25;
then A \/ A` = E by SUBSET_1:def 4;
then e = e /\ A \/ e /\ A` by A1,XBOOLE_1:23;
then e /\ A c= e by XBOOLE_1:7;
then e /\ A = {} or e /\ A = e by Th1;
hence thesis by XBOOLE_0:def 7;
end;
canceled 2;
theorem
for E being non empty set, A being Event of E st A <> {}
ex e being El_ev of E st e c= A
proof
let E be non empty set, A be Event of E;
assume A1: A <> {};
consider x being Element of A;
reconsider x as Element of E by A1,TARSKI:def 3;
A2: {x} is El_ev of E by Th7;
{x} c= A by A1,ZFMISC_1:37;
hence thesis by A2;
end;
theorem
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`
proof
let E be non empty set, e be El_ev of E, A be Event of E;
assume
A1: e c= A \/ A`;
ex a being Element of E st a in E & e = {a} by Th11;
then consider a being Element of E such that
A2: e = {a};
a in A \/ A` by A1,A2,ZFMISC_1:37;
then a in A or a in A` by XBOOLE_0:def 2;
hence thesis by A2,ZFMISC_1:37;
end;
theorem
e1 = e2 or e1 misses e2
proof
e1 /\ e2 c= e1 by XBOOLE_1:17;
then e1 /\ e2 = {} or e1 /\ e2 = e1 by Th1;
then e1 c= e2 or e1 /\ e2 = {} by XBOOLE_1:17;
hence thesis by Th1,XBOOLE_0:def 7;
end;
canceled 6;
theorem Th34:
A /\ B misses A /\ B`
proof
A /\ B misses A \ B by XBOOLE_1:89;
hence thesis by SUBSET_1:32;
end;
Lm1:
for E being finite non empty set holds 0 < card E
proof
let E be finite non empty set;
consider x being Element of E;
card {x} <= card E by CARD_1:80;
then 1 <= card E by CARD_1:79;
hence thesis by AXIOMS:22;
end;
Lm2:
card e = 1
proof
ex a st a in E & {a} = e by Th11;
hence thesis by CARD_1:79;
end;
definition
let E be finite non empty set;
let A be Event of E;
canceled 3;
func prob(A) -> Real equals
:Def4: card A / card E;
coherence;
end;
canceled 3;
theorem
for E being finite non empty set, e being El_ev of E holds
prob(e) = 1 / card E
proof
let E be finite non empty set, e be El_ev of E;
prob(e) = card e / card E by Def4;
hence thesis by Lm2;
end;
theorem Th39:
for E being finite non empty set holds prob([#] E) = 1
proof
let E be finite non empty set;
reconsider EE = [#] E as Subset of E;
prob([#] E) = card EE / card E by Def4;
then A1: prob([#] E) = card E / card E by SUBSET_1:def 4;
card E <> 0 by Lm1;
hence thesis by A1,XCMPLX_1:60;
end;
theorem Th40:
for E being finite non empty set holds prob({} E) = 0
proof let E be finite non empty set;
card {} / card E = 0 by CARD_1:78;
hence thesis by Def4;
end;
theorem Th41:
for E being finite non empty set, A,B being Event of E st A misses B
holds prob(A /\ B) = 0
proof
let E be finite non empty set, A,B be Event of E;
assume A misses B;
then A /\ B = {} E by XBOOLE_0:def 7;
hence thesis by Th40;
end;
theorem
for E being finite non empty set, A being Event of E holds prob(A) <= 1
proof
let E be finite non empty set, A be Event of E;
A1: prob(A) = card A / card E by Def4;
reconsider EE = [#] E as Subset of E;
prob [#] E = card EE / card E by Def4;
then A2: prob([#] E) = card E / card E by SUBSET_1:def 4;
A3: card A <= card E by CARD_1:80;
0 < card E by Lm1;
then 0 <= (card E)" by REAL_1:72;
then card A * (card E)" <= card E * (card E)" by A3,AXIOMS:25;
then card A / card E <= card E * (card E)" by XCMPLX_0:def 9;
then prob(A) <= card E / card E by A1,XCMPLX_0:def 9;
hence thesis by A2,Th39;
end;
theorem Th43:
for E being finite non empty set, A being Event of E holds 0 <= prob(A)
proof
let E be finite non empty set, A be Event of E;
A1: prob(A) = card A / card E by Def4;
0 < card E by Lm1;
then A2: 0 <= (card E)" by REAL_1:72;
{} c= A by XBOOLE_1:2;
then 0 <= card A by CARD_1:78,80;
then 0 * (card E)" <= card A * (card E)" by A2,AXIOMS:25;
hence thesis by A1,XCMPLX_0:def 9;
end;
theorem Th44:
for E being finite non empty set, A,B being Event of E st A c= B holds
prob(A) <= prob(B)
proof
let E be finite non empty set, A,B be Event of E;
assume A c= B;
then A1: card A <= card B by CARD_1:80;
0 < card E by Lm1;
then 0 <= (card E)" by REAL_1:72;
then card A * (card E)" <= card B * (card E)" by A1,AXIOMS:25;
then card A / card E <= card B * (card E)" by XCMPLX_0:def 9;
then card A / card E <= card B / card E by XCMPLX_0:def 9;
then prob(A) <= card B / card E by Def4;
hence thesis by Def4;
end;
canceled;
theorem Th46:
for E being finite non empty set, A,B being Event of E holds
prob(A \/ B) = prob(A) + prob(B) - prob(A /\ B)
proof
let E be finite non empty set, A,B be Event of E;
card (( A \/ B ) qua Event of E) = card A + card B - card ( A /\ B )
by CARD_2:64;
then A1: card ( A \/ B ) = card A + ( card B - card ( A /\ B )) by XCMPLX_1:29;
set q = ( card E )";
set p = card E;
card ( A \/ B ) * q = card A * q +
( card B - card ( A /\ B )) * q by A1,XCMPLX_1:8;
then card ( A \/ B ) * q = card A * q +
( card B * q - card ( A /\ B ) * q ) by XCMPLX_1:40;
then card ( A \/ B ) * q = card A * q +
card B * q - card ( A /\ B ) * q by XCMPLX_1:29;
then card ( A \/ B ) / p = card A * q + card B * q
- card ( A /\ B ) * q by XCMPLX_0:def 9;
then card ( A \/ B ) / p = card A / p + card B * q
- card ( A /\ B ) * q by XCMPLX_0:def 9;
then card ( A \/ B ) / p = card A / p + card B / p
- card ( A /\ B ) * q by XCMPLX_0:def 9;
then card ( A \/ B ) / p = card A / p + card B / p
- card ( A /\ B ) / p by XCMPLX_0:def 9;
then prob(A \/ B) = card A / p + card B / p
- card ( A /\ B ) / p by Def4;
then prob(A \/ B) = prob(A) + card B / p
- card ( A /\ B ) / p by Def4;
then prob(A \/ B) = prob(A) + prob(B) - card ( A /\ B ) / p by Def4;
hence thesis by Def4;
end;
theorem Th47:
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)
proof
let E be finite non empty set, A,B be Event of E;
assume A misses B;
then prob(A /\ B) = 0 by Th41;
then prob(A \/ B) = prob(A) + prob(B) - 0 by Th46;
hence thesis;
end;
theorem Th48:
for E being finite non empty set, A being Event of E holds
prob(A) = 1 - prob(A`) & prob(A`) = 1 - prob(A)
proof
let E be finite non empty set, A be Event of E;
A misses A` by SUBSET_1:44;
then prob(A \/ A`) = prob(A) + prob(A`) by Th47;
then prob( [#] E ) = prob(A) + prob(A`) by SUBSET_1:25;
then 1 = prob(A) + prob(A`) by Th39;
hence thesis by XCMPLX_1:26;
end;
theorem Th49:
for E being finite non empty set, A,B being Event of E holds
prob(A \ B) = prob(A) - prob(A /\ B)
proof
let E be finite non empty set, A,B be Event of E;
A1: prob(A) = prob((A \ B) \/ (A /\ B)) by XBOOLE_1:51;
A \ B misses A /\ B by XBOOLE_1:89;
then prob(A) = prob(A \ B) + prob(A /\ B) by A1,Th47;
hence thesis by XCMPLX_1:26;
end;
theorem Th50:
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)
proof
let E be finite non empty set, A,B be Event of E;
assume B c= A;
then prob(A /\ B) = prob(B) by XBOOLE_1:28;
hence thesis by Th49;
end;
theorem
for E being finite non empty set, A,B being Event of E holds
prob(A \/ B) <= prob(A) + prob(B)
proof
let E be finite non empty set, A,B be Event of E;
A1: prob(A \/ B) = prob(A) + prob(B) - prob(A /\ B) by Th46;
0 <= prob(A /\ B) by Th43;
hence thesis by A1,PROB_1:2;
end;
canceled;
theorem Th53:
for E being finite non empty set, A,B being Event of E holds
prob(A) = prob(A /\ B) + prob(A /\ B`)
proof
let E be finite non empty set, A,B be Event of E;
A /\ B misses A /\ B` by Th34;
then A1: prob((A /\ B) \/ (A /\ B`)) = prob(A /\ B) + prob(A /\ B`) by Th47;
A = A /\ ( A \/ [#] E ) by XBOOLE_1:21;
then A = A /\ [#] E by SUBSET_1:28;
then A = A /\ ( B \/ B`) by SUBSET_1:25;
hence thesis by A1,XBOOLE_1:23;
end;
theorem
for E being finite non empty set, A,B being Event of E holds
prob(A) = prob(A \/ B) - prob(B \ A)
proof
let E be finite non empty set, A,B be Event of E;
A1: A misses ( B \ A ) by XBOOLE_1:79;
prob(A \/ (B \ A)) = prob(A \/ B) by XBOOLE_1:39;
then prob(A \/ B) = prob(A) + prob(B \ A) by A1,Th47;
hence thesis by XCMPLX_1:26;
end;
theorem
for E being finite non empty set, A,B being Event of E holds
prob(A) + prob(A` /\ B) = prob(B) + prob(B` /\ A)
proof
let E be finite non empty set, A,B be Event of E;
prob(A) = prob(A /\ B) + prob(A /\ B`) by Th53;
then A1: prob(A /\ B) = prob(A) - prob(B` /\ A) by XCMPLX_1:26;
prob(B) = prob(A /\ B) + prob(B /\ A`) by Th53;
then prob(A) - prob(B` /\ A) = prob(B) - prob(A` /\ B) by A1,XCMPLX_1:26;
then prob(A) - ( prob(B` /\ A) - prob(B` /\ A) ) =
prob(B) - prob(A` /\ B) + prob(B` /\ A) by XCMPLX_1:37;
then prob(A) - 0 = prob(B) - prob(A` /\ B) + prob(B` /\ A) by XCMPLX_1:14;
then prob(A) = prob(B) + -prob(A` /\ B) + prob(B` /\ A) by XCMPLX_0:def 8;
then prob(A) + prob(A` /\ B) = prob(B) + prob(B` /\ A) +
-prob(A` /\ B) + prob(A` /\ B) by XCMPLX_1:1;
then prob(A) + prob(A` /\ B) = prob(B) + prob(B` /\ A) -
prob(A` /\ B) + prob(A` /\ B) by XCMPLX_0:def 8;
then prob(A) + prob(A` /\ B) = prob(B) + prob(B` /\ A) -
( prob(A` /\ B) - prob(A` /\ B) ) by XCMPLX_1:37;
then prob(A) + prob(A` /\ B) = prob(B) + prob(B` /\ A) - 0 by XCMPLX_1:14;
hence thesis;
end;
theorem Th56:
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)
proof
let E be finite non empty set, A,B,C be Event of E;
prob(A \/ B \/ C) = prob(A \/ B) + prob(C) - prob((A \/ B) /\ C) by Th46
.= ( ( prob(A) + prob(B) ) - prob(A /\ B) ) + prob(C) -
prob((A \/ B) /\ C) by Th46
.= ( ( prob(A) + prob(B) ) + -prob(A /\ B) ) + prob(C) -
prob((A \/ B) /\ C) by XCMPLX_0:def 8
.= ( prob(A) + prob(B) + prob(C) ) + -prob(A /\ B) -
prob((A \/ B) /\ C) by XCMPLX_1:1
.= ( prob(A) + prob(B) + prob(C) ) + -prob(A /\ B) -
prob((A /\ C) \/ (B /\ C)) by XBOOLE_1:23
.= ( prob(A) + prob(B) + prob(C) ) + -prob(A /\ B) -
( prob(A /\ C) + prob(B /\ C) - prob((A /\ C) /\ (B /\ C)) ) by Th46
.= ( prob(A) + prob(B) + prob(C) ) + -prob(A /\ B) -
( prob(A /\ C) + prob(B /\ C) - prob(A /\ ( C /\ (C /\ B)) )) by XBOOLE_1:16
.= ( prob(A) + prob(B) + prob(C) ) + -prob(A /\ B) -
( prob(A /\ C) + prob(B /\ C) - prob(A /\ (( C /\ C ) /\ B) )) by XBOOLE_1:
16
.= (( prob(A) + prob(B) + prob(C) ) + -prob(A /\ B)) -
( prob(A /\ C) + prob(B /\ C) - prob(A /\ B /\ C) ) by XBOOLE_1:16
.= (( prob(A) + prob(B) + prob(C) ) + -prob(A /\ B)) -
( prob(A /\ C) + prob(B /\ C) ) + prob(A /\ B /\ C) by XCMPLX_1:37
.= ( prob(A) + prob(B) + prob(C) ) + ( -(1 * prob(A /\ B)) -
( prob(A /\ C) + prob(B /\ C) )) + prob(A /\ B /\ C) by XCMPLX_1:29
.= ( prob(A) + prob(B) + prob(C) ) + ( (-1) * prob(A /\ B) -
( 1 * ( prob(A /\ C) + prob(B /\ C) ))) + prob(A /\ B /\ C) by XCMPLX_1:175
.= ( prob(A) + prob(B) + prob(C) ) + ( (-1) * prob(A /\ B) +
-(1*( prob(A /\ C) + prob(B /\ C) ))) + prob(A /\ B /\ C) by XCMPLX_0:def 8
.= ( prob(A) + prob(B) + prob(C) ) + ( (-1) * prob(A /\ B) +
(-1) * ( prob(A /\ C) + prob(B /\ C) )) + prob(A /\ B /\ C) by XCMPLX_1:175
.= ( prob(A) + prob(B) + prob(C) ) + (-1) * ( prob(A /\ B)
+ ( prob(A /\ C) + prob(B /\ C) )) + prob(A /\ B /\ C) by XCMPLX_1:8
.= ( prob(A) + prob(B) + prob(C) ) + -( 1 * ( prob(A /\ B) +
( prob(A /\ C) + prob(B /\ C) ))) + prob(A /\ B /\ C) by XCMPLX_1:175
.= ( prob(A) + prob(B) + prob(C) ) + -( prob(A /\ B) +
prob(A /\ C) + prob(B /\ C) ) + prob(A /\ B /\ C) by XCMPLX_1:1;
hence thesis by XCMPLX_0:def 8;
end;
theorem
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)
proof
let E be finite non empty set, A,B,C be Event of E;
assume that
A1: A misses B and
A2: A misses C and
A3: B misses C;
A misses (B /\ C) by A1,XBOOLE_1:74;
then A4: prob(A /\ (B /\ C)) = 0 by Th41;
prob(A \/ B \/ C) = ( prob(A) + prob(B) + prob(C) ) - ( prob(A /\ B) +
prob(A /\ C) + prob(B /\ C) ) + prob(A /\ B /\ C) by Th56
.= ( prob(A) + prob(B) + prob(C) ) - ( prob(A /\ B) + prob(A /\ C) +
prob(B /\ C) ) + 0 by A4,XBOOLE_1:16
.= ( prob(A) + prob(B) + prob(C) ) - ( prob(A /\ B) + prob(A /\ C) + 0 )
by A3,Th41
.= ( prob(A) + prob(B) + prob(C) ) - ( prob(A /\ B) + 0 ) by A2,Th41
.= ( prob(A) + prob(B) + prob(C) ) - 0 by A1,Th41;
hence thesis;
end;
theorem
for E being finite non empty set, A,B being Event of E holds
prob(A) - prob(B) <= prob(A \ B)
proof
let E be finite non empty set, A,B be Event of E;
A /\ B c= B by XBOOLE_1:17;
then prob(A /\ B) <= prob(B) by Th44;
then prob(A) - prob(B) <= prob(A) - prob(A /\ B) by REAL_1:92;
hence thesis by Th49;
end;
definition
let E be finite non empty set;
let B,A be Event of E;
func prob(A , B) -> Real equals
:Def5: prob(A /\ B) / prob(B);
coherence;
end;
canceled;
theorem Th60:
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)
proof
let E be finite non empty set, A,B be Event of E;
assume
A1: 0 < prob(B);
prob(A , B) * prob(B) = prob(A /\ B) / prob(B) * prob(B) by Def5;
hence thesis by A1,XCMPLX_1:88;
end;
theorem Th61:
for E being finite non empty set, A being Event of E holds
prob(A , [#] E ) = prob(A)
proof
let E be finite non empty set, A be Event of E;
prob([#] E) = 1 by Th39;
then A1:prob(A , [#] E) = prob(A /\ [#] E) / 1 by Def5;
A c= E;
then A c= [#] E by SUBSET_1:def 4;
hence thesis by A1,XBOOLE_1:28;
end;
theorem
for E being finite non empty set holds prob([#] E , [#] E) = 1
proof let E be finite non empty set;
prob([#] E) = 1 by Th39;
hence thesis by Th61;
end;
theorem
for E being finite non empty set holds prob({} E , [#] E) = 0
proof let E be finite non empty set;
prob({} E , [#] E) = prob({} E) by Th61;
hence thesis by Th40;
end;
theorem
for E being finite non empty set, A,B being Event of E st 0 < prob(B)
holds prob(A , B) <= 1
proof
let E be finite non empty set, A,B be Event of E;
assume
A1: 0 < prob(B);
then A2: 0 <= (prob(B))" by REAL_1:72;
A3: prob(A , B) = prob(A /\ B) / prob(B) by Def5;
A /\ B c= B by XBOOLE_1:17;
then prob(A /\ B) <= prob(B) by Th44;
then prob(A /\ B) * (prob(B))" <= prob(B) * (prob(B))" by A2,AXIOMS:25;
then prob(A /\ B) * (prob(B))" <= 1 by A1,XCMPLX_0:def 7;
hence thesis by A3,XCMPLX_0:def 9;
end;
theorem
for E being finite non empty set, A,B being Event of E st 0 < prob(B)
holds 0 <= prob(A , B)
proof
let E be finite non empty set, A,B be Event of E;
assume
A1: 0 < prob(B);
0 <= prob(A /\ B) by Th43;
then 0 <= prob(A /\ B) / prob(B) by A1,SQUARE_1:27;
hence thesis by Def5;
end;
theorem Th66:
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)
proof
let E be finite non empty set, A,B be Event of E;
assume
A1: 0 < prob(B);
A2: prob(A , B) = prob(A /\ B) / prob(B) by Def5;
prob(B \ A) + prob(A /\ B) =
( prob(B) - prob(A /\ B) ) + prob(A /\ B) by Th49;
then ( prob(A /\ B) + prob(B \ A) ) - prob(B \ A) =
prob(B) - prob(B \ A) by XCMPLX_1:27;
then prob(A , B) = ( prob(B) - prob(B \ A) ) / prob(B) by A2,XCMPLX_1:26;
then prob(A , B) = prob(B) / prob(B) - prob(B \ A) / prob(B)
by XCMPLX_1:121;
hence thesis by A1,XCMPLX_1:60;
end;
theorem
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)
proof
let E be finite non empty set, A,B be Event of E;
assume that
A1: 0 < prob(B) and
A2: A c= B;
prob(A , B) = 1 - prob(B \ A) / prob(B) by A1,Th66;
then prob(A , B) = 1 - ( prob(B) - prob(A) ) / prob(B) by A2,Th50;
then prob(A , B) = 1 - ( prob(B) / prob(B) - prob(A) / prob(B) )
by XCMPLX_1:121;
then prob(A , B) = 1 - ( 1 - prob(A) / prob(B) ) by A1,XCMPLX_1:60;
then prob(A , B) = 1 - 1 + prob(A) / prob(B) by XCMPLX_1:37; hence
thesis;
end;
theorem Th68:
for E being finite non empty set, A,B being Event of E st
A misses B holds prob(A , B) = 0
proof
let E be finite non empty set, A,B be Event of E;
assume
A misses B;
then prob(A /\ B) = 0 by Th41;
then prob(A , B) = 0 / prob(B) by Def5
.= 0 * (prob(B))";
hence thesis;
end;
theorem Th69:
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)
proof
let E be finite non empty set, A,B be Event of E;
assume that
A1: 0 < prob(A) and
A2: 0 < prob(B);
prob(A) * prob(B , A) = prob(A /\ B) by A1,Th60;
hence thesis by A2,Th60;
end;
theorem Th70:
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)
proof
let E be finite non empty set, A,B be Event of E;
assume
A1: 0 < prob(B);
A2: (A \/ A`) /\ B = [#] E /\ B by SUBSET_1:25;
[#] E /\ B = B
proof
[#] E /\ B = E /\ B by SUBSET_1:def 4;
hence thesis by XBOOLE_1:28;
end;
then A3: (A /\ B) \/ (A` /\ B) = B by A2,XBOOLE_1:23;
A /\ B misses B /\ A` by Th34;
then prob(A /\ B) + prob(A` /\ B) = prob(B) by A3,Th47;
then prob(A , B) * prob(B) + prob(A` /\ B) = prob(B) by A1,Th60;
then prob(A , B) * prob(B) + prob(A` , B) * prob(B) = prob(B)
by A1,Th60;
then ( prob(A , B) + prob(A` , B) ) * prob(B) = prob(B) by XCMPLX_1:8;
then ( prob(A , B) + prob(A` , B) ) * prob(B) * (prob(B))" = 1
by A1,XCMPLX_0:def 7;
then ( prob(A , B) + prob(A` , B) ) * ( prob(B) * (prob(B))" ) = 1
by XCMPLX_1:4;
then ( prob(A , B) + prob(A` , B) ) * 1 = 1 by A1,XCMPLX_0:def 7;
hence thesis by XCMPLX_1:26;
end;
theorem Th71:
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
proof
let E be finite non empty set, A,B be Event of E;
assume that
A1: 0 < prob(B) and
A2: B c= A;
prob(A /\ B) = prob(B) by A2,XBOOLE_1:28;
then prob(A , B) = prob(B) / prob(B) by Def5;
hence thesis by A1,XCMPLX_1:60;
end;
theorem
for E being finite non empty set, B being Event of E st 0 < prob(B)
holds prob([#] E , B) = 1
proof
let E be finite non empty set, B be Event of E;
assume
A1: 0 < prob(B);
B c= E;
then B c= [#] E by SUBSET_1:def 4;
hence thesis by A1,Th71;
end;
theorem
for E being finite non empty set, A being Event of E st 0 < prob(A)
holds prob(A` , A) = 0
proof
let E be finite non empty set, A be Event of E;
assume
A1: 0 < prob(A);
A` misses A by SUBSET_1:44;
then prob(A` /\ A) = 0 by Th41;
then prob(A` , A) * prob(A) = 0 by A1,Th60;
hence thesis by A1,XCMPLX_1:6;
end;
theorem
for E being finite non empty set, A being Event of E st prob(A) < 1
holds prob(A , A`) = 0
proof
let E be finite non empty set, A be Event of E;
assume
prob(A) < 1;
then prob(A) -1 < 1 - 1 by REAL_1:54;
then - ( 1 - prob(A) ) < 0 by XCMPLX_1:143;
then 0 < - ( - ( 1 - prob(A) ) ) by REAL_1:66;
then A1: 0 < prob(A`) by Th48;
A misses A` by SUBSET_1:44;
then prob(A /\ A`) = 0 by Th41;
then prob(A , A`) * prob(A`) = 0 by A1,Th60;
hence thesis by A1,XCMPLX_1:6;
end;
theorem Th75:
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
proof
let E be finite non empty set, A,B be Event of E;
assume that
A1: 0 < prob(B) and
A2: A misses B;
prob(A , B) = 0 by A2,Th68;
then 1 - prob(A` , B) = 0 by A1,Th70;
hence thesis by XCMPLX_1:15;
end;
theorem Th76:
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))
proof
let E be finite non empty set, A,B be Event of E;
assume that
A1: 0 < prob(A) and
A2: prob(B) < 1 and
A3: A misses B;
A4: prob(B`) = 1 - prob(B) by Th48;
prob(B) - 1 < 1 - 1 by A2,REAL_1:54;
then - ( 1 - prob(B) ) < 0 by XCMPLX_1:143;
then 0 < - ( - ( 1 - prob(B) ) ) by REAL_1:66;
then A5: 0 < prob(B`) by Th48;
then prob(A) * prob(B` , A) = prob(B`) * prob(A , B`) by A1,Th69;
then prob(A) * 1 = prob(B`) * prob(A , B`) by A1,A3,Th75;
then prob(A) * (prob(B`))" = prob(A , B`) * ( prob(B`) * (prob(B`))" )
by XCMPLX_1:4;
then prob(A) * (prob(B`))" = prob(A , B`) * 1 by A5,XCMPLX_0:def 7;
hence thesis by A4,XCMPLX_0:def 9;
end;
theorem
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))
proof
let E be finite non empty set, A,B be Event of E;
assume that
A1: 0 < prob(A) and
A2: prob(B) < 1 and
A3: A misses B;
A4: prob(B`) = 1 - prob(B) by Th48;
prob(B) -1 < 1 - 1 by A2,REAL_1:54;
then - ( 1 - prob(B) ) < 0 by XCMPLX_1:143;
then 0 < - ( - ( 1 - prob(B) ) ) by REAL_1:66;
then prob(A` , B`) = 1 - prob(A , B`) by A4,Th70;
hence thesis by A1,A2,A3,Th76;
end;
theorem
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)
proof
let E be finite non empty set, A,B,C be Event of E;
assume that
A1: 0 < prob(B /\ C) and
A2: 0 < prob(C);
prob(A /\ B /\ C) = prob(A /\ (B /\ C)) by XBOOLE_1:16;
then A3: prob(A /\ B /\ C) = prob(A , B /\ C) * prob(B /\ C) by A1,Th60;
prob(B /\ C) = prob(B , C) * prob(C) by A2,Th60;
hence thesis by A3,XCMPLX_1:4;
end;
theorem Th79:
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`)
proof
let E be finite non empty set, A,B be Event of E;
assume that
A1: 0 < prob(B) and
A2: prob(B) < 1;
prob(B) -1 < 1 - 1 by A2,REAL_1:54;
then - ( 1 - prob(B) ) < 0 by XCMPLX_1:143;
then 0 < - ( - ( 1 - prob(B) ) ) by REAL_1:66;
then A3: 0 < prob(B`) by Th48;
prob(A) = prob(A /\ B) + prob(A /\ B`) by Th53;
then prob(A) = prob(A , B) * prob(B) + prob(A /\ B`) by A1,Th60;
hence thesis by A3,Th60;
end;
theorem Th80:
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)
proof
let E be finite non empty set, A,B1,B2 be Event of E;
assume that
A1: 0 < prob(B1) and
A2: 0 < prob(B2) and
A3: B1 \/ B2 = E and
A4: B1 misses B2;
B2 \ B1 = E \ B1 by A3,XBOOLE_1:40;
then A5: B2 = E \ B1 by A4,XBOOLE_1:83;
then A6: B2 = (B1)` by SUBSET_1:def 5;
0 < prob((B1)`) by A2,A5,SUBSET_1:def 5;
then 0 < 1 - prob(B1) by Th48;
then 1 - ( 1 - prob(B1) ) < 1 by SQUARE_1:29;
then 1 - 1 + prob(B1) < 1 by XCMPLX_1:37; hence thesis by A1,A6,Th79;
end;
theorem Th81:
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)
proof
let E be finite non empty set, A,B1,B2,B3 be Event of E;
assume that
A1: 0 < prob(B1) and
A2: 0 < prob(B2) and
A3: 0 < prob(B3) and
A4: B1 \/ B2 \/ B3 = E and
A5: B1 /\ B2 = {} and
A6: B1 /\ B3 = {} and
A7: B2 /\ B3 = {};
(B1 \/ B2 \/ B3) /\ A = A by A4,XBOOLE_1:28;
then A8: ((B1 \/ B2) /\ A) \/ (B3 /\ A) = A by XBOOLE_1:23;
(B1 /\ B3) \/ (B2 /\ B3) = B2 /\ B3 by A6;
then (B1 \/ B2) /\ B3 = {} by A7,XBOOLE_1:23;
then (B1 \/ B2) misses B3 by XBOOLE_0:def 7;
then (B1 \/ B2) /\ A misses B3 /\ A by XBOOLE_1:76;
then prob(A) = prob((B1 \/ B2) /\ A) + prob(B3 /\ A) by A8,Th47;
then A9: prob(A) = prob((B1 /\ A) \/ (B2 /\ A)) + prob(B3 /\ A) by XBOOLE_1:23;
B1 misses B2 by A5,XBOOLE_0:def 7;
then B1 /\ A misses B2 /\ A by XBOOLE_1:76;
then prob(A) = prob(A /\ B1) + prob(A /\ B2) + prob(A /\ B3) by A9,Th47;
then prob(A) = prob(A , B1) * prob(B1) + prob(A /\ B2) + prob(A /\ B3)
by A1,Th60;
then prob(A) = prob(A , B1) * prob(B1) + prob(A , B2) * prob(B2) +
prob(A /\ B3) by A2,Th60;
hence thesis by A3,Th60;
end;
theorem
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) )
proof
let E be finite non empty set, A,B1,B2 be Event of E;
assume that
A1: 0 < prob(B1) and
A2: 0 < prob(B2) and
A3: B1 \/ B2 = E and
A4: B1 misses B2;
A5: prob(A) = prob(A , B1) * prob(B1) + prob(A , B2) * prob(B2)
by A1,A2,A3,A4,Th80;
prob(B1 , A) = prob(A /\ B1) / prob(A) by Def5;
hence thesis by A1,A5,Th60;
end;
theorem
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) )
proof
let E be finite non empty set, A,B1,B2,B3 be Event of E;
assume that
A1: 0 < prob(B1) and
A2: 0 < prob(B2) and
A3: 0 < prob(B3) and
A4: B1 \/ B2 \/ B3 = E and
A5: B1 misses B2 and
A6: B1 misses B3 and
A7: B2 misses B3;
A8: prob(A) = ( prob(A , B1) * prob(B1) + prob(A , B2) * prob(B2) ) +
prob(A , B3) * prob(B3) by A1,A2,A3,A4,A5,A6,A7,Th81;
prob(B1 , A) = prob(A /\ B1) / prob(A) by Def5;
hence thesis by A1,A8,Th60;
end;
definition
let E be finite non empty set;
let A, B be Event of E;
pred A, B are_independent means :Def6:
prob(A /\ B) = prob(A) * prob(B);
symmetry;
end;
canceled 2;
theorem
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)
proof
let E be finite non empty set, A,B be Event of E;
assume that
A1: 0 < prob(B) and
A2: A , B are_independent;
prob(A /\ B) = prob(A) * prob(B) by A2,Def6;
then prob(A , B) = ( prob(A) * prob(B) ) / prob(B) by Def5;
then prob(A , B) = prob(A) * ( prob(B) / prob(B) ) by XCMPLX_1:75;
then prob(A , B) = prob(A) * 1 by A1,XCMPLX_1:60;
hence thesis;
end;
theorem
for E being finite non empty set, A,B being Event of E st
prob(B) = 0 holds A , B are_independent
proof
let E be finite non empty set, A,B be Event of E;
assume
A1: prob(B) = 0;
A /\ B c= B by XBOOLE_1:17;
then prob(A /\ B) <= 0 by A1,Th44;
then A2: prob(A /\ B) = 0 by Th43;
0 = prob(A) * 0;
hence thesis by A1,A2,Def6;
end;
theorem
for E being finite non empty set, A,B being Event of E st
A , B are_independent holds A` , B are_independent
proof
let E be finite non empty set, A,B be Event of E;
assume
A1: A , B are_independent;
prob(A` /\ B) = prob(B \ A) by SUBSET_1:32;
then prob(A` /\ B) = prob(B) - prob(A /\ B) by Th49;
then prob(A` /\ B) = 1 * prob(B) - prob(A) * prob(B) by A1,Def6;
then prob(A` /\ B) = ( 1 - prob(A) ) * prob(B) by XCMPLX_1:40;
then prob(A` /\ B) = prob(A`) * prob(B) by Th48;
hence thesis by Def6;
end;
theorem
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
proof
let E be finite non empty set, A,B be Event of E;
assume that
A1: A misses B and
A2: A , B are_independent;
prob(A /\ B) = 0 by A1,Th41;
then prob(A) * prob(B) = 0 by A2,Def6;
hence thesis by XCMPLX_1:6;
end;