EconCSLib.SocialChoice.Voting.ProfileSurgery #

Reusable profile-modification constructions for strict voting profiles.

The main construction is zProfile P Q R, the Muller-Satterthwaite splice: alternatives in R are ranked above alternatives outside R; inside R the ballot follows P, and outside R it follows Q.

source

noncomputable def SocialChoice.Voting.zBallot {A : Type u_2} [Fintype A] (P Q : LinearOrder A) (R : Set A) [(a : A) → Decidable (a ∈ R)] :

LinearOrder A

Splice two ballots across a set of alternatives.

Equations

SocialChoice.Voting.zBallot P Q R = SocialChoice.Voting.ballotFromInjective inferInstance (SocialChoice.Voting.zKey✝ P Q R) ⋯

Instances For

source

noncomputable def SocialChoice.Voting.zProfile {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (P Q : Profile N A) (R : Set A) [(a : A) → Decidable (a ∈ R)] :

Profile N A

Pointwise profile splice.

Equations

SocialChoice.Voting.zProfile P Q R = { pref := fun (i : N) => SocialChoice.Voting.zBallot (P.pref i) (Q.pref i) R }

Instances For

source

@[simp]

theorem SocialChoice.Voting.zProfile_apply {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (P Q : Profile N A) (R : Set A) [(a : A) → Decidable (a ∈ R)] (i : N) :

(zProfile P Q R).pref i = zBallot (P.pref i) (Q.pref i) R

source

theorem SocialChoice.Voting.zProfile_prefers_inside {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (P Q : Profile N A) (R : Set A) [(a : A) → Decidable (a ∈ R)] {a b : A} (ha : a ∈ R) (hb : b ∈ R) (i : N) :

Prefers (zProfile P Q R) i a b ↔ Prefers P i a b

Inside R, the splice follows the first profile.

source

theorem SocialChoice.Voting.zProfile_prefers_outside {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (P Q : Profile N A) (R : Set A) [(a : A) → Decidable (a ∈ R)] {a b : A} (ha : a ∉ R) (hb : b ∉ R) (i : N) :

Prefers (zProfile P Q R) i a b ↔ Prefers Q i a b

Outside R, the splice follows the second profile.

source

theorem SocialChoice.Voting.zProfile_prefers_inside_outside {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (P Q : Profile N A) (R : Set A) [(a : A) → Decidable (a ∈ R)] {a b : A} (ha : a ∈ R) (hb : b ∉ R) (i : N) :

Prefers (zProfile P Q R) i a b

Every alternative inside R is ranked above every alternative outside R.