Lean declarations

def SocialChoice.FairDivision.Indivisible.paretoDomCount EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Indivisible.EnvyCycle

noncomputable def paretoDomCount [Fintype N] [Fintype G]
    (v : Valuation N G) (A : Allocation N G) : ℕ :=
  (Finset.univ.filter (fun B : N → Finset G => ∀ i : N, v.val i (A i) ≤ v.val i (B i))).card

lemma SocialChoice.FairDivision.Indivisible.paretoDomSet_subset EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Indivisible.EnvyCycle

lemma paretoDomSet_subset [Fintype N] [Fintype G]
    (v : Valuation N G) (A A' : Allocation N G)
    (h : ∀ i : N, v.val i (A i) ≤ v.val i (A' i)) :
    Finset.univ.filter (fun B : N → Finset G => ∀ i : N, v.val i (A' i) ≤ v.val i (B i)) ⊆
    Finset.univ.filter (fun B : N → Finset G => ∀ i : N, v.val i (A i) ≤ v.val i (B i))

lemma SocialChoice.FairDivision.Indivisible.self_mem_paretoDomSet EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Indivisible.EnvyCycle

lemma self_mem_paretoDomSet [Fintype N] [Fintype G]
    (v : Valuation N G) (A : Allocation N G) :
    A ∈ Finset.univ.filter (fun B : N → Finset G => ∀ i : N, v.val i (A i) ≤ v.val i (B i))

lemma SocialChoice.FairDivision.Indivisible.not_mem_paretoDomSet_of_strict EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Indivisible.EnvyCycle

lemma not_mem_paretoDomSet_of_strict [Fintype N] [Fintype G]
    (v : Valuation N G) (A A' : Allocation N G)
    (_hweak : ∀ i : N, v.val i (A i) ≤ v.val i (A' i))
    (hstrict : ∃ j : N, v.val j (A j) < v.val j (A' j)) :
    A ∉ Finset.univ.filter (fun B : N → Finset G => ∀ i : N, v.val i (A' i) ≤ v.val i (B i))

lemma SocialChoice.FairDivision.Indivisible.rotateBundles_paretoDomCount_lt EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Indivisible.EnvyCycle

Rotation along an envy cycle strictly decreases the Pareto domination count.

lemma rotateBundles_paretoDomCount_lt [Fintype N] [Fintype G] [DecidableEq N]
    (v : Valuation N G) (A : Allocation N G)
    (l : List N) (hcyc : isEnvyCycle v A l) :
    paretoDomCount v (rotateBundles A l) < paretoDomCount v A

Modules: EconCSLib.SocialChoice.FairDivision.Indivisible.EnvyCycle

Pareto-Domination Count Termination Measure

The envy-cycle elimination algorithm ([[social_choice.fair_division.indivisible.envy_cycle_algorithm]]) repeatedly rotates bundles along cycles. To prove termination we need a strictly decreasing well-founded measure.

The chosen measure is the Pareto-domination count: the number of allocations (over the finite set of possible $\mathrm{Allocation}\ N\ G$ functions for $N, G$ finite) that Pareto-dominate or equal the current allocation in agent-utility vectors.

In Lean: paretoDomCount v allGoods A : ℕ, with hypotheses [Fintype N] [Fintype G].

Structural lemmas

paretoDomSet_subset: the domination set is a subset of the (finite) set of complete allocations of allGoods.
self_mem_paretoDomSet: $A$ Pareto-dominates itself (weak domination is reflexive), so $A$ is in its own set and the count is $\ge 1$.
not_mem_paretoDomSet_of_strict: if $A'$ strictly improves over $A$ (some agent gets strictly more), then $A$ no longer belongs to $A'$'s Pareto-domination set — i.e. $A$ is dropped from the count when we move to $A'$.

Strict decrease under rotation

rotateBundles_paretoDomCount_lt (with [DecidableEq N]): if $l$ is an envy cycle, the rotation strictly decreases the Pareto-domination count: $$ \mathrm{paretoDomCount}(\mathrm{rotate}(A, l)) < \mathrm{paretoDomCount}(A). $$

The argument:

Cycle rotation strictly improves at least one agent ([[social_choice.fair_division.indivisible.rotate_bundles]]'s rotateBundles_improves) and weakly improves the rest.
Therefore $\mathrm{rotate}(A, l)$ Pareto-dominates $A$ strictly.
By not_mem_paretoDomSet_of_strict, $A$ leaves the Pareto-domination set of $\mathrm{rotate}(A, l)$, dropping the count by at least one.
The new set is a subset of the old (any allocation dominating $\mathrm{rotate}(A, l)$ also dominates $A$).

Hence the count strictly decreases, which gives termination.

Why this measure works

The total number of allocations is finite ([Fintype N] and [Fintype G] together with Finset.card allGoods), so any strictly-decreasing $\mathbb{N}$-valued measure is well-founded. This lets eliminateAllCycles ([[social_choice.fair_division.indivisible.eliminate_all_cycles]]) be defined by well-founded recursion in Lean.

References

Lipton, Markakis, Mossel, and Saberi (2004). "On Approximately Fair Allocations of Indivisible Goods". EC. Termination of envy-cycle elimination.

Used by