EconCSLib.SocialChoice.FairDivision.Indivisible.Efficiency

Efficiency notions for indivisible goods allocation.

Main definitions

• IsParetoOptimal — no allocation weakly dominates A with at least one strict improvement

Design

IsParetoOptimal is stated with an explicit IsAllocation hypothesis on the dominating allocation B, so that the comparison is only over valid complete allocations (not arbitrary functions N → Finset G).

The combination EF1 + PO (Pareto optimal) always exists via the maximum Nash welfare allocation (Caragiannis et al. 2019), and also via envy-cycle elimination (Lipton et al. 2004). These results are formalized in later phases.

References

• Nisan et al., Algorithmic Game Theory, Chapter 12
• Lipton et al., "On Approximately Fair Allocations of Indivisible Goods" (EC 2004)
• Caragiannis et al., "The Unreasonable Fairness of Maximum Nash Welfare" (EC 2016)

Pareto optimality

@[reducible, inline]

abbrev SocialChoice.FairDivision.Indivisible.IsParetoOptimal {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] (v : Valuation N G) (allGoods : Finset G) (A : Allocation N G) : Prop

An allocation A is Pareto optimal if no complete allocation B weakly improves every agent's bundle value and strictly improves at least one agent's value.

[Fintype N] is required because IsAllocation uses Finset.univ.biUnion. [DecidableEq G] is required for Finset operations. [AGT Ch.12]

Equations

• One or more equations did not get rendered due to their size.

Basic properties

theorem SocialChoice.FairDivision.Indivisible.not_paretoImproved_self {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] (v : Valuation N G) (allGoods : Finset G) (A : Allocation N G) : ¬(IsAllocation allGoods A ∧ (∀ (i : N), v.val i (A i) ≤ v.val i (A i)) ∧ ∃ (i : N), v.val i (A i) < v.val i (A i))

The allocation itself is not a Pareto improvement over itself.