EconCSLib.SocialChoice.FairDivision.Divisible.Existence #

Existence theorems for envy-free complete divisible allocations.

Main results #

proportional_exists — for any n agents with non-atomic finite measures on [0,1], a complete proportional allocation exists (each agent values their piece at ≥ 1/n of the cake)
ef_exists — for any n agents with non-atomic finite measures on [0,1], a complete envy-free allocation exists

Proof strategy for `ef_exists` (Stromquist 1980) #

We follow the proof of Stromquist, "How to Cut a Cake Fairly", Amer. Math. Monthly 87 (1980).

Setup #

The division simplex S = stdSimplex ℝ (Fin n) is the standard (n-1)-simplex. A point x ∈ S represents a way to divide the cake into n consecutive pieces: coordinate xᵢ ≥ 0 encodes the "fractional length" of the i-th piece, and ∑ xᵢ = 1. The actual cut points in ℝ are recovered via a fixed homeomorphism φ : (0,1) ≃ₜ ℝ; the i-th piece is φ((∑_{j<i} xⱼ, ∑_{j≤i} xⱼ]).

The face opposite vertex i is simplexFaceOpp i = {x ∈ S | xᵢ = 0}, the set of divisions where piece i is empty.

Key definitions #

For each agent j : Fin n and piece index i : Fin n:

strom_A i j — the preference set of agent j for piece i: the set of divisions x ∈ S where piece i achieves maximum value for agent j. This set is closed (by continuity of the value function, strom_value_continuous).
strom_B i j — the unique preference set: divisions where piece i is agent j's unique maximizer. This set is open (relative to S).
strom_U i — the agent preference union: ⋃ⱼ strom_B i j, the set of divisions where some agent uniquely prefers piece i. Each strom_U i is open and does not intersect simplexFaceOpp i.

Proof by KKM #

The proof splits into two cases:

Usual case (strom_U covers S): Apply kkm_open_cover to obtain a point x* ∈ ⋂ᵢ strom_U i. At x*, each piece i has a unique claimant among the agents, and the claimants are all distinct (since strom_B i j and strom_B i j' are disjoint for j ≠ j'). Assigning each agent their uniquely preferred piece yields an EF allocation.

Unusual case (strom_U does not cover S): Any uncovered division x has every agent indifferent between two or more pieces. We eliminate this by approximating the strom_A i j sets: choose irrationals α₀, …, αₙ₋₁ linearly independent over ℚ, and for a large M define modified preference sets strom_A' i j by intersecting strom_A i j with the half-open cells {x | xₖ ∈ [L/M + αⱼ, (L+1)/M + αⱼ)}. The resulting strom_U' sets DO cover S (the irrationality prevents coincidences), so the usual case applies. As M → ∞, the approximate fair divisions converge (by compactness of S) to a fair division for the original preferences.

References #

Stromquist, "How to Cut a Cake Fairly", Amer. Math. Monthly 87 (1980), pp. 640–644
Dubins–Spanier, "How to Cut a Cake Fairly", Amer. Math. Monthly 68 (1961), pp. 1–17
Su, "Rental Harmony: Sperner's Lemma in Fair Division", Amer. Math. Monthly (1999)
Nisan et al., Algorithmic Game Theory, Chapter 13

Proportional existence #

source

theorem SocialChoice.FairDivision.Divisible.proportional_exists {N : Type u_1} [Fintype N] [Nonempty N] (μ : N → MeasureTheory.Measure ↑unitInterval) [∀ (i : N), MeasureTheory.IsFiniteMeasure (μ i)] [∀ (i : N), MeasureTheory.NoAtoms (μ i)] :

∃ (A : Allocation N ↑unitInterval), IsAllocation A ∧ IsProportional (Fintype.card N) (MeasureValuation μ) A

Proportional allocations always exist for n agents with non-atomic finite measures on [0,1].

A proportional allocation assigns each agent a piece they value at ≥ 1/n of the total cake.

Proof sketch (moving knife, proportional variant):

By induction on n = Fintype.card N.

Base case (n = 1): The single agent receives the entire cake.

Inductive step: Given n agents, find a cut point t* ∈ [0,1] such that μ₀([0, t*]) = μ₀([0,1])/n. Assign agent 0 the piece [0, t*], which they value at exactly 1/n. Apply the inductive hypothesis to the remaining n-1 agents on (t*, 1], scaled to 1/(n-1) of the remainder.

Each agent's piece has value ≥ 1/n of their total measure on [0,1]:

