Lean declarations

structure SocialChoice.FairDivision.Indivisible.Instance EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Indivisible.Instance

structure Instance (N G : Type*) where
  /-- The goods that must be allocated. -/
  allGoods : Finset G
  /-- Each agent's ordinal preference over bundles. -/
  sharePref : N → Pref (Finset G)

def SocialChoice.FairDivision.Indivisible.Instance.toShareInstance EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Indivisible.Instance

def toShareInstance {N G : Type*} [Fintype N] [DecidableEq G]
    (I : Instance N G) :
    SocialChoice.FairDivision.ShareInstance N (Finset G) (Finset G) where
  resource := I.allGoods
  feasible := fun A => IsAllocation I.allGoods A
  sharePref := I.sharePref

Modules: EconCSLib.SocialChoice.FairDivision.Indivisible.Instance

Indivisible Ordinal Instance

An indivisible ordinal instance is the no-externality share model specialized to discrete-item allocation: each agent's preference is an ordinal preference on bundles $\mathrm{Finset}\ G$.

In Lean: structure SocialChoice.FairDivision.Indivisible.Instance N G with a sharePref : N → Pref (Finset G) field plus the outer good set allGoods : Finset G.

Feasibility is the partition predicate [[social_choice.fair_division.indivisible.allocation]].

Bridge to the generic share-instance API

Indivisible.Instance.toShareInstance (with [Fintype N] [DecidableEq G]) views the indivisible ordinal instance as a generic no-externality share instance ([[social_choice.fair_division.share_instance]]) over share type $\mathrm{Finset}\ G$ and resource value allGoods. This lets all generic share-instance solution concepts apply.

This wrapper layer parallels the divisible analogue ([[social_choice.fair_division.divisible.ordinal_instance]]) — both plug into the same shared social-choice infrastructure via toShareInstance.

References

[AGT Chapter 11] Nisan, Roughgarden, Tardos, and Vazirani, Algorithmic Game Theory. Indivisible-goods instances.

Indivisible Ordinal Instance

Bridge to the generic share-instance API

References

Also in