EconCSLib.SocialChoice.FairDivision.Indivisible.MMS

Maximin share (MMS) value and α-MMS approximations for indivisible goods.

Valuations and approximation ratios are real-valued throughout this file.

The full-MMS predicate ("Is allocation A fair under MMS?") is IsMaxminShare, defined in Fairness.lean alongside EF, EF1, EFX, and PROP. This file adds:

• the numerical MMS value mmsValue (the actual worst-bundle value an agent can guarantee by self-partitioning),
• the α-MMS approximation predicate IsAlphaMMS (every agent receives ≥ α fraction of their MMS value), and
• basic results connecting these to IsMaxminShare and to each other.

Main definitions

• FairDivision.mmsValue v allGoods i — the MMS value of agent i: sup_{B : n-partition} inf_{j : N} v_i(B_j).
• FairDivision.IsAlphaMMS α v allGoods A — α-MMS: every agent receives ≥ α times their MMS value.

Key results

Proved:

• iInf_partition_le_mmsValue — min-bundle of any complete allocation ≤ MMS value.
• mmsValue_le_of_forall — MMS value ≤ any upper bound on partition minimums.
• mmsValue_nonneg — MMS value is nonneg for nonneg valuations ([Fintype G]).
• mmsValue_le_proportional_share_additive — n * mmsValue ≤ v_i(G).
• isMaxminShare_iff_isAlphaMMS_one — IsMaxminShare coincides with IsAlphaMMS 1.
• isAlphaMMS_zero — 0-MMS is trivially satisfied for nonneg valuations.
• isAlphaMMS_mono_alpha — α-MMS is monotone decreasing in α.
• IsMaxminShare.isAlphaMMS — full MMS implies α-MMS for 0 ≤ α ≤ 1.
• IsProportional.isAlphaMMS_additive — PROP implies α-MMS for all 0 ≤ α ≤ 1.

Fairness hierarchy

For additive valuations with complete allocations:

EF → EFX → EF1 → PROP → MMS → α-MMS  (0 ≤ α ≤ 1)

Unlike EF, EF1, and PROP, full MMS is not always achievable for n ≥ 3 agents [Procaccia-Wang 2014]. However, (3/4)-MMS is always achievable [Garg-Taki 2021].

References

• Budish — "The Combinatorial Assignment Problem" (JPE 2011) [MMS concept]
• Procaccia, Wang — "Fair Enough: Guaranteeing Approximate Maximin Shares" (EC 2014)
• Amanatidis, Markakis, Nikzad, Saberi — "Approximation Algorithms for Computing Maximin Share Allocations" (ACM TALG 2017)
• Garg, Taki — "An Improved Approximation Algorithm for Maximin Shares" (EC 2021)

MMS value

noncomputable def SocialChoice.FairDivision.Indivisible.mmsValue {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] (v : Valuation N G) (allGoods : Finset G) (i : N) : ℝ

The maximin share (MMS) value of agent i with respect to valuation v and good set allGoods.

mmsValue v allGoods i = sup_{B : n-partition} inf_{j : N} v_i(B_j).

