:: Bertrand's Ballot Theorem
:: by Karol P\kak
::
:: Received June 13, 2014
:: Copyright (c) 2014-2021 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, SUBSET_1, FUNCT_1, NAT_1, TARSKI, FINSET_1, RELAT_1,
AFINSQ_1, ARYTM_1, ARYTM_3, FINSEQ_1, FINSEQ_2, XXREAL_0, CARD_1,
XBOOLE_0, ORDINAL4, CARD_3, FINSOP_1, FUNCOP_1, BINOP_2, REALSET1,
FUNCT_4, CARD_FIN, BALLOT_1, RPR_1, REAL_1, PRGCOR_2, CATALAN2, VALUED_0,
SETWISEO;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, RELAT_1,
FUNCT_1, XCMPLX_0, FINSET_1, XXREAL_0, AFINSQ_1, RELSET_1, FINSEQ_1,
FINSEQ_2, DOMAIN_1, FUNCT_2, FUNCT_4, FUNCOP_1, BINOP_2, AFINSQ_2,
NEWTON, XREAL_0, RPR_1, CARD_FIN, CATALAN2, VALUED_0, FINSEQOP, SETWOP_2,
RVSUM_1, NAT_D;
constructors PARTFUN3, BINOM, WELLORD2, SETWISEO, NAT_D, BINOP_2, RELSET_1,
AFINSQ_2, RPR_1, CARD_FIN, CATALAN2, FINSEQOP, FINSOP_1, RVSUM_1, NEWTON,
RFINSEQ;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FUNCT_4,
FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, BINOP_2, CARD_1, AFINSQ_1,
RELSET_1, VALUED_0, AFINSQ_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, RVSUM_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin :: Preliminaries
reserve D,D1,D2 for non empty set,
d,d1,d2 for XFinSequence of D,
n,k,i,j for Nat;
theorem :: BALLOT_1:1 ::: AFINSQ_2:84
XFS2FS (d|n) = (XFS2FS d) |n;
theorem :: BALLOT_1:2 ::: AFINSQ_1:97
rng d = rng (XFS2FS d);
theorem :: BALLOT_1:3
for d1 being XFinSequence of D1, d2 being XFinSequence of D2 st
d1 = d2 holds XFS2FS d1 = XFS2FS d2;
theorem :: BALLOT_1:4
XFS2FS d1 = XFS2FS d2 implies d1 = d2;
theorem :: BALLOT_1:5 ::: AFINSQ_2:85
for D being set
for d be FinSequence of D holds XFS2FS (FS2XFS d) = d;
theorem :: BALLOT_1:6
for f be FinSequence, x,y be object st rng f c= {x,y} & x<>y
holds card (f"{x}) + card (f"{y}) = len f;
theorem :: BALLOT_1:7
for f,g be Function st f is one-to-one
for x be object st x in dom f holds Coim(f*g,f.x) = Coim(g,x);
theorem :: BALLOT_1:8
for r be Real, f be real-valued FinSequence st rng f c= {0,r}
holds Sum f = r * card (f"{r});
begin :: Properties of Elections
reserve A,B for object,
v for Element of (n+k)-tuples_on {A,B},
f,g for FinSequence;
definition
let A,n,B,k;
func Election(A,n,B,k) -> Subset of (n+k)-tuples_on {A,B} means
:: BALLOT_1:def 1
v in it iff card (v"{A}) = n;
end;
registration
let A,n,B,k;
cluster Election(A,n,B,k) -> finite;
end;
theorem :: BALLOT_1:9
Election(A,n,A,0) = {n|-> A};
theorem :: BALLOT_1:10
k>0 implies Election(A,n,A,k) is empty;
registration let A,n; let k be non empty Nat;
cluster Election(A,n,A,k) -> empty;
end;
theorem :: BALLOT_1:11
Election(A,n,B,k) = Choose(Seg (n+k),n,A,B);
theorem :: BALLOT_1:12
A <> B implies (v in Election(A,n,B,k) iff card (v"{B}) = k);
theorem :: BALLOT_1:13
A <> B implies card Election(A,n,B,k) = (n+k) choose n;
begin :: Properties of Ballot Elections
definition
let A,n,B,k;
let v be FinSequence;
attr v is A,n,B,k-dominated-election means
:: BALLOT_1:def 2
v in Election(A,n,B,k) &
for i st i >0 holds card ((v|i)"{A}) > card ((v|i)"{B});
end;
theorem :: BALLOT_1:14
f is A,n,B,k-dominated-election implies A <> B;
theorem :: BALLOT_1:15
f is A,n,B,k-dominated-election implies n > k;
theorem :: BALLOT_1:16
A <> B & n > 0 implies n|->A is A,n,B,0-dominated-election;
theorem :: BALLOT_1:17
f is A,n,B,k-dominated-election & i < n-k
implies f^(i|->B) is A,n,B,k+i-dominated-election;
theorem :: BALLOT_1:18
f is A,n,B,k-dominated-election & g is A,i,B,j-dominated-election implies
f^g is A,n+i,B,k+j-dominated-election;
definition
let A,n,B,k;
func DominatedElection(A,n,B,k) -> Subset of Election(A,n,B,k) means
:: BALLOT_1:def 3
f in it iff f is A,n,B,k-dominated-election;
end;
theorem :: BALLOT_1:19
A = B or n <= k implies DominatedElection(A,n,B,k) is empty;
theorem :: BALLOT_1:20
n > k & A <> B implies (n|->A)^(k|->B) in DominatedElection(A,n,B,k);
theorem :: BALLOT_1:21
A <> B implies
card DominatedElection(A,n,B,k) = card DominatedElection(0,n,1,k);
theorem :: BALLOT_1:22
for p being FinSequence of NAT holds
p is 0,n,1,k-dominated-election iff
p is Tuple of n+k,{0,1} & n>0 & Sum p = k &
for i st i >0 holds 2* Sum (p|i) < i;
theorem :: BALLOT_1:23
f is A,n,B,k-dominated-election implies f.1 = A;
theorem :: BALLOT_1:24
for d be XFinSequence of NAT holds
d in Domin_0(n+k,k) iff <*0*>^(XFS2FS d) in DominatedElection(0,n+1,1,k);
theorem :: BALLOT_1:25
card Domin_0(n+k,k) = card DominatedElection(0,n+1,1,k);
theorem :: BALLOT_1:26
card Domin_0(n+k,k) = card DominatedElection(0,n+1,1,k);
theorem :: BALLOT_1:27
A <> B & n > k implies
card DominatedElection(A,n,B,k) = ((n-k) / (n+k)) * ((n+k) choose k);
begin :: Main Theorem
::$N Bertrand's Ballot Theorem
theorem :: BALLOT_1:28
A <> B & n >= k implies prob DominatedElection(A,n,B,k) = (n-k) / (n+k);