:: by Karol P\kak

::

:: Received June 13, 2014

:: Copyright (c) 2014-2018 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

for d being XFinSequence of D

for n being Nat holds XFS2FS (d | n) = (XFS2FS d) | n

proof end;

theorem Th3: :: 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

for d1 being XFinSequence of D1

for d2 being XFinSequence of D2 st d1 = d2 holds

XFS2FS d1 = XFS2FS d2

proof end;

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

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)

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}))

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;

ex b_{1} 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_{1} iff card (v " {A}) = n )

for b_{1}, b_{2} 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_{1} iff card (v " {A}) = n ) ) & ( for v being Element of (n + k) -tuples_on {A,B} holds

( v in b_{2} iff card (v " {A}) = n ) ) holds

b_{1} = b_{2}

end;
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 for v being Element of (n + k) -tuples_on {A,B} holds

( v in it iff card (v " {A}) = n );

ex b

for v being Element of (n + k) -tuples_on {A,B} holds

( v in b

proof end;

uniqueness for b

( v in b

( v in b

b

proof 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_{5} being Subset of ((n + k) -tuples_on {A,B}) holds

( b_{5} = Election (A,n,B,k) iff for v being Element of (n + k) -tuples_on {A,B} holds

( v in b_{5} iff card (v " {A}) = n ) );

for A being object

for n being Nat

for B being object

for k being Nat

for b

( b

( v in b

registration

let A be object ;

let n be Nat;

let B be object ;

let k be Nat;

coherence

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

end;
let n be Nat;

let B be object ;

let k be Nat;

coherence

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

registration

let A be object ;

let n be Nat;

let k be non empty Nat;

coherence

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

end;
let n be Nat;

let k be non empty Nat;

coherence

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

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 )

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

for A, B being object st A <> B holds

card (Election (A,n,B,k)) = (n + k) choose n

proof 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}) ) ) );

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

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

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

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

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

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;

ex b_{1} being Subset of (Election (A,n,B,k)) st

for f being FinSequence holds

( f in b_{1} iff f is A,n,B,k -dominated-election )

for b_{1}, b_{2} being Subset of (Election (A,n,B,k)) st ( for f being FinSequence holds

( f in b_{1} iff f is A,n,B,k -dominated-election ) ) & ( for f being FinSequence holds

( f in b_{2} iff f is A,n,B,k -dominated-election ) ) holds

b_{1} = b_{2}

end;
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 for f being FinSequence holds

( f in it iff f is A,n,B,k -dominated-election );

ex b

for f being FinSequence holds

( f in b

proof end;

uniqueness for b

( f in b

( f in b

b

proof 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_{5} being Subset of (Election (A,n,B,k)) holds

( b_{5} = DominatedElection (A,n,B,k) iff for f being FinSequence holds

( f in b_{5} iff f is A,n,B,k -dominated-election ) );

for A being object

for n being Nat

for B being object

for k being Nat

for b

( b

( f in b

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

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)

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

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

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

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

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

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)

for A, B being object st A <> B & n >= k holds

prob (DominatedElection (A,n,B,k)) = (n - k) / (n + k)

proof end;