:: Bertrand's Ballot Theorem
:: by Karol P\kak
::
:: Received June 13, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users

theorem Th1: :: BALLOT_1:1

for D being non empty set
for d being XFinSequence of D
for n being Nat holds XFS2FS (d | n) = (XFS2FS d) | n by AFINSQ_2:84;

theorem Th2: :: BALLOT_1:2

for D being non empty set
for d being XFinSequence of D holds rng d = rng (XFS2FS d) by AFINSQ_1:97;

theorem :: BALLOT_1:3

for D1, D2 being non empty set
for d1 being XFinSequence of D1
for d2 being XFinSequence of D2 st d1 = d2 holds
XFS2FS d1 = XFS2FS d2 ;

theorem Th4: :: BALLOT_1:4

for D being non empty set
for d1, d2 being XFinSequence of D st XFS2FS d1 = XFS2FS d2 holds
d1 = d2

proof end;

theorem :: BALLOT_1:5

for D being set
for d being FinSequence of D holds XFS2FS (FS2XFS d) = d ;

theorem Th6: :: BALLOT_1:6

for f being FinSequence
for x, y being object st rng f c= {x,y} & x <> y holds
(card (f " {x})) + (card (f " {y})) = len f

proof end;

theorem Th7: :: BALLOT_1:7

for f, g being Function st f is one-to-one holds
for x being object st x in dom f holds
Coim ((f * g),(f . x)) = Coim (g,x)

proof end;

theorem Th21: :: BALLOT_1:8

