Lean declarations

structure SocialChoice.FairDivision.Indivisible.AdditiveInstance EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Indivisible.Instance
An additive indivisible-goods instance, represented by per-item weights.
```
structure AdditiveInstance (N G : Type*) where
  /-- The goods that must be allocated. -/
  allGoods : Finset G
  /-- Per-agent, per-good weights. -/
  weight : N → G → ℝ
```
def SocialChoice.FairDivision.Indivisible.AdditiveInstance.toAdditiveValuation EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Indivisible.Instance
The raw additive valuation induced by additive per-item weights.
```
def toAdditiveValuation {N G : Type*}
    (I : AdditiveInstance N G) : AdditiveValuation N G where
  weight := I.weight
```
def SocialChoice.FairDivision.Indivisible.AdditiveInstance.toValuation EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Indivisible.Instance
The abstract valuation induced by additive per-item weights.
```
def toValuation {N G : Type*}
    (I : AdditiveInstance N G) : Valuation N G :=
  I.toAdditiveValuation.toValuation
```
def SocialChoice.FairDivision.Indivisible.AdditiveInstance.toCardinalInstance EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Indivisible.Instance
The cardinal instance induced by additive per-item weights.
```
def toCardinalInstance {N G : Type*}
    (I : AdditiveInstance N G) : CardinalInstance N G where
  allGoods := I.allGoods
  utility := I.toValuation.val
```

def SocialChoice.FairDivision.Indivisible.AdditiveInstance.toGenericCardinalInstance EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Indivisible.Instance

def toGenericCardinalInstance {N G : Type*} [Fintype N] [DecidableEq G]
    (I : AdditiveInstance N G) :
    SocialChoice.FairDivision.CardinalInstance N (Finset G) (Finset G) :=
  I.toCardinalInstance.toGenericCardinalInstance

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

def toShareInstance {N G : Type*} [Fintype N] [DecidableEq G]
    (I : AdditiveInstance N G) :
    SocialChoice.FairDivision.ShareInstance N (Finset G) (Finset G) :=
  I.toGenericCardinalInstance.toShareInstance

Modules: EconCSLib.SocialChoice.FairDivision.Indivisible.Instance

Indivisible Additive Instance

An indivisible additive instance equips each agent with per-item weights $w(i, g) \in \mathbb{R}$, with the bundle utility computed additively: $$ v_i(S) = \sum_{g \in S} w(i, g). $$

In Lean: structure SocialChoice.FairDivision.Indivisible.AdditiveInstance N G with a weight field plus the outer good set allGoods : Finset G.

Conversions

Five conversions tie the additive-instance layer into the rest of the stack:

toAdditiveValuation — view the weights as an AdditiveValuation ([[social_choice.fair_division.indivisible.additive_valuation]]).
toValuation — compose with AdditiveValuation.toValuation to get a bare Valuation.
toCardinalInstance — view as an indivisible cardinal instance ([[social_choice.fair_division.indivisible.cardinal_instance]]) with $\mathrm{utility}\ i\ S = \sum_g w(i, g)$.
toGenericCardinalInstance — view as a generic real-valued cardinal fair-division instance.
toShareInstance — view as the underlying ordinal share instance.

Instance-keyed wrappers

Same as for the cardinal layer ([[social_choice.fair_division.indivisible.cardinal_instance]]), all fairness and welfare predicates are re-exported at the additive instance level. The bundled round-robin ([[social_choice.fair_division.indivisible.round_robin_alloc]]) and envy-cycle ([[social_choice.fair_division.indivisible.envy_cycle_algorithm]]) rules are stated against AdditiveInstance, providing algorithm-by-instance call sites.

References

[AGT Chapter 11] Nisan, Roughgarden, Tardos, and Vazirani, Algorithmic Game Theory. Additive instances in indivisible fair division.

Indivisible Additive Instance

Conversions

Instance-keyed wrappers

References

Also in