:: 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);