Lean declarations

abbrev SocialChoice.FairDivision.Indivisible.IsMaxmin EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Indivisible.SocialWelfare

abbrev IsMaxmin [Fintype N] [Nonempty N] [DecidableEq G]
    (v : Valuation N G) (allGoods : Finset G) (A : Allocation N G) : Prop :=
  SocialChoice.FairDivision.IsMaxmin (fun B => IsAllocation allGoods B) v.val A

lemma SocialChoice.FairDivision.Indivisible.egalitarianWelfare_le EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Indivisible.SocialWelfare
Egalitarian welfare is bounded above by any agent's bundle value.
```
lemma egalitarianWelfare_le [Nonempty N]
    (v : Valuation N G) (A : Allocation N G) (i : N) :
    egalitarianWelfare v A ≤ v.val i (A i)
```

lemma SocialChoice.FairDivision.Indivisible.nsmul_egalitarianWelfare_le_utilitarianWelfare EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Indivisible.SocialWelfare

lemma nsmul_egalitarianWelfare_le_utilitarianWelfare
    [Nonempty N]
    (v : Valuation N G) (A : Allocation N G)
    (hle : ∀ i : N, egalitarianWelfare v A ≤ v.val i (A i)) :
    Fintype.card N • egalitarianWelfare v A ≤ utilitarianWelfare v A

Modules: EconCSLib.SocialChoice.FairDivision.Indivisible.SocialWelfare

Indivisible Egalitarian (Maximin) Welfare

Specialisation of the generic egalitarian welfare ([[social_choice.fair_division.egalitarian_welfare]]) to the indivisible setting: for a valuation $v$ and allocation $A$ on a finite nonempty agent type, $$ W_{\mathrm{egal}}(v, A) = \min_{i \in N} v_i(A(i)). $$

The same definition egalitarianWelfare (under SocialChoice.FairDivision) applies, taking v.val for the per-agent utility function and the indivisible allocation ([[social_choice.fair_division.indivisible.allocation]]) for the share assignment.

The instance-keyed optimality predicate is wrapped here:

IsMaxmin (abbrev): no complete allocation (IsAllocation allGoods B) has strictly larger egalitarian welfare.

Basic lemmas

Re-exported from the generic layer with the indivisible-friendly hypotheses:

egalitarianWelfare_le: $W_{\mathrm{egal}}(v, A) \le v_i(A(i))$ for every agent $i$.
nsmul_egalitarianWelfare_le_utilitarianWelfare: combined with [[social_choice.fair_division.indivisible.utilitarian_welfare]], $|N| \cdot W_{\mathrm{egal}} \le W_{\mathrm{util}}$.

Relation to MMS

Egalitarian welfare is a global maximin (over all $i$, take the worst-off), while MMS ([[social_choice.fair_division.indivisible.maximin_share]]) is a per-agent maximin (over self-partitions). They are conceptually related but distinct: $W_{\mathrm{egal}}$ depends only on the bundle values, while MMS additionally depends on each agent's full valuation structure.

References

[AGT Chapter 11] Nisan, Roughgarden, Tardos, and Vazirani, Algorithmic Game Theory. Egalitarian welfare for indivisible goods.

Indivisible Egalitarian (Maximin) Welfare

Basic lemmas

Relation to MMS

References

Also in