Social Choice.Fair Division.Indivisible.Mms

8 nodes 3 formalized 5 staged

Theorem IsMaxminShare ↔ IsAlphaMMS 1 staged

Lemma MMS Value — Basic Bounds staged

Definition Maximin Share (MMS) Allocation formalized

Definition Maximin Share Value formalized

Theorem PROP ⇒ MMS (Additive Valuations, Complete Allocations) staged

Theorem PROP ⇒ α-MMS (Additive Valuations) staged

Definition α-MMS Allocation formalized

Theorem α-MMS — Monotonicity and Endpoint Lemmas staged