Agent 0's piece: exactly μ₀([0,1])/n by construction.
Agent i > 0 (inductive hypothesis on restricted measures): value ≥ 1/(n-1) of remainder. Since the remainder has value ≥ (n-1)/n * μᵢ([0,1]) for agent i (they didn't cut, so the cut was possibly suboptimal for them), we get value ≥ 1/(n-1) * (n-1)/n * μᵢ([0,1]) = 1/n * μᵢ([0,1]).

Key Lean ingredients:

cut_exists (in DubinsSpanier.lean) — IVT lemma for placing a knife at any fraction
dubinsSpanierProportional — the inductive algorithm for Fin n agents
Fintype.equivFin N — bijection N ≃ Fin (Fintype.card N) to convert types

Proof: apply dubinsSpanierProportional with the measure family reindexed along the bijection e := Fintype.equivFin N, then transport the allocation back along e.

EF existence: Stromquist scaffolding #

This section develops the scaffolding for the Stromquist proof of ef_exists, following Stromquist (1980). The main components are:

The piece function strom_piece: maps a simplex point and a piece index to a subset of ℝ.
The value function strom_value: evaluates a measure on a piece.
The preference sets strom_A, strom_B, strom_U: closed/open subsets of the simplex encoding agent preferences.
The KKM application and the assignment of pieces to agents.

Design note: strom_A i j is defined on all of Fin n → ℝ (not restricted to the simplex). This ensures strom_B i j is genuinely open in the ambient space, which is required for the KKM open-cover theorem. The simplex constraint appears explicitly only in strom_A_covers and the KKM application.

Piece function and partition #

source

noncomputable def SocialChoice.FairDivision.Divisible.strom_piece (n : ℕ) (x : Fin n → ℝ) (i : Fin n) :

Set ℝ

The i-th piece at division x: the subset of ℝ assigned to piece i when the cake is divided according to x ∈ stdSimplex ℝ (Fin n).

Construction: Fix a homeomorphism φ : (0,1) ≃ₜ ℝ (e.g., φ(t) = tan(π(t - 1/2))). At division x, the i-th piece is φ((∑_{j<i} xⱼ, ∑_{j≤i} xⱼ]).

Equivalently for measures supported on [0,1]: piece i is the interval (∑_{j<i} xⱼ, ∑_{j≤i} xⱼ] in [0,1].

The key properties (stated as separate lemmas below) are:

The pieces partition ℝ (strom_piece_partition).
Each piece is measurable (strom_piece_measurable).
Piece i is empty iff xᵢ = 0 (strom_piece_empty_iff).

Equations

SocialChoice.FairDivision.Divisible.strom_piece n x i = Set.Ico (∑ j : Fin n with j < i, x j) (∑ j : Fin n with j ≤ i, x j)

Instances For

source

theorem SocialChoice.FairDivision.Divisible.strom_piece_partition (n : ℕ) (x : Fin n → ℝ) (hx : x ∈ stdSimplex ℝ (Fin n)) :

(∀ (i : Fin n), MeasurableSet (strom_piece n x i)) ∧ (∀ (i j : Fin n), i ≠ j → Disjoint (strom_piece n x i) (strom_piece n x j)) ∧ ⋃ (i : Fin n), strom_piece n x i = Set.Ico 0 1

The pieces at any division x ∈ stdSimplex ℝ (Fin n) form a measurable partition of Set.Ico 0 1 ⊆ ℝ. (They do not cover all of ℝ; see strom_usual_case for how the complement is handled when constructing a IsAllocation.)

source

theorem SocialChoice.FairDivision.Divisible.strom_piece_empty_iff (n : ℕ) (x : Fin n → ℝ) (hx : x ∈ stdSimplex ℝ (Fin n)) (i : Fin n) :

strom_piece n x i = ∅ ↔ x i = 0

Piece i is empty (measure zero for all agents) if and only if xᵢ = 0.

This is the measure-theoretic content of "face i corresponds to piece i being empty": at a point x in simplexFaceOpp i, the piece strom_piece n x i contains no mass.

Value function and its continuity #

source

noncomputable def SocialChoice.FairDivision.Divisible.strom_value (n : ℕ) (μ : Fin n → MeasureTheory.Measure ℝ) (x : Fin n → ℝ) (j i : Fin n) :

ℝ

The value agent j assigns to piece i at division x: strom_value μ x j i = μ j (strom_piece n x i).

Equations

SocialChoice.FairDivision.Divisible.strom_value n μ x j i = ((μ j) (SocialChoice.FairDivision.Divisible.strom_piece n x i)).toReal

Instances For

source

theorem SocialChoice.FairDivision.Divisible.strom_value_continuous (n : ℕ) (μ : Fin n → MeasureTheory.Measure ℝ) [∀ (i : Fin n), MeasureTheory.IsFiniteMeasure (μ i)] [∀ (i : Fin n), MeasureTheory.NoAtoms (μ i)] (j i : Fin n) :

Continuous fun (x : Fin n → ℝ) => strom_value n μ x j i

The value function x ↦ strom_value μ x j i is continuous on all of Fin n → ℝ.

Proof: The piece endpoints l(x) = ∑_{k<i} xk and r(x) = ∑_{k≤i} xk are linear (hence continuous) in x. The measure of the piece equals max (CDF_j(r(x)) - CDF_j(l(x))) 0 where CDF_j is the continuous CDF of μ j (continuous by cdfRealContinuous). The composition is continuous.

Preference sets #

Unique preference sets #

Agent preference union #

The usual case: KKM gives a fair assignment #

The unusual case: shifted coordinate cells #

Helper lemmas for the unusual case #

EF existence (general n agents) #

source

theorem SocialChoice.FairDivision.Divisible.ef_exists {N : Type u_1} [Fintype N] [Nonempty N] (μ : N → MeasureTheory.Measure ↑unitInterval) [∀ (i : N), MeasureTheory.IsFiniteMeasure (μ i)] [∀ (i : N), MeasureTheory.NoAtoms (μ i)] :

∃ (A : Allocation N ↑unitInterval), IsAllocation A ∧ IsEnvyFree (MeasureValuation μ) A

EF allocations always exist for any finite number of agents with non-atomic finite measures on [0,1].

This is the fundamental existence theorem of divisible fair division (Stromquist 1980).

Proof (via Stromquist's KKM argument, sketched):

Push each measure on [0,1] forward along Subtype.val : I → ℝ.
Reindex agents as Fin n (n = Fintype.card N) via Fintype.equivFin N.
Apply strom_unusual_case to get an EF allocation for Fin n agents. (strom_unusual_case subsumes the usual case: it handles both via the approximation argument, which reduces to strom_usual_case when the U sets already cover the simplex.)
Pull the allocation back to [0,1] along Subtype.val and transport it back along the bijection.