for r being Real
for f being real-valued FinSequence st rng f c= {0,r} holds
Sum f = r * (card (f " {r}))

proof end;

definition

let A be object ;
let n be Nat;
let B be object ;
let k be Nat;

func Election (A,n,B,k) -> Subset of ((n + k) -tuples_on {A,B}) means :Def1: :: BALLOT_1:def 1
for v being Element of (n + k) -tuples_on {A,B} holds
( v in it iff card (v " {A}) = n );

existence
ex b₁ being Subset of ((n + k) -tuples_on {A,B}) st
for v being Element of (n + k) -tuples_on {A,B} holds
( v in b₁ iff card (v " {A}) = n )

proof end;

uniqueness
for b₁, b₂ being Subset of ((n + k) -tuples_on {A,B}) st ( for v being Element of (n + k) -tuples_on {A,B} holds
( v in b₁ iff card (v " {A}) = n ) ) & ( for v being Element of (n + k) -tuples_on {A,B} holds
( v in b₂ iff card (v " {A}) = n ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Election BALLOT_1:def 1 :
for A being object
for n being Nat
for B being object
for k being Nat
for b₅ being Subset of ((n + k) -tuples_on {A,B}) holds
( b₅ = Election (A,n,B,k) iff for v being Element of (n + k) -tuples_on {A,B} holds
( v in b₅ iff card (v " {A}) = n ) );

registration

let A be object ;
let n be Nat;
let B be object ;
let k be Nat;

cluster Election (A,n,B,k) -> finite ;

coherence
Election (A,n,B,k) is finite ;

end;

theorem :: BALLOT_1:9

for n being Nat
for A being object holds Election (A,n,A,0) = {(n |-> A)}

proof end;

theorem ElectionEmpty: :: BALLOT_1:10

for n, k being Nat
for A being object st k > 0 holds
Election (A,n,A,k) is empty

proof end;

registration

let A be object ;
let n be Nat;
let k be non empty Nat;

cluster Election (A,n,A,k) -> empty ;

coherence
Election (A,n,A,k) is empty

proof end;

end;

theorem Th10: :: BALLOT_1:11

for n, k being Nat
for A, B being object holds Election (A,n,B,k) = Choose ((Seg (n + k)),n,A,B)

proof end;

theorem Th11: :: BALLOT_1:12

for n, k being Nat
for A, B being object
for v being Element of (n + k) -tuples_on {A,B} st A <> B holds
( v in Election (A,n,B,k) iff card (v " {B}) = k )

proof end;

theorem Th12: :: BALLOT_1:13

for n, k being Nat
for A, B being object st A <> B holds
card (Election (A,n,B,k)) = (n + k) choose n

proof end;

definition

let A be object ;
let n be Nat;
let B be object ;
let k be Nat;
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 being Nat st i > 0 holds
card ((v | i) " {A}) > card ((v | i) " {B}) ) );

end;

:: deftheorem defines -dominated-election BALLOT_1:def 2 :
for A being object
for n being Nat
for B being object
for k being Nat
for v being FinSequence holds
( v is A,n,B,k -dominated-election iff ( v in Election (A,n,B,k) & ( for i being Nat st i > 0 holds
card ((v | i) " {A}) > card ((v | i) " {B}) ) ) );

theorem Th13: :: BALLOT_1:14

for n, k being Nat
for A, B being object
for f being FinSequence st f is A,n,B,k -dominated-election holds
A <> B

proof end;

theorem Th14: :: BALLOT_1:15

for n, k being Nat
for A, B being object
for f being FinSequence st f is A,n,B,k -dominated-election holds
n > k

proof end;

theorem Th15: :: BALLOT_1:16

for n being Nat
for A, B being object st A <> B & n > 0 holds
n |-> A is A,n,B, 0 -dominated-election

proof end;

theorem Th16: :: BALLOT_1:17

for n, k, i being Nat
for A, B being object
for f being FinSequence st f is A,n,B,k -dominated-election & i < n - k holds
f ^ (i |-> B) is A,n,B,k + i -dominated-election

proof end;

theorem :: BALLOT_1:18

for n, k, i, j being Nat
for A, B being object
for f, g being FinSequence st f is A,n,B,k -dominated-election & g is A,i,B,j -dominated-election holds
f ^ g is A,n + i,B,k + j -dominated-election

proof end;

definition

let A be object ;
let n be Nat;
let B be object ;
let k be Nat;

func DominatedElection (A,n,B,k) -> Subset of (Election (A,n,B,k)) means :Def3: :: BALLOT_1:def 3
for f being FinSequence holds
( f in it iff f is A,n,B,k -dominated-election );

existence
ex b₁ being Subset of (Election (A,n,B,k)) st
for f being FinSequence holds
( f in b₁ iff f is A,n,B,k -dominated-election )

proof end;

uniqueness
for b₁, b₂ being Subset of (Election (A,n,B,k)) st ( for f being FinSequence holds
( f in b₁ iff f is A,n,B,k -dominated-election ) ) & ( for f being FinSequence holds
( f in b₂ iff f is A,n,B,k -dominated-election ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines DominatedElection BALLOT_1:def 3 :
for A being object
for n being Nat
for B being object
for k being Nat
for b₅ being Subset of (Election (A,n,B,k)) holds
( b₅ = DominatedElection (A,n,B,k) iff for f being FinSequence holds
( f in b₅ iff f is A,n,B,k -dominated-election ) );

theorem Th18: :: BALLOT_1:19

for n, k being Nat
for A, B being object st ( A = B or n <= k ) holds
DominatedElection (A,n,B,k) is empty

proof end;

theorem :: BALLOT_1:20

for n, k being Nat
for A, B being object st n > k & A <> B holds
(n |-> A) ^ (k |-> B) in DominatedElection (A,n,B,k)

proof end;

theorem Th20: :: BALLOT_1:21

for n, k being Nat
for A, B being object st A <> B holds
card (DominatedElection (A,n,B,k)) = card (DominatedElection (0,n,1,k))

proof end;

theorem Th22: :: BALLOT_1:22

for n, k being Nat
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 being Nat st i > 0 holds
2 * (Sum (p | i)) < i ) ) )

proof end;

theorem Th23: :: BALLOT_1:23

for n, k being Nat
for A, B being object
for f being FinSequence st f is A,n,B,k -dominated-election holds
f . 1 = A

proof end;

theorem Th24: :: BALLOT_1:24

for n, k being Nat
for d being XFinSequence of NAT holds
( d in Domin_0 ((n + k),k) iff <*0*> ^ (XFS2FS d) in DominatedElection (0,(n + 1),1,k) )

proof end;

theorem :: BALLOT_1:25

for n, k being Nat holds card (Domin_0 ((n + k),k)) = card (DominatedElection (0,(n + 1),1,k))

proof end;

theorem Th26: :: BALLOT_1:26

for n, k being Nat holds card (Domin_0 ((n + k),k)) = card (DominatedElection (0,(n + 1),1,k))

proof end;

theorem Th27: :: BALLOT_1:27

for n, k being Nat
for A, B being object st A <> B & n > k holds
card (DominatedElection (A,n,B,k)) = ((n - k) / (n + k)) * ((n + k) choose k)

proof end;

:: Bertrand's Ballot Theorem

theorem :: BALLOT_1:28

for n, k being Nat
for A, B being object st A <> B & n >= k holds
prob (DominatedElection (A,n,B,k)) = (n - k) / (n + k)

proof end;