Documentation

Linglib.Core.SocialChoice.Rules

Five classical rules with the conditions they meet or fail. Majority rule, after May, meets every Arrow condition except weak-ordering outputs. The Pareto rule, after Weymark, is a quasi-ordering that leaves every trade-off incomparable. The utilitarian rule meets every Arrow condition except ordinal invariance, failing even ratio-scale invariance. The Cobb–Douglas rule, after Tsui and Weymark, is ratio-scale invariant on non-negative profiles, and the maximin rule needs only ordinal level comparability. The Pareto rule is the unanimous verdict of the utilitarian rules with positive weights, so a trade-off is exactly a pair that two positive weightings rank oppositely.

Main definitions #

SocialChoice.majority, SocialChoice.paretoRule, SocialChoice.utilitarian, SocialChoice.maximin, SocialChoice.cobbDouglas: the five rules.

Main statements #

SocialChoice.paretoRule_iff_forall_utilitarian: the Pareto rule is the unanimous verdict of the positively weighted utilitarian rules.
SocialChoice.not_ordinalInvariant_utilitarian: the utilitarian rule needs cardinal information.
SocialChoice.maximin_ordinalLevelInvariant: the maximin rule needs only ordinal level comparability.

References #

Majority rule #

def SocialChoice.majority {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [LinearOrder K] :

Rule ι α K

Under majority rule x ⪰ y iff at least as many individuals rank x weakly above y as rank y weakly above x.

Equations

SocialChoice.majority v x y = ({i : ι | v x i ≤ v y i}.card ≤ {i : ι | v y i ≤ v x i}.card)

Instances For

@[instance_reducible]

instance SocialChoice.instDecidableRelMajority {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [LinearOrder K] (v : Profile ι α K) :

DecidableRel (majority v)

Equations

SocialChoice.instDecidableRelMajority v x✝¹ x✝ = id inferInstance

theorem SocialChoice.majority_weakPareto {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [LinearOrder K] [Nonempty ι] :

WeakPareto majority

theorem SocialChoice.majority_independent {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [LinearOrder K] :

Independent majority

theorem SocialChoice.majority_ordinalInvariant {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [LinearOrder K] :

Invariant ordinal majority

theorem SocialChoice.majority_anonymous {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [LinearOrder K] :

Anonymous majority

theorem SocialChoice.majority_paretoIndifferent {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [LinearOrder K] :

ParetoIndifferent majority

theorem SocialChoice.majority_nonDictatorial {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [LinearOrder K] [Nontrivial ι] [Nontrivial α] [Nontrivial K] :

NonDictatorial majority

The Pareto rule #

def SocialChoice.paretoRule {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Preorder K] :

Rule ι α K

Under the Pareto rule x ⪰ y iff every individual ranks x weakly above y.

Equations

SocialChoice.paretoRule v x y = (v y ≤ v x)

Instances For

theorem SocialChoice.paretoRule_quasiOrderValued {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Preorder K] :

QuasiOrderValued paretoRule

theorem SocialChoice.paretoRule_strongPareto {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Preorder K] :

StrongPareto paretoRule

theorem SocialChoice.paretoRule_paretoIndifferent {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Preorder K] :

ParetoIndifferent paretoRule

theorem SocialChoice.paretoRule_independent {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Preorder K] :

Independent paretoRule

theorem SocialChoice.paretoRule_anonymous {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Preorder K] :

Anonymous paretoRule

theorem SocialChoice.paretoRule_incomparable {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Preorder K] {v : Profile ι α K} {x y : α} {i j : ι} (hi : v y i < v x i) (hj : v x j < v y j) :

¬paretoRule v x y ∧ ¬paretoRule v y x

A trade-off, one individual ranking x strictly above y and another y above x, is incomparable under the Pareto rule.

theorem SocialChoice.paretoRule_ordinalInvariant {ι : Type u_1} {α : Type u_2} {K : Type u_3} [LinearOrder K] :

Invariant ordinal paretoRule

The utilitarian rule #

def SocialChoice.utilitarian {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] [LinearOrder K] (c : ι → K) :

Rule ι α K

Under the utilitarian rule with weights c, x ⪰ y iff the weighted sum of values favours x.

Equations

SocialChoice.utilitarian c v x y = (c ⬝ᵥ v y ≤ c ⬝ᵥ v x)

Instances For

theorem SocialChoice.utilitarian_weakOrderValued {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] [LinearOrder K] (c : ι → K) :

WeakOrderValued (utilitarian c)

theorem SocialChoice.utilitarian_paretoIndifferent {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] [LinearOrder K] (c : ι → K) :

ParetoIndifferent (utilitarian c)

theorem SocialChoice.utilitarian_independent {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] [LinearOrder K] (c : ι → K) :

Independent (utilitarian c)

theorem SocialChoice.utilitarian_weakPareto {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] [LinearOrder K] (c : ι → K) [IsStrictOrderedRing K] (hc : ∀ (i : ι), 0 ≤ c i) (hpos : ∃ (i : ι), 0 < c i) :

WeakPareto (utilitarian c)

theorem SocialChoice.utilitarian_cardinalUnitInvariant {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] [LinearOrder K] (c : ι → K) [IsStrictOrderedRing K] :

Invariant cardinalUnit (utilitarian c)

theorem SocialChoice.utilitarian_nonDictatorial {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] [LinearOrder K] (c : ι → K) [IsStrictOrderedRing K] [Nontrivial α] (h₂ : ∀ (i : ι), ∃ (j : ι), j ≠ i ∧ 0 < c j) :

NonDictatorial (utilitarian c)

theorem SocialChoice.not_ratioInvariant_utilitarian {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] [LinearOrder K] (c : ι → K) [IsStrictOrderedRing K] [Nontrivial α] {i j : ι} (hij : i ≠ j) (hi : 0 < c i) (hj : 0 < c j) :

¬Invariant ratio (utilitarian c)

With two positive weights the utilitarian rule is not even ratio-scale invariant, since rescaling one individual's values breaks a tie.

theorem SocialChoice.not_ordinalInvariant_utilitarian {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] [LinearOrder K] (c : ι → K) [IsStrictOrderedRing K] [Nontrivial α] {i j : ι} (hij : i ≠ j) (hi : 0 < c i) (hj : 0 < c j) :

¬Invariant ordinal (utilitarian c)

theorem SocialChoice.paretoRule_iff_forall_utilitarian {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] [LinearOrder K] [IsStrictOrderedRing K] {v : Profile ι α K} {x y : α} :

paretoRule v x y ↔ ∀ (c : ι → K), (∀ (i : ι), 0 < c i) → utilitarian c v x y

The Pareto rule ranks x weakly above y iff every utilitarian rule with positive weights does.

theorem SocialChoice.asymmRel_paretoRule_iff_forall_utilitarian {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] [LinearOrder K] [IsStrictOrderedRing K] {v : Profile ι α K} {x y : α} :

AsymmRel (paretoRule v) x y ↔ ∀ (c : ι → K), (∀ (i : ι), 0 < c i) → AsymmRel (utilitarian c v) x y

The Pareto rule ranks x strictly above y iff every utilitarian rule with positive weights does.

The maximin rule #

def SocialChoice.maximin {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Nonempty ι] [LinearOrder K] :

Rule ι α K

Under the maximin rule, x ⪰ y iff the lowest value of x is at least the lowest value of y.

Equations

SocialChoice.maximin v x y = (Finset.univ.inf' ⋯ (v y) ≤ Finset.univ.inf' ⋯ (v x))

Instances For

theorem SocialChoice.maximin_ordinalLevelInvariant {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Nonempty ι] [LinearOrder K] :

Invariant ordinalLevel maximin

The maximin rule needs only ordinal level comparability, since a common strictly increasing map moves every lowest value alike.

The Cobb–Douglas rule #

def SocialChoice.cobbDouglas {ι : Type u_1} {α : Type u_2} [Fintype ι] (c : ι → ℝ) :

Rule ι α ℝ

Under the Cobb–Douglas rule with exponents c, x ⪰ y iff the weighted geometric product of values favours x.

Equations

SocialChoice.cobbDouglas c v x y = (∏ i : ι, v y i ^ c i ≤ ∏ i : ι, v x i ^ c i)

Instances For

theorem SocialChoice.cobbDouglas_weakOrderValued {ι : Type u_1} {α : Type u_2} [Fintype ι] (c : ι → ℝ) :

WeakOrderValued (cobbDouglas c)

theorem SocialChoice.cobbDouglas_paretoIndifferent {ι : Type u_1} {α : Type u_2} [Fintype ι] (c : ι → ℝ) :

ParetoIndifferent (cobbDouglas c)

theorem SocialChoice.cobbDouglas_independent {ι : Type u_1} {α : Type u_2} [Fintype ι] (c : ι → ℝ) :

Independent (cobbDouglas c)

theorem SocialChoice.cobbDouglas_transform_of_nonneg {ι : Type u_1} {α : Type u_2} [Fintype ι] (c : ι → ℝ) {f : ι → ℝ → ℝ} (hf : f ∈ ratio) {v : Profile ι α ℝ} (hv : ∀ (x : α) (i : ι), 0 ≤ v x i) :

cobbDouglas c (Profile.transform f v) = cobbDouglas c v

On non-negative profiles the Cobb–Douglas rule is ratio-scale invariant.