:: Bertrand's Ballot Theorem
:: by Karol P\kak
::
:: Received June 13, 2014
:: Copyright (c) 2014-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, 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;
definitions TARSKI, XBOOLE_0, FUNCT_1;
equalities FUNCOP_1, RELAT_1, ORDINAL1, FINSEQ_1, FINSEQ_2;
expansions TARSKI, XBOOLE_0, FUNCT_1, FINSEQ_1, CATALAN2;
theorems AFINSQ_1, TARSKI, FUNCT_1, XBOOLE_0, ZFMISC_1, RELAT_1, XBOOLE_1,
NAT_1, FUNCT_2, XCMPLX_1, CARD_2, WELLORD2, ENUMSET1, CARD_1, NEWTON,
XREAL_1, FUNCOP_1, FUNCT_4, XXREAL_0, NAT_D, XREAL_0, AFINSQ_2, ORDINAL1,
RPR_1, FINSEQ_1, FINSEQ_2, FINSEQ_5, RVSUM_1, FINSEQ_3, FINSEQ_6,
NECKLACE, CARD_FIN, CATALAN2;
schemes FUNCT_2, NAT_1;
begin :: Preliminaries
reserve D,D1,D2 for non empty set,
d,d1,d2 for XFinSequence of D,
n,k,i,j for Nat;
theorem Th1: ::: AFINSQ_2:84
XFS2FS (d|n) = (XFS2FS d) |n by AFINSQ_2:84;
theorem Th2: ::: AFINSQ_1:97
rng d = rng (XFS2FS d) by AFINSQ_1:97;
theorem
for d1 being XFinSequence of D1, d2 being XFinSequence of D2 st
d1 = d2 holds XFS2FS d1 = XFS2FS d2;
theorem Th4:
XFS2FS d1 = XFS2FS d2 implies d1 = d2
proof
assume
A1: XFS2FS d1 = XFS2FS d2;
set Xd1=XFS2FS d1,Xd2=XFS2FS d2;
A2: len Xd1 = len d1 by AFINSQ_1:def 9;
A3: len Xd2=len d2 by AFINSQ_1:def 9;
for i st i < len d1 holds d1.i = d2.i
proof
let i such that
A4: i < len d1;
A5: i+1 <= len d1 by A4,NAT_1:13;
A6: i+1-1=i;
then d1.i = Xd1.(i+1) by NAT_1:11,A5,AFINSQ_1:def 9;
hence thesis by A6,NAT_1:11,A5,A2,A3,A1,AFINSQ_1:def 9;
end;
hence thesis by A2,A3,A1,AFINSQ_1:9;
end;
theorem ::: AFINSQ_2:85
for D being set
for d be FinSequence of D holds XFS2FS (FS2XFS d) = d;
theorem Th6:
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
proof
let f be FinSequence, A,B be object;
A1:{A}\/{B}={A,B} by ENUMSET1:1;
assume that
A2: rng f c= {A,B}
and
A3: A<>B;
f"rng f c= f"{A,B} by A2,RELAT_1:143;
then
A4: dom f = f"{A,B} by RELAT_1:132,RELAT_1:134
.= (f"{A})\/(f"{B}) by RELAT_1:140,A1;
f"{A} misses f"{B}
proof
assume f"{A} meets f"{B};
then consider x be object such that
A5: x in f"{A} and
A6: x in f"{B} by XBOOLE_0:3;
A7: f.x in {A} by A5,FUNCT_1:def 7;
A8: f.x in {B} by A6,FUNCT_1:def 7;
f.x = A by A7,TARSKI:def 1;
hence thesis by A8,TARSKI:def 1,A3;
end;
hence card (f"{A}) + card (f"{B})= card dom f by A4,CARD_2:40
.= card Seg len f by FINSEQ_1:def 3
.= len f by FINSEQ_1:57;
end;
theorem Th7:
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)
proof
let f,g be Function such that
A1: f is one-to-one;
let x be object such that
A2: x in dom f;
set fg=f*g;
thus Coim(fg,f.x) c= Coim(g,x)
proof
let z be object;
assume
A3: z in Coim(fg,f.x);
then
A4: z in dom fg by FUNCT_1:def 7;
A5: fg.z in {f.x} by A3,FUNCT_1:def 7;
A6: z in dom g by A4,FUNCT_1:11;
A7: g.z in dom f by A4,FUNCT_1:11;
A8: fg.z=f.(g.z) by A4,FUNCT_1:12;
fg.z=f.x by A5,TARSKI:def 1;
then g.z=x by A7,A8,A2,A1;
then g.z in {x} by TARSKI:def 1;
hence thesis by FUNCT_1:def 7,A6;
end;
let z be object;
assume
A9: z in Coim(g,x);
then
A10: z in dom g by FUNCT_1:def 7;
g.z in {x} by A9,FUNCT_1:def 7;
then
A11: g.z=x by TARSKI:def 1;
then
A12: fg.z=f.x by FUNCT_1:13,A10;
A13: z in dom fg by A11,A2,FUNCT_1:11,A10;
f.x in {f.x} by TARSKI:def 1;
hence thesis by A12,A13,FUNCT_1:def 7;
end;
theorem Th21:
for r be Real, f be real-valued FinSequence st rng f c= {0,r}
holds Sum f = r * card (f"{r})
proof
let r be Real;
defpred P[Nat] means for f be real-valued FinSequence st
len f = $1 & rng f c= {0,r} holds Sum f = r* card (f"{r});
A1:P[0]
proof
let f be real-valued FinSequence such that
A2: len f = 0 and
rng f c= {0,r};
A3: f={} by A2;
then f"{r}={};
hence thesis by A3,RVSUM_1:72;
end;
A4:for n st P[n] holds P[n+1]
proof
let n such that
A5: P[n];
set n1=n+1;
let f be real-valued FinSequence such that
A6: len f = n1
and
A7: rng f c= {0,r};
rng f c= REAL;
then reconsider F=f as FinSequence of REAL by FINSEQ_1:def 4;
set fn=F|n,FF=<*f.n1*>;
A8: f = fn^FF by A6,FINSEQ_3:55;
then
A9: Sum f = Sum fn + (F.n1) by RVSUM_1:74;
rng fn c= rng f by RELAT_1:70;
then
A10: rng fn c= {0,r} by A7;
A11: len fn = n by NAT_1:11,A6,FINSEQ_1:59;
then
A12: Sum fn = r*card (fn"{r}) by A10,A5;
A13: dom FF = Seg 1 by FINSEQ_1:38;
rng FF = {F.n1} by FINSEQ_1:38;
then
A14: FF = Seg 1 --> F.n1 by A13,FUNCOP_1:9;
A15: card (f"{r}) = card (fn"{r}) + card (FF"{r}) by FINSEQ_3:57,A8;
1 <= n1 by NAT_1:11;
then n1 in dom F by A6,FINSEQ_3:25;
then
A16: F.n1 in rng F by FUNCT_1:def 3;
per cases;
suppose
A17: F.n1 <> r;
then not F.n1 in {r} by TARSKI:def 1;
then
A18: FF"{r}={} by A14,FUNCOP_1:16;
F.n1 = 0 by A17,A16,A7,TARSKI:def 2;
hence thesis by A11,A10,A5,A9,A15,A18;
end;
suppose
A19: F.n1 = r;
then FF"{r}=Seg 1 by A14,FUNCOP_1:15;
then card (FF"{r}) = 1 by FINSEQ_1:57;
hence thesis by A12,A9,A15,A19;
end;
end;
A20: for n holds P[n] from NAT_1:sch 2(A1,A4);
let f be real-valued FinSequence;
P[len f] by A20;
hence thesis;
end;
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 :Def1:
v in it iff card (v"{A}) = n;
existence
proof
set V={v: card (v"{A}) = n};
V c= (n+k)-tuples_on {A,B}
proof
let x be object;
assume x in V;
then ex v st v=x & card (v"{A}) = n;
hence thesis;
end;
then reconsider V as Subset of (n+k)-tuples_on {A,B};
take V;
let v;
hereby assume v in V;
then ex v1 be Element of (n+k)-tuples_on {A,B} st
v=v1 & card (v1"{A}) = n;
hence card (v"{A}) = n;
end;
thus thesis;
end;
uniqueness
proof
let V1,V2 be Subset of (n+k)-tuples_on {A,B};
assume that
A1: v in V1 iff card (v"{A}) = n and
A2: v in V2 iff card (v"{A}) = n;
hereby let x be object;
assume
A3: x in V1;
then reconsider v=x as Element of (n+k)-tuples_on {A,B};
card (v"{A})=n by A1,A3;
hence x in V2 by A2;
end;
let x be object;
assume
A4: x in V2;
then reconsider v=x as Element of (n+k)-tuples_on {A,B};
card (v"{A})=n by A2,A4;
hence x in V1 by A1;
end;
end;
registration
let A,n,B,k;
cluster Election(A,n,B,k) -> finite;
coherence;
end;
theorem
Election(A,n,A,0) = {n|-> A}
proof
A1: {A,A}={A} by ENUMSET1:29;
thus Election(A,n,A,0) c= {n|-> A}
proof
let x be object;
assume
A2: x in Election(A,n,A,0);
then reconsider v=x as Element of (n+0)-tuples_on {A} by ENUMSET1:29;
A3: card (v"{A})=n by A2,Def1;
A4: len v =n by CARD_1:def 7;
per cases;
suppose rng v={};
then v = {}-->{A};
then v = n|->A by A3;
hence thesis by TARSKI:def 1;
end;
suppose rng v <>{};
then v = (dom v)--> A by ZFMISC_1:33,FUNCOP_1:9;
then v = n|->A by A4,FINSEQ_1:def 3;
hence thesis by TARSKI:def 1;
end;
end;
A in {A} by TARSKI:def 1;
then reconsider nA=n|->A as Element of n-tuples_on {A,A} by A1,FINSEQ_2:112;
nA"{A} = Seg n by FUNCOP_1:15;
then card (nA"{A})=n by FINSEQ_1:57;
then nA in Election(A,n,A,0) by Def1;
hence thesis by ZFMISC_1:31;
end;
theorem ElectionEmpty:
k>0 implies Election(A,n,A,k) is empty
proof
assume
A1: k>0;
assume Election(A,n,A,k) is non empty;
then consider v be object such that
A2: v in Election(A,n,A,k);
reconsider v as Element of (n+k)-tuples_on {A} by A2,ENUMSET1:29;
A3: card dom v =(n+k) by CARD_1:def 7;
v"(rng v) c= v"{A} by RELAT_1:143;
then v"{A} = dom v by RELAT_1:134,132;
then n+k = n by A3,Def1,A2;
hence contradiction by A1;
end;
registration let A,n; let k be non empty Nat;
cluster Election(A,n,A,k) -> empty;
coherence
proof
k > 0;
hence thesis by ElectionEmpty;
end;
end;
theorem Th10:
Election(A,n,B,k) = Choose(Seg (n+k),n,A,B)
proof
thus Election(A,n,B,k) c= Choose(Seg (n+k),n,A,B)
proof
let x be object;
assume
A1: x in Election(A,n,B,k);
then reconsider v=x as Element of (n+k)-tuples_on {A,B};
A2: rng v c= {A,B};
len v = n+k by CARD_1:def 7;
then dom v = Seg (n+k) by FINSEQ_1:def 3;
then reconsider V=v as Function of Seg (n+k),{A,B} by FUNCT_2:2,A2;
card (v"{A}) = n by A1,Def1;
then V in Choose(Seg (n+k),n,A,B) by CARD_FIN:def 1;
hence thesis;
end;
let x be object;
assume x in Choose(Seg (n+k),n,A,B);
then consider f be Function of Seg (n+k),{A,B} such that
A3: f = x and
A4: card (f"{A})=n by CARD_FIN:def 1;
A5: rng f c= {A,B};
A6: dom f = Seg (n+k) by FUNCT_2:def 1;
then reconsider f as FinSequence by FINSEQ_1:def 2;
reconsider f as FinSequence of {A,B} by A5,FINSEQ_1:def 4;
n+k in NAT by ORDINAL1:def 12;
then len f = n+k by FINSEQ_1:def 3,A6;
then f is Element of (n+k)-tuples_on {A,B} by FINSEQ_2:92;
hence x in Election(A,n,B,k) by A3,A4,Def1;
end;
theorem Th11:
A <> B implies (v in Election(A,n,B,k) iff card (v"{B}) = k)
proof
assume
A1: A<>B;
A2: rng v c= {A,B};
A3: len v = n+k by CARD_1:def 7;
A4: card (v"{A}) + card (v"{B}) = len v by Th6,A2,A1;
thus v in Election(A,n,B,k) implies card (v"{B}) = k
proof
assume v in Election(A,n,B,k);
then card (v"{A})=n by Def1;
hence thesis by A4,A3;
end;
assume card (v"{B}) = k;
hence v in Election(A,n,B,k) by A4,A3,Def1;
end;
theorem Th12:
A <> B implies card Election(A,n,B,k) = (n+k) choose n
proof
assume
A1: A<>B;
thus card Election(A,n,B,k) = card Choose(Seg (n+k),n,A,B) by Th10
.= card Seg (n+k) choose n by A1,CARD_FIN:16
.= (n+k) choose n by FINSEQ_1:57;
end;
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
v in Election(A,n,B,k) &
for i st i >0 holds card ((v|i)"{A}) > card ((v|i)"{B});
end;
theorem Th13:
f is A,n,B,k-dominated-election implies A <> B
proof
assume
A1: f is A,n,B,k-dominated-election;
then reconsider f as Element of (n+k)-tuples_on {A,B};
len f+1 >= len f by NAT_1:13;
then f| (len f+1 ) = f by FINSEQ_1:58;
then card (f"{A}) > card (f"{B}) by A1;
hence thesis;
end;
theorem Th14:
f is A,n,B,k-dominated-election implies n > k
proof
assume
A1: f is A,n,B,k-dominated-election;
then reconsider f as Element of (n+k)-tuples_on {A,B};
len f+1 >= len f by NAT_1:13;
then
A2: f| (len f+1) = f by FINSEQ_1:58;
A3: A<>B by A1,Th13;
A4: card (f"{A}) = n by A1,Def1;
card (f"{B}) = k by A1,A3,Th11;
hence thesis by A2,A1,A4;
end;
theorem Th15:
A <> B & n > 0 implies n|->A is A,n,B,0-dominated-election
proof
set nA=n|->A;
assume that
A1: A<>B and
A2: n>0;
A is Element of {A,B} by TARSKI:def 2;
then reconsider nA as Element of (n+0)-tuples_on {A,B} by FINSEQ_2:112;
nA"rng nA c= nA"{A} by FUNCOP_1:13,RELAT_1:143;
then dom nA = nA"{A} by RELAT_1:132, RELAT_1:134;
then card (nA"{A}) = card Seg len nA by FINSEQ_1:def 3
.= len nA by FINSEQ_1:57
.= n by CARD_1:def 7;
hence n|->A in Election(A,n,B,0) by Def1;
let i such that
A3: i>0;
set nAi=nA|i;
A4: nAi = (Seg n /\ Seg i)-->A by FUNCOP_1:12;
A5: not A in {B} by A1,TARSKI:def 1;
per cases;
suppose i<= n;
then (Seg i) /\(Seg n) = Seg i by FINSEQ_1:5,XBOOLE_1:28;
then
A6: nAi"{A} = Seg i by A4,FUNCOP_1:15;
nAi"{B} = {} by A5,FUNCOP_1:16,A4;
hence thesis by A6,A3;
end;
suppose i > n;
then (Seg i) /\(Seg n) = Seg n by FINSEQ_1:5,XBOOLE_1:28;
then
A7: nAi"{A} = Seg n by A4,FUNCOP_1:15;
nAi"{B} = {} by A5,FUNCOP_1:16,A4;
hence thesis by A2,A7;
end;
end;
theorem Th16:
f is A,n,B,k-dominated-election & i < n-k
implies f^(i|->B) is A,n,B,k+i-dominated-election
proof
set iB=i|->B;
assume that
A1: f is A,n,B,k-dominated-election
and
A2: i < n-k;
A3:A<>B by A1,Th13;
A4:rng iB c= {B} by FUNCOP_1:13;
{B} c= {A,B} by ZFMISC_1:7;
then rng iB c= {A,B} by A4;
then reconsider iB as FinSequence of {A,B} by FINSEQ_1:def 4;
reconsider F=f as Element of (n+k)-tuples_on {A,B} by A1;
set fB=f^(i|->B);
A5:len f = n+k by A1,CARD_1:def 7;
A6:len (F^iB) = n+k+i by CARD_1:def 7;
then reconsider FB=F^iB as Element of (n+(k+i))-tuples_on {A,B}
by FINSEQ_2:92;
A7:not B in {A} by A3,TARSKI:def 1;
then
A8:iB"{A} = {} by FUNCOP_1:16;
A9:card (FB"{A}) = card (F"{A})+card (iB"{A}) by FINSEQ_3:57;
A10:card (F"{A}) = n by Def1,A1;
hence fB in Election(A,n,B,k+i) by A9,A8,Def1;
let j such that
A11: j>0;
set FBj=FB|j;
A12:card (f"{B}) = k by A3,Th11,A1;
A13:i+k < n-k+k by A2,XREAL_1:6;
per cases;
suppose j <= n+k;
then FBj = f|j by A5,FINSEQ_5:22;
hence card ((fB|j)"{A}) > card ((fB|j)"{B}) by A11,A1;
end;
suppose
A14: j > n+k & j <= n+k+i;
then reconsider j1=j-(n+k) as Nat by NAT_1:21;
A15: j1+(n+k)<= i+(n+k) by A14;
then
A16: j1 <=i by XREAL_1:6;
Seg i/\Seg j1=Seg j1 by A15,XREAL_1:6,FINSEQ_1:7;
then
A17: iB|Seg j1 = Seg j1 --> B by FUNCOP_1:12;
A18: (Seg j1 --> B) "{A} = {} by A7,FUNCOP_1:16;
A19: FBj = FB| Seg (len F +j1) by A5
.= F^(Seg j1 --> B) by A17,FINSEQ_6:14;
then
A20: card (FBj"{A}) = n + card ((Seg j1 --> B) "{A}) by A10,FINSEQ_3:57
.= n by A18;
B in {B} by TARSKI:def 1;
then (Seg j1 --> B) "{B} = Seg j1 by FUNCOP_1:14;
then card (FBj"{B}) = k + card Seg j1 by A12,A19,FINSEQ_3:57
.= k+ j1 by FINSEQ_1:57;
then card (FBj"{B}) <= k+ i by A16,XREAL_1:6;
hence card ((fB|j)"{A}) > card ((fB|j)"{B}) by A20,A13,XXREAL_0:2;
end;
suppose j > n+k+i;
then
A21: FB|j=FB by FINSEQ_1:58,A6;
A22: iB "{A} = {} by A7,FUNCOP_1:16;
B in {B} by TARSKI:def 1;
then iB "{B} = Seg i by FUNCOP_1:14;
then card (FB"{B}) = k+card Seg i by A12,FINSEQ_3:57
.= k+i by FINSEQ_1:57;
hence card ((fB|j)"{A}) > card ((fB|j)"{B}) by A21,A22,A9,Def1,A1,A13;
end;
end;
theorem
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
proof
assume that
A1: f is A,n,B,k-dominated-election
and
A2: g is A,i,B,j-dominated-election;
A3: A<>B by A1,Th13;
reconsider F=f as Element of (n+k)-tuples_on {A,B} by A1;
reconsider G=g as Element of (i+j)-tuples_on {A,B} by A2;
A4: len F = n+k by CARD_1:def 7;
A5: len (F^G) = (n+k)+(i+j) by CARD_1:def 7;
then reconsider FG=F^G as Element of ((n+k)+(i+j))-tuples_on {A,B}
by FINSEQ_2:92;
card (FG"{A}) = card (F"{A}) + card (G"{A}) by FINSEQ_3:57
.= n + card (G"{A}) by A1,Def1
.= n + i by A2,Def1;
hence f^g in Election(A,n+i,B,k+j) by Def1;
let h be Nat such that
A6: h>0;
per cases;
suppose h <= n+k;
then FG|h = F|h by A4,FINSEQ_5:22;
hence thesis by A1,A6;
end;
suppose
A7: h > n+k & h <= n+k+i+j;
then reconsider h1=h-(n+k) as Nat by NAT_1:21;
A8: h1 <>0 by A7;
h1+len F = h by A4;
then
A9: FG| h = F^(G|h1) by FINSEQ_6:14;
then
A10: card ((FG|h)"{A}) = card (F"{A}) + card ((G|h1)"{A}) by FINSEQ_3:57
.= n+card ((G|h1)"{A}) by A1,Def1;
A11: card ((FG|h)"{B}) = card (F"{B}) + card ((G|h1)"{B}) by A9,FINSEQ_3:57
.= k+card ((G|h1)"{B}) by A3,A1,Th11;
card ((G|h1)"{A}) > card ((G|h1)"{B}) by A8,A2;
hence thesis by A10,A11,Th14,A1,XREAL_1:8;
end;
suppose h > n+k+i+j;
then
A12: FG|h=FG by FINSEQ_1:58,A5;
A13: card (FG"{A}) = card (F"{A}) +card (G"{A}) by FINSEQ_3:57
.= n+ card (G"{A}) by A1,Def1
.= n+i by A2,Def1;
A14: card (FG"{B}) = card (F"{B}) +card (G"{B}) by FINSEQ_3:57
.= k+card (G"{B}) by A3,A1,Th11
.= k+j by A3,A2,Th11;
n > k by Th14,A1;
hence thesis by Th14,A2,A13,A14,XREAL_1:8,A12;
end;
end;
definition
let A,n,B,k;
func DominatedElection(A,n,B,k) -> Subset of Election(A,n,B,k) means :Def3:
f in it iff f is A,n,B,k-dominated-election;
existence
proof
set BALL={v:v is A,n,B,k-dominated-election};
BALL c= Election(A,n,B,k)
proof
let x be object;
assume x in BALL;
then ex v st x=v & v is A,n,B,k-dominated-election;
hence thesis;
end;
then reconsider BALL as Subset of Election(A,n,B,k);
take BALL;
let f;
f in BALL implies f is A,n,B,k-dominated-election
proof
assume f in BALL;
then ex v st f=v & v is A,n,B,k-dominated-election;
hence thesis;
end;
hence thesis;
end;
uniqueness
proof
let B1,B2 be Subset of Election(A,n,B,k) such that
A1: f in B1 iff f is A,n,B,k-dominated-election and
A2: f in B2 iff f is A,n,B,k-dominated-election;
thus B1 c= B2 by A1,A2;
let x be object;
thus thesis by A2,A1;
end;
end;
theorem Th18:
A = B or n <= k implies DominatedElection(A,n,B,k) is empty
proof
assume A1:A=B or n <=k;
assume DominatedElection(A,n,B,k) is non empty;
then consider f be object such that
A2: f in DominatedElection(A,n,B,k);
f in Election(A,n,B,k) by A2;
then reconsider f as Element of (n+k)-tuples_on {A,B};
f is A,n,B,k-dominated-election by A2,Def3;
hence thesis by Th13,Th14,A1;
end;
theorem
n > k & A <> B implies (n|->A)^(k|->B) in DominatedElection(A,n,B,k)
proof
assume that
A1: n >k and
A2: A<>B;
k < n-0 by A1;
then (n|->A)^(k|->B) is A,n,B,0+k-dominated-election by Th16,A2,Th15;
hence thesis by Def3;
end;
theorem Th20:
A <> B implies
card DominatedElection(A,n,B,k) = card DominatedElection(0,n,1,k)
proof
assume A1:A<>B;
set T=(A,B)-->(0,1),W=(0,1)-->(A,B);
A2: dom T = {A,B} by FUNCT_4:62;
A3: rng T = {0,1} by A1,FUNCT_4:64;
A4: rng W={A,B} by FUNCT_4:64;
A5: dom W = {0,1} by FUNCT_4:62;
A6: A is set by TARSKI:1;
A7: B is set by TARSKI:1;
A8: rng (A.-->0) = {0} by A6,FUNCOP_1:88;
A9: rng (B.-->1) = {1} by A7,FUNCOP_1:88;
A10: rng (0.-->A) = {A} by A6,FUNCOP_1:88;
A11: rng (1.-->B) = {B} by A7,FUNCOP_1:88;
A12: (A.-->0) +* (B.-->1) is one-to-one by A8,A9,ZFMISC_1:11,FUNCT_4:92;
A13: (0.-->A) +* (1.-->B) is one-to-one by A10,A11,A1,ZFMISC_1:11,FUNCT_4:92;
A14: T is one-to-one by A12,FUNCT_4:def 4;
A15: W is one-to-one by A13,FUNCT_4:def 4;
A16: T.A=0 by A1,FUNCT_4:63;
A17: T.B=1 by FUNCT_4:63;
A18: W.0=A by FUNCT_4:63;
A19: W.1=B by FUNCT_4:63;
defpred P[object,object] means for f st f=$1 holds T*f=$2;
A20:for x be object st x in DominatedElection(A,n,B,k)
ex y be object st y in DominatedElection(0,n,1,k) & P[x,y]
proof
let x be object such that
A21: x in DominatedElection(A,n,B,k);
x in Election(A,n,B,k) by A21;
then reconsider f=x as Element of (n+k)-tuples_on {A,B};
A22: len f = n+k by CARD_1:def 7;
A23: dom f = Seg len f by FINSEQ_1:def 3;
rng f c= {A,B};
then
A24: dom (T*f)=Seg len f by A23,A2,RELAT_1:27;
A25: rng (T*f) c= {0,1} by A3,RELAT_1:26;
reconsider Tf=T*f as FinSequence;
reconsider Tf as FinSequence of {0,1} by A25,FINSEQ_1:def 4;
len Tf = len f by A24,FINSEQ_1:def 3;
then reconsider Tf as Element of (n+k)-tuples_on {0,1} by A22,FINSEQ_2:92;
take Tf;
Tf is 0,n,1,k-dominated-election
proof
A26: A in dom T by A2,TARSKI:def 2;
A27: B in dom T by A2,TARSKI:def 2;
Coim(Tf,0)=Coim(f,A) by A26,Th7,A14,A16;
then card Coim(Tf,0) = n by A21,Def1;
hence Tf in Election(0,n,1,k) by Def1;
let i such that
A28: i>0;
A29: Tf|i = T*(f|i) by RELAT_1:83;
then
A30: Coim(Tf|i,0)=Coim(f|i,A) by A26,Th7,A14,A16;
A31: Coim(Tf|i,1)=Coim(f|i,B) by A29,A27,Th7,A14,A17;
f is A,n,B,k-dominated-election by A21,Def3;
hence thesis by A28,A30,A31;
end;
hence thesis by Def3;
end;
consider C be Function of DominatedElection(A,n,B,k),
DominatedElection(0,n,1,k) such that
A32:for x being object st x in DominatedElection(A,n,B,k) holds P[x,C.x]
from FUNCT_2:sch 1(A20);
DominatedElection(0,n,1,k) c= rng C
proof
let x be object;
assume
A33:x in DominatedElection(0,n,1,k);
then x in Election(0,n,1,k);
then reconsider f=x as Element of (n+k)-tuples_on {0,1};
A34: len f = n+k by CARD_1:def 7;
A35: dom f = Seg len f by FINSEQ_1:def 3;
A36: rng f c= {0,1};
then
A37: dom (W*f)=Seg len f by A35,A5,RELAT_1:27;
A38: rng (W*f) c= {A,B} by A4,RELAT_1:26;
reconsider Wf=W*f as FinSequence by A37,FINSEQ_1:def 2;
reconsider Wf as FinSequence of {A,B} by A38,FINSEQ_1:def 4;
len Wf = len f by A37,FINSEQ_1:def 3;
then reconsider Wf as Element of (n+k)-tuples_on {A,B} by A34,FINSEQ_2:92;
Wf is A,n,B,k-dominated-election
proof
A39: 0 in dom W by A5,TARSKI:def 2;
A40: 1 in dom W by A5,TARSKI:def 2;
Coim(Wf,A)=Coim(f,0) by A39,Th7,A15,A18;
then card Coim(Wf,A)= n by A33,Def1;
hence Wf in Election(A,n,B,k) by Def1;
let i such that
A41: i>0;
A42: Wf|i = W*(f|i) by RELAT_1:83;
then
A43: Coim(Wf|i,A)=Coim(f|i,0) by A39,Th7,A15,A18;
A44: Coim(Wf|i,B)=Coim(f|i,1) by A42,A40,Th7,A15,A19;
f is 0,n,1,k-dominated-election by A33,Def3;
hence thesis by A41,A43,A44;
end;
then
A45: Wf in DominatedElection(A,n,B,k) by Def3;
then
A46: Wf in dom C by FUNCT_2:def 1,A33;
C.Wf = T*Wf by A45,A32
.= W"*(W*f) by A6,A7,A1,NECKLACE:10
.= (W"*W)*f by RELAT_1:36
.= (id {0,1}) * f by A15,A5,FUNCT_1:39
.= f by RELAT_1:53,A36;
hence thesis by A46,FUNCT_1:def 3;
end;
then
A47: DominatedElection(0,n,1,k) = rng C;
per cases;
suppose
A48: DominatedElection(0,n,1,k)={};
DominatedElection(A,n,B,k)={}
proof
assume DominatedElection(A,n,B,k) <>{};
then consider x be object such that
A49: x in DominatedElection(A,n,B,k) by XBOOLE_0:def 1;
ex y be object st y in DominatedElection(0,n,1,k) & P[x,y] by A20,A49;
hence thesis by A48;
end;
hence thesis by A48;
end;
suppose DominatedElection(0,n,1,k)<>{};
then
A50: dom C = DominatedElection(A,n,B,k) by FUNCT_2:def 1;
C is one-to-one
proof
let x1,x2 be object such that
A51: x1 in dom C
and
A52: x2 in dom C
and
A53: C.x1=C.x2;
A54: x1 in Election(A,n,B,k) by A50,A51;
x2 in Election(A,n,B,k) by A50,A52;
then reconsider x1,x2 as Element of (n+k) -tuples_on {A,B} by A54;
A55: len x1 = n+k by CARD_1:def 7;
A56: len x2 = n+k by CARD_1:def 7;
A57: dom x1 = Seg (n+k) by A55,FINSEQ_1:def 3;
A58: dom x2 = Seg (n+k) by A56,FINSEQ_1:def 3;
A59: rng x1 c= dom T by A2;
A60: rng x2 c= dom T by A2;
A61: T is one-to-one by A12,FUNCT_4:def 4;
A62: C.x1 = T*x1 by A51,A32;
C.x2 = T*x2 by A52,A32;
hence thesis by A62,A57,A58,A59,A60,A61,A53,FUNCT_1:27;
end;
hence thesis by WELLORD2:def 4,A47,A50,CARD_1:5;
end;
end;
theorem Th22:
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
proof
let p be FinSequence of NAT;
thus p is 0,n,1,k-dominated-election implies
p is Tuple of n+k,{0,1} & n>0 & Sum p = k &
for i st i >0 holds 2* Sum (p|i) < i
proof
assume
A1: p is 0,n,1,k-dominated-election;
then reconsider P=p as Element of (n+k)-tuples_on {0,1};
A2: rng P c= {0,1};
then Sum p = 1 * card (p"{1}) by Th21;
hence p is Tuple of n+k,{0,1} & n > 0 & Sum p = k by A2,A1,Th11,Th14;
let i such that
A3: i>0;
rng (p|i) c= rng p by RELAT_1:70;
then
A4: rng (p|i) c= {0,1} by A2;
then
A5: 1*card ((p|i)"{1}) = Sum (p|i) by Th21;
card ((p|i)"{1}) + card ((p|i)"{0}) = len (p|i) by A4,Th6;
then len (p|i) - Sum (p|i) > Sum (p|i) by A1,A3,A5;
then
A6: len (p|i) > Sum (p|i)+Sum (p|i) by XREAL_1:20;
per cases;
suppose
A7: i > len p;
then p|i=p by FINSEQ_1:58;
hence thesis by A6,A7,XXREAL_0:2;
end;
suppose i <=len p;
hence thesis by FINSEQ_1:59,A6;
end;
end;
assume that
A8: p is Tuple of n+k,{0,1}
and
A9: n>0
and
A10: Sum p = k
and
A11: for i st i >0 holds 2* Sum (p|i) < i;
A12: rng p c= {0,1} by A8, FINSEQ_1:def 4;
A13: len p = n+k by A8,CARD_1:def 7;
A14: 1*card (p"{1}) = k by A12,Th21,A10;
reconsider P=p as Element of (n+k)-tuples_on {0,1} by A8,FINSEQ_2:92,A13;
A15: card (p"{1})+ card (p"{0}) = len p by A12,Th6;
then card (P"{0}) = n by A14,A13;
hence p in Election(0,n,1,k) by Def1;
let i such that
A16: i>0;
rng (p|i) c= rng p by RELAT_1:70;
then
A17: rng (p|i) c= {0,1} by A12;
then
A18: 1*card ((p|i)"{1}) = Sum (p|i) by Th21;
A19: 2* Sum (p|i) < i by A16,A11;
A20: card ((p|i)"{1}) + card ((p|i)"{0}) = len (p|i) by A17,Th6;
per cases;
suppose i > len p;
then
A21: p|i = p by FINSEQ_1:58;
p |len p = p by FINSEQ_1:58;
then 2* Sum p < len p by A8,A9,A11;
then k+ k < n+k by A8,A10,CARD_1:def 7;
hence thesis by XREAL_1:6,A14,A15,A13,A21;
end;
suppose i <= len p;
then card ((p|i)"{1})+card ((p|i)"{1})<card ((p|i)"{1})+card ((p|i)"{0})
by FINSEQ_1:59,A18,A20,A19;
hence thesis by XREAL_1:6;
end;
end;
theorem Th23:
f is A,n,B,k-dominated-election implies f.1 = A
proof
set f1=f|1;
assume
A1:f is A,n,B,k-dominated-election;
then n > k by Th14;
then len f >= 1+0 by A1,NAT_1:13;
then
A2: len f1 = 1 by FINSEQ_1:59;
card (f1"{A}) > card (f1"{B}) by A1;
then
A3: f1"{A} is non empty;
dom f1 = Seg 1 by FINSEQ_1:def 3,A2;
then
A4: f1"{A} = {1} by RELAT_1:132,FINSEQ_1:2,A3,ZFMISC_1:33;
1 in {1} by FINSEQ_1:2;
then f1.1 in {A} by A4,FUNCT_1:def 7;
then A=f1.1 by TARSKI:def 1;
hence thesis by FINSEQ_3:112;
end;
theorem Th24:
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)
proof
let d be XFinSequence of NAT;
set Xd=XFS2FS d,Z=<*0*>,ZXd=Z^Xd;
reconsider D=d as XFinSequence of REAL;
A1: len Z = 1 by FINSEQ_1:39;
rng Z ={0} by FINSEQ_1:39;
then
A2: rng Z c= {0,1} by ZFMISC_1:7;
thus d in Domin_0(n+k,k) implies ZXd in DominatedElection(0,n+1,1,k)
proof
assume
A4: d in Domin_0(n+k,k);
then
A5: d is dominated_by_0 by CATALAN2:20;
A6: Sum d = k by A4,CATALAN2:20;
len d = n+k by A4,CATALAN2:20;
then
A7: len Xd = n+k by AFINSQ_1:def 9;
A8: rng Xd c= {0,1} by A5,Th2;
rng (Z^Xd) = rng Z\/rng Xd by FINSEQ_1:31;
then reconsider ZX=ZXd as FinSequence of {0,1}
by XBOOLE_1:8,A8,A2,FINSEQ_1:def 4;
len ZX = n+k+1 by A1,A7,FINSEQ_1:22;
then
A9: ZX is Tuple of n+1+k,{0,1} by CARD_1:def 7;
A10: Sum ZXd = 0 + Sum Xd by RVSUM_1:76
.= 0+addreal $$ XFS2FS D by RVSUM_1:def 12
.= addreal "**" D by AFINSQ_2:44
.= k by A6,AFINSQ_2:48;
for i st i >0 holds 2* Sum (ZXd|i) < i
proof
let i such that
A11: i>0;
reconsider i1=i-1 as Nat by A11,NAT_1:14,NAT_1:21;
ZXd| i = ZXd|Seg (i1+1)
.= Z ^ (Xd|i1) by A1,FINSEQ_6:14;
then
A12: Sum (ZXd| i) = 0 + Sum (Xd|i1) by RVSUM_1:76
.= 0 + Sum XFS2FS (d|i1) by Th1
.= Sum XFS2FS (D|i1)
.=addreal $$ XFS2FS (D|i1) by RVSUM_1:def 12
.= addreal "**" (D|i1) by AFINSQ_2:44
.= Sum (d|i1) by AFINSQ_2:48;
2* Sum (d|i1) < i1+1 by A5,CATALAN2:2,NAT_1:13;
hence thesis by A12;
end;
then ZXd is 0,n+1,1,k-dominated-election by A9,Th22,A10;
hence thesis by Def3;
end;
assume ZXd in DominatedElection(0,n+1,1,k);
then
A13: ZXd is 0,n+1,1,k-dominated-election by Def3;
then ZXd is Tuple of n+1+k,{0,1} by Th22;
then
A14: rng ZXd c= {0,1} by FINSEQ_1:def 4;
rng Xd c= rng ZXd by FINSEQ_1:30;
then
A15: rng Xd c= {0,1} by A14;
A16: len ZXd = n+1+k by A13,CARD_1:def 7;
A17: len ZXd = 1 + len Xd by A1,FINSEQ_1:22;
A18: len Xd = len d by AFINSQ_1:def 9;
for k st k <= dom d holds 2*Sum (d|k) <= k
proof
let k such that k <= dom d;
ZXd| (k+1) = Z ^ (Xd|k) by A1,FINSEQ_6:14;
then Sum (ZXd| (k+1)) = 0 + Sum (Xd|k) by RVSUM_1:76
.= 0 + Sum XFS2FS (d|k) by Th1
.= Sum XFS2FS (D|k)
.= addreal $$ XFS2FS (D|k) by RVSUM_1:def 12
.= addreal "**" (D|k) by AFINSQ_2:44
.= Sum (d|k) by AFINSQ_2:48;
then 2* Sum (d|k) < k+1 by A13,Th22;
hence thesis by NAT_1:13;
end;
then A19:d is dominated_by_0 by A15, Th2;
Sum (ZXd) = 0 + Sum (Xd) by RVSUM_1:76
.= Sum XFS2FS D
.= addreal $$ XFS2FS (D) by RVSUM_1:def 12
.= addreal "**" (D) by AFINSQ_2:44
.= Sum (d) by AFINSQ_2:48;
then Sum d = k by A13,Th22;
hence d in Domin_0(n+k,k) by A19,A16,A17,A18,CATALAN2:def 2;
end;
theorem
card Domin_0(n+k,k) = card DominatedElection(0,n+1,1,k)
proof
set D=Domin_0(n+k,k),B=DominatedElection(0,n+1,1,k);
set Z=<*0*>;
defpred F[object,object] means for d be XFinSequence of NAT st d=$1
holds $2=Z^(XFS2FS d);
A1:for x being object st x in D ex y being object st y in B & F[x,y]
proof
let x be object;
assume
A2: x in D;
then consider p be XFinSequence of NAT such that
A3: p = x and
p is dominated_by_0 & dom p = n+k & Sum p = k by CATALAN2:def 2;
take y = Z^(XFS2FS p);
thus thesis by Th24,A3,A2;
end;
consider f be Function of D,B such that
A4:for x being object st x in D holds F[x,f.x] from FUNCT_2:sch 1(A1);
per cases;
suppose B <>{};
then
A5: dom f = D by FUNCT_2:def 1;
B c= rng f
proof
let y be object;
assume
A6: y in B;
then y in Election(0,n+1,1,k);
then reconsider g=y as Element of (n+1+k)-tuples_on {0,1};
g is (0,n+1,1,k)-dominated-election by A6,Def3;
then
A7: g.1 = 0 by Th23;
consider d be Element of {0,1}, dg be FinSequence of {0,1} such that
A8: d = g.1
and
A9: g = <*d*>^dg by FINSEQ_3:102;
{0,1} c= NAT;
then rng FS2XFS dg c= NAT;
then reconsider G=FS2XFS dg as XFinSequence of NAT by RELAT_1:def 19;
A10: XFS2FS G = dg;
then
A11: G in D by A6,A8,A9,A7,Th24;
f.G = g by A10,A6,A8,A9,A7,Th24,A4;
hence thesis by A11,A5,FUNCT_1:def 3;
end;
then
A12: rng f = B;
f is one-to-one
proof
let x1,x2 be object such that
A13: x1 in dom f
and
A14: x2 in dom f
and
A15: f.x1 = f.x2;
consider p1 be XFinSequence of NAT such that
A16: p1 = x1
and
p1 is dominated_by_0 & dom p1 = n+k & Sum p1 = k
by A13,CATALAN2:def 2;
consider p2 be XFinSequence of NAT such that
A17: p2 = x2
and
p2 is dominated_by_0 & dom p2 = n+k & Sum p2 = k
by A14,CATALAN2:def 2;
A18: f.p1 = Z^(XFS2FS p1) by A16, A13,A4;
f.p2 = Z^(XFS2FS p2) by A14,A17,A4;
then XFS2FS p1 = XFS2FS p2 by A18,A15,A16,A17,FINSEQ_1:33;
hence thesis by Th4,A16,A17;
end;
hence thesis by WELLORD2:def 4,A5,A12,CARD_1:5;
end;
suppose
A19: B={};
D={}
proof
assume D<>{};
then consider x be object such that
A20: x in D by XBOOLE_0:def 1;
ex y being object st y in B & F[x,y] by A20,A1;
hence thesis by A19;
end;
hence thesis by A19;
end;
end;
theorem Th26:
card Domin_0(n+k,k) = card DominatedElection(0,n+1,1,k)
proof
set D=Domin_0(n+k,k),B=DominatedElection(0,n+1,1,k);
set Z=<*0*>;
defpred F[object,object] means for d be XFinSequence of NAT st d=$1
holds $2=Z^(XFS2FS d);
A1:for x being object st x in D ex y being object st y in B & F[x,y]
proof
let x be object;
assume
A2: x in D;
then consider p be XFinSequence of NAT such that
A3: p = x
and
p is dominated_by_0 & dom p = n+k & Sum p = k by CATALAN2:def 2;
take y = Z^(XFS2FS p);
thus thesis by Th24,A3,A2;
end;
consider f be Function of D,B such that
A4:for x being object st x in D holds F[x,f.x] from FUNCT_2:sch 1(A1);
per cases;
suppose B <>{};
then
A5: dom f = D by FUNCT_2:def 1;
B c= rng f
proof
let y be object;
assume
A6: y in B;
then y in Election(0,n+1,1,k);
then reconsider g=y as Element of (n+1+k)-tuples_on {0,1};
g is (0,n+1,1,k)-dominated-election by A6,Def3;
then
A7: g.1 = 0 by Th23;
consider d be Element of {0,1}, dg be FinSequence of {0,1} such that
A8: d = g.1
and
A9: g = <*d*>^dg by FINSEQ_3:102;
{0,1} c= NAT;
then rng FS2XFS dg c= NAT;
then reconsider G=FS2XFS dg as XFinSequence of NAT by RELAT_1:def 19;
A10: XFS2FS G = dg;
then
A11: G in D by A6,A8,A9,A7,Th24;
f.G = g by A10,A6,A8,A9,A7,Th24,A4;
hence thesis by A11,A5,FUNCT_1:def 3;
end;
then
A12: rng f = B;
f is one-to-one
proof
let x1,x2 be object such that
A13: x1 in dom f
and
A14: x2 in dom f
and
A15: f.x1 = f.x2;
consider p1 be XFinSequence of NAT such that
A16: p1 = x1
and
p1 is dominated_by_0 & dom p1 = n+k & Sum p1 = k
by A13,CATALAN2:def 2;
consider p2 be XFinSequence of NAT such that
A17: p2 = x2
and
p2 is dominated_by_0 & dom p2 = n+k & Sum p2 = k
by A14,CATALAN2:def 2;
A18: f.p1 = Z^(XFS2FS p1) by A16,A13,A4;
f.p2 = Z^(XFS2FS p2) by A14,A17,A4;
then XFS2FS p1 = XFS2FS p2 by A18,A15,A16,A17,FINSEQ_1:33;
hence thesis by Th4,A16,A17;
end;
hence thesis by WELLORD2:def 4,A5,A12,CARD_1:5;
end;
suppose A19:B={};
D={}
proof
assume D<>{};
then consider x be object such that
A20: x in D by XBOOLE_0:def 1;
ex y being object st y in B & F[x,y] by A20,A1;
hence thesis by A19;
end;
hence thesis by A19;
end;
end;
theorem Th27:
A <> B & n > k implies
card DominatedElection(A,n,B,k) = ((n-k) / (n+k)) * ((n+k) choose k)
proof
assume that
A1: A<>B
and
A2: n > k;
reconsider n1=n-1 as Nat by A2,NAT_1:20;
A3: n1+1 = n;
then n1 >= k by A2,NAT_1:13;
then
A4: n1+k >= k+k by XREAL_1:6;
A5: n1+k >= k+0 by XREAL_1:6;
A6: n+k >= k+0 by XREAL_1:6;
set n1k=n1+k,nk=n+k;
A7: n1k+1 = nk;
n * (1/n)=1 by A2,XCMPLX_1:106;
then
A8: (nk!) / ((n1!)*(k!)) = n * (1/n) * ((nk!) / ((n1!)*(k!)))
.= n * ((1/n) * ((nk!) / ((n1!)*(k!))))
.= n * ( (nk!) / (n*((n1!)*(k!)))) by XCMPLX_1:103
.= n * ( (nk!) / (n*(n1!)*(k!)))
.= n * ( (nk!) / ((n!)*(k!))) by A3,NEWTON:15;
nk * (1/nk)=1 by A2,XCMPLX_1:106;
then
A9: (n1k!)/ ((n1!)*(k!)) = nk * (1/nk) * ((n1k!)/ ((n1!)*(k!)))
.= (1/nk) * ( nk* ((n1k!)/ ((n1!)*(k!))))
.= (1/nk) * ((nk* (n1k!))/ ((n1!)*(k!)))
by XCMPLX_1:74
.= (1/nk) * ( (nk!) / ((n1!)*(k!)))
by A7, NEWTON:15
.= (1/nk) * n * ( (nk!) / ((n!)*(k!)) ) by A8
.= (n/nk) * ( (nk!) / ((n!)*(k!)) ) by XCMPLX_1:99;
A10: n1+k-k = n1;
A11: nk-k=n;
thus card DominatedElection(A,n,B,k)= card DominatedElection(0,n1+1,1,k)
by A1,Th20
.= card Domin_0(n1+k,k) by Th26
.= (n1+k+1-2*k) / (n1+k+1-k) * ((n1+k) choose k) by A4,CATALAN2:29
.= (n-k) / (n) * (((n1k)!)/((n1!)*(k!))) by NEWTON:def 3,A5,A10
.= (n-k) /(n) * (n/nk)*( (nk!) / ((n!)*(k!)) ) by A9
.= ((n-k) / nk) * ( (nk!) / ((n!)*(k!)) ) by A2,XCMPLX_1:98
.= ((n-k) / nk) * (nk choose k) by A11,A6,NEWTON:def 3;
end;
begin :: Main Theorem
::$N Bertrand's Ballot Theorem
::$L https://en.wikipedia.org/wiki/Bertrand's_ballot_theorem Bertrand's Ballot Theorem
theorem
A <> B & n >= k implies prob DominatedElection(A,n,B,k) = (n-k) / (n+k)
proof
assume
A1: A<>B & n >= k;
then
A2: card Election(A,n,B,k) = (n+k) choose n by Th12;
A3: n+ k >= k+0 & (n+k)-k =n & n+k >= n by NAT_1:11;
A4: (n+k) choose n >0 by NAT_1:11,CATALAN2:26;
per cases by A1,XXREAL_0:1;
suppose
A5: n=k;
then DominatedElection(A,n,B,k) is empty by Th18;
then card DominatedElection(A,n,B,k) = 0;
then prob DominatedElection(A,n,B,k) = 0/((n+k) choose n)
by A2,RPR_1:def 1;
hence thesis by A5;
end;
suppose n > k; then
A6: card DominatedElection(A,n,B,k) =((n-k)/(n+k))*((n+k) choose k)
by A1,Th27
.= ((n-k) / (n+k))*((n+k) choose n) by A3,NEWTON:20;
thus prob DominatedElection(A,n,B,k)
= ((n-k)/(n+k))*((n+k) choose n) / ((n+k) choose n)
by A2,A6,RPR_1:def 1
.= ((n-k)/(n+k))*(((n+k) choose n)/((n+k) choose n)) by XCMPLX_1:74
.= ((n-k)/(n+k))*1 by A4,XCMPLX_1:60
.= (n-k)/(n+k);
end;
end;