:: Bertrand's Ballot Theorem
:: by Karol P\kak
::
:: 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) = () | 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 () 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 () = 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 b1 being Subset of ((n + k) -tuples_on {A,B}) st
for v being Element of (n + k) -tuples_on {A,B} holds
( v in b1 iff card (v " {A}) = n )
proof end;
uniqueness
for b1, b2 being Subset of ((n + k) -tuples_on {A,B}) st ( for v being Element of (n + k) -tuples_on {A,B} holds
( v in b1 iff card (v " {A}) = n ) ) & ( for v being Element of (n + k) -tuples_on {A,B} holds
( v in b2 iff card (v " {A}) = n ) ) holds
b1 = b2
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 b5 being Subset of ((n + k) -tuples_on {A,B}) holds
( b5 = Election (A,n,B,k) iff for v being Element of (n + k) -tuples_on {A,B} holds
( v in b5 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 b1 being Subset of (Election (A,n,B,k)) st
for f being FinSequence holds
( f in b1 iff f is A,n,B,k -dominated-election )
proof end;
uniqueness
for b1, b2 being Subset of (Election (A,n,B,k)) st ( for f being FinSequence holds
( f in b1 iff f is A,n,B,k -dominated-election ) ) & ( for f being FinSequence holds
( f in b2 iff f is A,n,B,k -dominated-election ) ) holds
b1 = b2
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 b5 being Subset of (Election (A,n,B,k)) holds
( b5 = DominatedElection (A,n,B,k) iff for f being FinSequence holds
( f in b5 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 ^ () 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;