Lean declarations

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

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

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

lemma utilitarianWelfare_mono
    (v : Valuation N G) (A B : Allocation N G)
    (h : ∀ i : N, v.val i (A i) ≤ v.val i (B i)) :
    utilitarianWelfare v A ≤ utilitarianWelfare v B

lemma SocialChoice.FairDivision.Indivisible.utilitarianWelfare_unique EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Indivisible.SocialWelfare
```
lemma utilitarianWelfare_unique [Unique N]
    (v : Valuation N G) (A : Allocation N G) :
    utilitarianWelfare v A = v.val default (A default)
```

Modules: EconCSLib.SocialChoice.FairDivision.Indivisible.SocialWelfare

Indivisible Utilitarian Welfare

Specialisation of the generic utilitarian welfare ([[social_choice.fair_division.utilitarian_welfare]]) to the indivisible setting: for a valuation $v$ and allocation $A$, $$ W_{\mathrm{util}}(v, A) = \sum_{i \in N} v_i(A(i)). $$

The same definition utilitarianWelfare (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:

IsUtilitarianOptimal (abbrev): no complete allocation (IsAllocation allGoods B) has strictly larger utilitarian welfare.

Basic lemmas

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

utilitarianWelfare_mono: pointwise improvement implies welfare improvement.
utilitarianWelfare_unique (@[simp]): for Unique N, welfare equals the single agent's utility.

Relation to fairness

Utilitarian welfare optimization can conflict with fairness: maximizing total welfare may produce highly unequal allocations (give everything to the agent with highest per-item values). The Nash welfare (geometric mean instead of arithmetic mean) is the standard mediator — its maximizer is known to be EF1 + PO under additive valuations (Caragiannis et al. 2019). EconCSLib does not yet formalize Nash welfare; this welfare module is the additive-mean counterpart.

References

[AGT Chapter 11] Nisan, Roughgarden, Tardos, and Vazirani, Algorithmic Game Theory. Utilitarian welfare for indivisible goods.
Caragiannis, Kurokawa, Moulin, Procaccia, Shah, and Wang (2019). "The Unreasonable Fairness of Maximum Nash Welfare". EC.

Indivisible Utilitarian Welfare

Basic lemmas

Relation to fairness

References

Also in