EconCSLib.SocialChoice.FairDivision.Divisible.DubinsSpanier

The Dubins–Spanier moving-knife algorithm for n-agent proportional divisible allocation.

Algorithm (informal)

Given n agents with non-atomic finite measures μ₀, …, μ_{n-1} on [0,1]:

1. For each agent i, find a threshold tᵢ ∈ [0,1] with μᵢ([0, tᵢ]) = μᵢ([0,1]) / n.

2. Let i* = argmin { tᵢ : i ∈ [n] } and t* = tᵢ*.

3. Assign agent i* the piece [0, t*].

4. Restrict each remaining agent j ≠ i* to (t*, 1] and apply the algorithm recursively with n - 1 agents.

Why proportionality holds

• Agent i*: by construction, μᵢ*([0, t*]) = μᵢ*([0,1])/n. ✓

• Remaining agent j: since t* ≤ tⱼ, μⱼ([0, t*]) ≤ μⱼ([0,1])/n, so μⱼ((t*, 1]) ≥ (n-1)/n · μⱼ([0,1]). By induction on the remaining n - 1 agents, agent j's piece has value at least μⱼ([0,1])/n. ✓

Main results

• cut_exists — IVT: for any 0 < c < μ([0,1]), there exists t ∈ [0,1] with μ([0,t]) = c.
• dubinsSpanierProportional — proportional allocations always exist for n ≥ 1 agents.

Status

All lemmas and theorems are fully proved, including ds_step (the moving-knife inductive step) which constructs the full allocation via Fin.insertNth and proves partition validity and proportionality using ennreal_prop_step.

References

• Dubins–Spanier, "How to Cut a Cake Fairly", Amer. Math. Monthly (1961)
• Nisan et al., Algorithmic Game Theory, Chapter 13

Helpers for the unit-interval model

IVT lemmas for measures

theorem SocialChoice.FairDivision.Divisible.cut_exists (μ : MeasureTheory.Measure ↑unitInterval) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.NoAtoms μ] (c : ℝ) (hc_pos : 0 < c) (hc_lt : c < (μ Set.univ).toReal) : ∃ (t : ↑unitInterval), (μ (Set.Iic t)).toReal = c

Intermediate Value Theorem for measures on [0,1]: for a finite non-atomic measure μ on the unit interval and any target 0 < c < μ([0,1]), there exists t ∈ [0,1] such that the initial segment Set.Iic t has value exactly c.

This is the analytic step used by the Dubins–Spanier moving-knife argument in its standard unit-interval formulation.

ENNReal proportionality arithmetic

Inductive proportional existence (Fin n)

Main induction

Main theorem

theorem SocialChoice.FairDivision.Divisible.dubinsSpanierProportional (n : ℕ) (hn : 0 < n) (μ : Fin n → MeasureTheory.Measure ↑unitInterval) [∀ (i : Fin n), MeasureTheory.IsFiniteMeasure (μ i)] [∀ (i : Fin n), MeasureTheory.NoAtoms (μ i)] : ∃ (A : Allocation (Fin n) ↑unitInterval), IsAllocation A ∧ IsProportional n (MeasureValuation μ) A

Dubins–Spanier: proportional allocations always exist for n ≥ 1 agents with non-atomic finite measures on [0,1].

For any n ≥ 1 agents (μ : Fin n → Measure I) with IsFiniteMeasure and NoAtoms, there is a complete measurable partition A of [0,1] such that every agent i values their piece A i at at least 1/n of the whole cake:

∀ i, μ i Set.univ ≤ n · μ i (A i).

Proof: induction on n using ds_one (base) and ds_step (inductive step).

theorem SocialChoice.FairDivision.Divisible.dubinsSpanier_exists_proportional_allocation (n : ℕ) (hn : 0 < n) (M : MeasureInstance (Fin n) ↑unitInterval) [∀ (i : Fin n), MeasureTheory.IsFiniteMeasure (M.measure i)] [∀ (i : Fin n), MeasureTheory.NoAtoms (M.measure i)] : ∃ (A : Allocation (Fin n) ↑unitInterval), IsAllocation A ∧ M.IsProportional n A

Bundled-instance form of Dubins-Spanier proportional existence.

noncomputable def SocialChoice.FairDivision.Divisible.dubinsSpanierRule (n : ℕ) (hn : 0 < n) (M : MeasureInstance (Fin n) ↑unitInterval) [∀ (i : Fin n), MeasureTheory.IsFiniteMeasure (M.measure i)] [∀ (i : Fin n), MeasureTheory.NoAtoms (M.measure i)] : { A : Allocation (Fin n) ↑unitInterval // IsAllocation A }

The Dubins-Spanier rule on bundled measure instances. It chooses one of the proportional allocations supplied by the constructive existence proof.

Equations

• SocialChoice.FairDivision.Divisible.dubinsSpanierRule n hn M = ⟨Classical.choose ⋯, ⋯⟩

theorem SocialChoice.FairDivision.Divisible.dubinsSpanierRule_isProportional (n : ℕ) (hn : 0 < n) (M : MeasureInstance (Fin n) ↑unitInterval) [∀ (i : Fin n), MeasureTheory.IsFiniteMeasure (M.measure i)] [∀ (i : Fin n), MeasureTheory.NoAtoms (M.measure i)] : M.IsProportional n ↑(dubinsSpanierRule n hn M)

The bundled Dubins-Spanier rule is proportional.