Documentation

EconCSLib.SocialChoice.FairDivision.Indivisible.EFX

EconCSLib.SocialChoice.FairDivision.Indivisible.EFX #

EFX (envy-free up to any good) allocations for 2 agents.

Main results #

EFX existence for 2 agents #

Theorem: For 2 agents with additive nonneg valuations on any set of goods, a complete EFX allocation always exists.

Proof sketch (maximality argument): Among all complete allocations where agent 0 is non-envious (v_0(A_0) ≥ v_0(A_1)), choose A* to maximize v_1(A_1).

  1. Agent 0 is EFX trivially (non-envious by construction).

  2. Agent 1: suppose EFX fails at some good g ∈ A*_0, i.e., v_1(A*_0 \ {g}) > v_1(A*_1).

    Case A (v_0(A*_0 \ {g}) < v_0(A*_1 ∪ {g})): the swap allocation (A*_1 ∪ {g}, A*_0 \ {g}) has agent 0 non-envious (they get the larger bundle). Agent 1 now holds A*_0 \ {g} with value > v_1(A*_1). Contradicts maximality of A*.

    Case B (v_0(A*_0 \ {g}) ≥ v_0(A*_1 ∪ {g}), v_1(g) > 0): the allocation (A*_0 \ {g}, A*_1 ∪ {g}) keeps agent 0 non-envious, and v_1(A*_1 ∪ {g}) = v_1(A*_1) + v_1(g) > v_1(A*_1). Contradicts maximality of A*.

    Case C (Case B with v_1(g) = 0): v_1(A*_0) = v_1(A*_0 \ {g}) > v_1(A*_1) > 0, so some other g' ∈ A*_0 satisfies v_1(g') > 0. Apply Case A or B to g'. (Terminates since A*_0 is finite and we exhaust zero-v_1 goods first.)

The formal proof below follows this maximality argument directly. EnvyCycle.lean develops a separate EF1 algorithm for many agents.

References #

Sufficient conditions for EFX #

source
theorem SocialChoice.FairDivision.Indivisible.IsEFX.of_noEnvy_mono {G : Type u_2} [DecidableEq G] (v : Valuation (Fin 2) G) (hmono : ∀ (i : Fin 2) (S T : Finset G), T ⊆ S → v.val i T ≤ v.val i S) (A : Allocation (Fin 2) G) (h : IsEnvyFree v A) :
IsEFX v A

If neither agent envies and the valuation is monotone (subsets have less value), the allocation is EFX. Immediate from IsEnvyFree.isEFX_of_mono.

Note: no-envy alone does NOT imply EFX without monotonicity.

EFX when one bundle is a singleton #

source
theorem SocialChoice.FairDivision.Indivisible.isEFX_of_singleton_bundle {G : Type u_2} [DecidableEq G] (v : Valuation (Fin 2) G) (A : Allocation (Fin 2) G) (i j : Fin 2) {g : G} (hAi : A i = {g}) (h_empty_le : v.val j ∅ ≤ v.val j (A j)) (h : G) :
h ∈ A i → v.val j (A i \ {h}) ≤ v.val j (A j)

If agent i's bundle is a singleton {g}, then agent j is EFX with respect to agent i: removing the sole good from A i leaves ∅, which agent j values at most their own bundle.

The hypothesis h_empty_le : v.val j ∅ ≤ v.val j (A j) is satisfied whenever valuations are additive with nonneg weights (AdditiveValuation with 0 ≤ w.weight j g for all g).

EFX for 2 agents, 2 goods #

source
theorem SocialChoice.FairDivision.Indivisible.efx_two_agents_two_goods {G : Type u_2} [DecidableEq G] (v : Valuation (Fin 2) G) {g₀ g₁ : G} (h₀ : v.val 0 ∅ ≤ v.val 0 {g₀}) (h₁ : v.val 1 ∅ ≤ v.val 1 {g₁}) (A : Allocation (Fin 2) G) (hA0 : A 0 = {g₀}) (hA1 : A 1 = {g₁}) :
IsEFX v A

EFX for 2 agents and 2 goods: the allocation giving one good to each agent is EFX.

For any two goods g₀ and g₁, the allocation A 0 = {g₀}, A 1 = {g₁} satisfies EFX for both agents, provided each agent values the empty bundle at most their own good. This holds for any additive nonneg valuation (v.val i ∅ = 0 ≤ v.val i {g}).

Proof: Each bundle is a singleton. Removing the one element leaves ∅, so the EFX condition reduces to v.val j ∅ ≤ v.val j (A j), which holds by hypothesis.

General EFX existence for 2 agents #

source
theorem SocialChoice.FairDivision.Indivisible.efx_exists_two_agents {G : Type u_2} [Fintype G] [DecidableEq G] (w : AdditiveValuation (Fin 2) G) (hnn₀ : ∀ (g : G), 0 ≤ w.weight 0 g) (hnn₁ : ∀ (g : G), 0 ≤ w.weight 1 g) (allGoods : Finset G) :
∃ (A : Allocation (Fin 2) G), IsAllocation allGoods A ∧ IsEFX w.toValuation A

EFX existence for 2 agents (general m goods, additive nonneg valuations).