Lean declarations

structure SocialChoice.FairDivision.ShareInstance EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Basic

structure ShareInstance (N R S : Type*) where
  /-- Resource-side data for the instance. -/
  resource : R
  /-- Feasible allocations for the given resource data. -/
  feasible : Allocation N S → Prop
  /-- Each agent's preference over individual shares. -/
  sharePref : N → Pref S

def SocialChoice.FairDivision.ShareInstance.toInstance EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Basic

def toInstance {N R S : Type*}
    (I : ShareInstance N R S) : Instance N R S where
  resource := I.resource
  feasible := I.feasible
  pref i :=
    { rel := fun A B => I.sharePref i (A i) (B i)
      prop :=
        { reflexive := fun A => I.sharePref i |>.prop.reflexive (A i)
          transitive := fun _ _ _ hAB hBC => I.sharePref i |>.prop.transitive hAB hBC
          total := fun A B => I.sharePref i |>.prop.total (A i) (B i) } }

Modules: EconCSLib.SocialChoice.FairDivision.Basic

Share Instance (No-Externality Model)

A share instance is a fair-division instance restricted to the no-externality model: each agent ranks only the share they personally receive, not the entire allocation.

In Lean: SocialChoice.FairDivision.ShareInstance N R S, with fields resource : R, feasible : Allocation N S → Prop, and sharePref : N → Pref S.

This is the standard input shape for textbook fair-division problems (envy-freeness, proportionality, MMS, etc., all formulated in terms of each agent's own share).

Lift to the full-allocation interface

There is a canonical embedding toInstance : ShareInstance N R S → Instance N R S ([[social_choice.fair_division.instance]]) that promotes share preferences to allocation preferences by comparing two allocations only through the evaluating agent's own share: $$ A \preceq_i B \iff A(i) \preceq_{\mathrm{share},i} B(i). $$

The promoted relation inherits reflexivity, transitivity, and totality pointwise from sharePref i, so the result is a valid Pref on allocations.

This lift is the bridge that makes the share-instance API a true special case of the generic allocation-preference instance, and lets the same solution concepts apply at both layers.

References

[AGT Chapter 11] Nisan, Roughgarden, Tardos, and Vazirani, Algorithmic Game Theory. No-externality fair-division model.

Share Instance (No-Externality Model)

Lift to the full-allocation interface

References

Used by

Also in