Lean declarations

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

A real-valued cardinal indivisible-goods instance.

structure CardinalInstance (N G : Type*) where
  /-- The goods that must be allocated. -/
  allGoods : Finset G
  /-- Utility assigned by each agent to each bundle. -/
  utility : N → Finset G → ℝ

def SocialChoice.FairDivision.Indivisible.CardinalInstance.toValuation EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Indivisible.Instance
The raw valuation induced by a cardinal indivisible instance.
```
def toValuation {N G : Type*}
    (I : CardinalInstance N G) : Valuation N G where
  val := I.utility
```

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

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

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

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

def SocialChoice.FairDivision.Indivisible.CardinalInstance.IsEnvyFree EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Indivisible.Instance
Envy-freeness for an indivisible cardinal instance.
```
def IsEnvyFree {N G : Type*}
    (I : CardinalInstance N G) (A : Allocation N G) : Prop :=
  SocialChoice.FairDivision.Indivisible.IsEnvyFree I.toValuation A
```
def SocialChoice.FairDivision.Indivisible.CardinalInstance.IsEF1 EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Indivisible.Instance
Envy-freeness up to one good for an indivisible cardinal instance.
```
def IsEF1 {N G : Type*} [DecidableEq G]
    (I : CardinalInstance N G) (A : Allocation N G) : Prop :=
  SocialChoice.FairDivision.Indivisible.IsEF1 I.toValuation A
```
def SocialChoice.FairDivision.Indivisible.CardinalInstance.IsEFX EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Indivisible.Instance
Envy-freeness up to any good for an indivisible cardinal instance.
```
def IsEFX {N G : Type*} [DecidableEq G]
    (I : CardinalInstance N G) (A : Allocation N G) : Prop :=
  SocialChoice.FairDivision.Indivisible.IsEFX I.toValuation A
```

def SocialChoice.FairDivision.Indivisible.CardinalInstance.IsProportional EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Indivisible.Instance

def IsProportional {N G : Type*}
    (I : CardinalInstance N G) (n : ℕ) (A : Allocation N G) : Prop :=
  SocialChoice.FairDivision.Indivisible.IsProportional n I.toValuation I.allGoods A

def SocialChoice.FairDivision.Indivisible.CardinalInstance.IsEquitable EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Indivisible.Instance
Equitability for an indivisible cardinal instance.
```
def IsEquitable {N G : Type*}
    (I : CardinalInstance N G) (A : Allocation N G) : Prop :=
  SocialChoice.FairDivision.Indivisible.IsEquitable I.toValuation A
```
def SocialChoice.FairDivision.Indivisible.CardinalInstance.IsMaxminShare EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Indivisible.Instance
Maximin-share guarantee for an indivisible cardinal instance.
```
def IsMaxminShare {N G : Type*} [Fintype N] [DecidableEq G]
    (I : CardinalInstance N G) (A : Allocation N G) : Prop :=
  SocialChoice.FairDivision.Indivisible.IsMaxminShare I.toValuation I.allGoods A
```

def SocialChoice.FairDivision.Indivisible.CardinalInstance.IsParetoOptimal EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Indivisible.Instance

Pareto optimality for an indivisible cardinal instance.

def IsParetoOptimal {N G : Type*} [Fintype N] [DecidableEq G]
    (I : CardinalInstance N G) (A : Allocation N G) : Prop :=
  SocialChoice.FairDivision.Indivisible.IsParetoOptimal I.toValuation I.allGoods A

def SocialChoice.FairDivision.Indivisible.CardinalInstance.IsUtilitarianOptimal EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Indivisible.Instance

Utilitarian optimality for an indivisible cardinal instance.

def IsUtilitarianOptimal {N G : Type*} [Fintype N] [DecidableEq G]
    (I : CardinalInstance N G) (A : Allocation N G) : Prop :=
  SocialChoice.FairDivision.Indivisible.IsUtilitarianOptimal I.toValuation I.allGoods A

def SocialChoice.FairDivision.Indivisible.CardinalInstance.IsMaxmin EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Indivisible.Instance
Maximin social-welfare optimality for an indivisible cardinal instance.
```
def IsMaxmin {N G : Type*} [Fintype N] [Nonempty N] [DecidableEq G]
    (I : CardinalInstance N G) (A : Allocation N G) : Prop :=
  SocialChoice.FairDivision.Indivisible.IsMaxmin I.toValuation I.allGoods A
```

Modules: EconCSLib.SocialChoice.FairDivision.Indivisible.Instance

Indivisible Cardinal Instance

An indivisible cardinal instance assigns each agent a real-valued utility for every bundle: $$ \mathrm{utility} : N \to \mathrm{Finset}\ G \to \mathbb{R}. $$

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

Bridges

toValuation — wrap as a bare Valuation ([[social_choice.fair_division.indivisible.valuation]]).
toGenericCardinalInstance — view as a generic real-valued cardinal fair-division instance ([[social_choice.fair_division.cardinal_instance]]) over share type $\mathrm{Finset}\ G$ and resource value allGoods.
toShareInstance — compose with inducedSharePref to get the underlying indivisible ordinal instance ([[social_choice.fair_division.indivisible.ordinal_instance]]).

Instance-keyed wrappers

A full menu of instance-keyed fairness and welfare predicates is re-exported:

IsEnvyFree, IsEF1, IsEFX, IsProportional, IsEquitable, IsMaxminShare — fairness predicates.
IsParetoOptimal, IsUtilitarianOptimal, IsMaxmin — efficiency / welfare-optimality predicates.

All wrappers are definitional pass-throughs to the corresponding generic or Indivisible-prefixed predicates with $I.\mathrm{utility}$ and feasibility supplied from the instance.

References

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

Used by

Indivisible Additive Instance

Indivisible Cardinal Instance

Bridges

Instance-keyed wrappers

References

Used by

Also in