Intuitively: the best (highest) minimum-bundle value agent i can guarantee by proposing a complete n-partition of allGoods. The outer iSup ranges over all complete allocations {B // IsAllocation allGoods B}; the inner iInf ranges over all agent indices j : N (the bundle labels).

The corresponding predicate ("did agent i receive at least their MMS value?") is IsMaxminShare in Fairness.lean. See isMaxminShare_iff_isAlphaMMS_one for the connection.

If no complete allocation exists (e.g., N = ∅), iSup over the empty subtype yields sSup ∅ = 0 in ℝ. Use [Nonempty N] to ensure a complete allocation exists.

[Budish 2011; AGT Ch.11]

Equations

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

IsAlphaMMS — approximate MMS allocation

def SocialChoice.FairDivision.Indivisible.IsAlphaMMS {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 α-MMS if every agent receives at least α times their MMS value.

IsAlphaMMS α v allGoods A ↔ ∀ i, α * mmsValue v allGoods i ≤ v.val i (A i).

The scalar α : ℝ quantifies approximation quality:

• α = 1: full MMS, equivalent to IsMaxminShare from Fairness.lean (see isMaxminShare_iff_isAlphaMMS_one).
• α = 3/4: always achievable for additive valuations (see exists_isAlphaMMS_threefourths).
• α = 0: trivially satisfied for nonneg valuations (see isAlphaMMS_zero).

[Budish 2011; Amanatidis et al. 2017; Garg-Taki 2021]

Equations

• SocialChoice.FairDivision.Indivisible.IsAlphaMMS α v allGoods A = ∀ (i : N), α * SocialChoice.FairDivision.Indivisible.mmsValue v allGoods i ≤ v.val i (A i)

Properties of mmsValue

theorem SocialChoice.FairDivision.Indivisible.iInf_partition_le_mmsValue {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] (v : Valuation N G) (allGoods : Finset G) (i : N) (B : Allocation N G) (hB : IsAllocation allGoods B) (hbdd : BddAbove (Set.range fun (X : { A : Allocation N G // IsAllocation allGoods A }) => ⨅ (j : N), v.val i (↑X j))) : ⨅ (j : N), v.val i (B j) ≤ mmsValue v allGoods i

The min-bundle value of any complete allocation is at most the MMS value.

For any complete allocation B: iInf_{j : N} v_i(B_j) ≤ mmsValue v allGoods i.

Requires BddAbove of the range of all per-allocation minimums, which holds when [Fintype G] (finitely many partitions).

[Budish 2011]

theorem SocialChoice.FairDivision.Indivisible.mmsValue_le_of_forall {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] (v : Valuation N G) (allGoods : Finset G) (i : N) (hne : Nonempty { A : Allocation N G // IsAllocation allGoods A }) (ub : ℝ) (h : ∀ (B : Allocation N G), IsAllocation allGoods B → ⨅ (j : N), v.val i (B j) ≤ ub) : mmsValue v allGoods i ≤ ub

The MMS value is at most any upper bound on all per-allocation minimum bundle values.

If ub is an upper bound — for every complete allocation B, iInf_j v_i(B_j) ≤ ub — then mmsValue v allGoods i ≤ ub.

hne is needed because ciSup_le requires the index type to be nonempty.

theorem SocialChoice.FairDivision.Indivisible.mmsValue_nonneg {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] [Fintype G] (v : Valuation N G) (allGoods : Finset G) (i : N) (hne : Nonempty { A : Allocation N G // IsAllocation allGoods A }) (hnonneg : ∀ (S : Finset G), 0 ≤ v.val i S) : 0 ≤ mmsValue v allGoods i

For nonneg valuations with at least one complete allocation, the MMS value is nonneg.

hne ensures the iSup is nonempty. [Fintype G] makes the allocation subtype [Finite], enabling Finite.le_ciSup without a separate BddAbove hypothesis.

theorem SocialChoice.FairDivision.Indivisible.mmsValue_le_proportional_share_additive {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] (w : AdditiveValuation N G) (allGoods : Finset G) (i : N) (hne : Nonempty { A : Allocation N G // IsAllocation allGoods A }) : ↑(Fintype.card N) * mmsValue w.toValuation allGoods i ≤ w.toValuation.val i allGoods

For additive valuations, the MMS value is at most the proportional share: n * mmsValue ≤ v_i(allGoods).

Proof: For any complete B, min_j v_i(B_j) ≤ avg_j v_i(B_j) = v_i(allGoods)/n (minimum ≤ average). Since this bound holds for every B, it holds for the supremum mmsValue = sup_B min_j v_i(B_j). Uses mmsValue_le_of_forall.

i : N guarantees Fintype.card N ≥ 1, so division by n is safe.

[Budish 2011]

Connection to IsMaxminShare and α-MMS

theorem SocialChoice.FairDivision.Indivisible.isMaxminShare_iff_isAlphaMMS_one {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] [Nonempty N] [Fintype G] (v : Valuation N G) (allGoods : Finset G) (A : Allocation N G) (hne : Nonempty { A' : Allocation N G // IsAllocation allGoods A' }) : IsMaxminShare v allGoods A ↔ IsAlphaMMS 1 v allGoods A

IsMaxminShare from Fairness.lean coincides with IsAlphaMMS 1.

→ direction (IsMaxminShare → IsAlphaMMS 1): for every complete B, there exists j with v_i(B_j) ≤ v_i(A_i), so iInf_j v_i(B_j) ≤ v_i(A_i). Then ciSup_le gives mmsValue ≤ v_i(A_i), and 1 * mmsValue = mmsValue by one_mul.

← direction (IsAlphaMMS 1 → IsMaxminShare): for any complete B, iInf_j v_i(B_j) ≤ mmsValue ≤ v_i(A_i). Since N is Nonempty and Fintype, the infimum is achieved at some j*, giving v_i(B_{j*}) ≤ v_i(A_i).

[Nonempty N] ensures iInf is nonempty. [Fintype G] makes the allocation subtype [Finite], enabling Finite.le_ciSup in the ← direction. hne is required by the → direction (to call ciSup_le).

Monotonicity and basic implications for α-MMS

theorem SocialChoice.FairDivision.Indivisible.isAlphaMMS_mono_alpha {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] (v : Valuation N G) (allGoods : Finset G) (A : Allocation N G) (α β : ℝ) (hβα : β ≤ α) (hmms_nn : ∀ (i : N), 0 ≤ mmsValue v allGoods i) (hα : IsAlphaMMS α v allGoods A) : IsAlphaMMS β v allGoods A

α-MMS is monotone decreasing in α: if A is α-MMS and β ≤ α, then A is β-MMS.

Proof: β * mmsValue ≤ α * mmsValue ≤ v_i(A_i) since β ≤ α and mmsValue ≥ 0.

theorem SocialChoice.FairDivision.Indivisible.isAlphaMMS_zero {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] (v : Valuation N G) (allGoods : Finset G) (A : Allocation N G) (hnonneg : ∀ (i : N) (S : Finset G), 0 ≤ v.val i S) : IsAlphaMMS 0 v allGoods A

Every allocation trivially satisfies 0-MMS for nonneg valuations.

0 * mmsValue = 0 ≤ v_i(A_i) by zero_mul and nonnegativity.

theorem SocialChoice.FairDivision.Indivisible.IsMaxminShare.isAlphaMMS {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] [Nonempty N] [Fintype G] (v : Valuation N G) (allGoods : Finset G) (A : Allocation N G) (hne : Nonempty { A' : Allocation N G // IsAllocation allGoods A' }) (hMMS : IsMaxminShare v allGoods A) (α : ℝ) (hα_le : α ≤ 1) (hmms_nn : ∀ (i : N), 0 ≤ mmsValue v allGoods i) : IsAlphaMMS α v allGoods A

IsMaxminShare implies α-MMS for α ≤ 1 and nonneg MMS values.

Proportionality implies α-MMS

theorem SocialChoice.FairDivision.Indivisible.IsProportional.isAlphaMMS_additive {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] [Nonempty N] [Fintype G] (w : AdditiveValuation N G) {allGoods : Finset G} {A : Allocation N G} (hne : Nonempty { A' : Allocation N G // IsAllocation allGoods A' }) (hProp : IsProportional (Fintype.card N) w.toValuation allGoods A) (α : ℝ) (hα_le : α ≤ 1) (hmms_nn : ∀ (i : N), 0 ≤ mmsValue w.toValuation allGoods i) : IsAlphaMMS α w.toValuation allGoods A

PROP implies α-MMS for additive valuations and α ≤ 1.

Follows by chaining: IsProportional.isMaxminShare → isMaxminShare_iff_isAlphaMMS_one.mp → IsMaxminShare.isAlphaMMS.

[Budish 2011]