Lean declarations

structure SocialChoice.FairDivision.Divisible.CardinalInstance EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Divisible.Instance
A real-valued cardinal divisible-goods instance.
```
structure CardinalInstance (N Ω : Type*) where
  /-- Utility assigned by each agent to each cake piece. -/
  utility : N → Set Ω → ℝ
```

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

def toGenericCardinalInstance {N Ω : Type*} [MeasurableSpace Ω] [Fintype N]
    (I : CardinalInstance N Ω) :
    SocialChoice.FairDivision.CardinalInstance N (Set Ω) (Set Ω) where
  resource := Set.univ
  feasible := fun A => IsAllocation A
  utility := I.utility

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

def toShareInstance {N Ω : Type*} [MeasurableSpace Ω] [Fintype N]
    (I : CardinalInstance N Ω) :
    SocialChoice.FairDivision.ShareInstance N (Set Ω) (Set Ω) :=
  I.toGenericCardinalInstance.toShareInstance

def SocialChoice.FairDivision.Divisible.CardinalInstance.IsEnvyFree EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Divisible.Instance

Envy-freeness for a divisible cardinal instance.

def IsEnvyFree {N Ω : Type*} [MeasurableSpace Ω] [Fintype N]
    (I : CardinalInstance N Ω) (A : Allocation N Ω) : Prop :=
  SocialChoice.FairDivision.CardinalInstance.IsEnvyFree
    I.toGenericCardinalInstance A

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

Proportionality for a divisible cardinal instance, relative to the whole cake.

def IsProportional {N Ω : Type*} [MeasurableSpace Ω] [Fintype N]
    (I : CardinalInstance N Ω) (n : ℕ) (A : Allocation N Ω) : Prop :=
  SocialChoice.FairDivision.CardinalInstance.IsProportional
    I.toGenericCardinalInstance n Set.univ A

def SocialChoice.FairDivision.Divisible.CardinalInstance.IsEquitable EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Divisible.Instance

Equitability for a divisible cardinal instance.

def IsEquitable {N Ω : Type*} [MeasurableSpace Ω] [Fintype N]
    (I : CardinalInstance N Ω) (A : Allocation N Ω) : Prop :=
  SocialChoice.FairDivision.CardinalInstance.IsEquitable
    I.toGenericCardinalInstance A

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

Pareto optimality for a divisible cardinal instance.

def IsParetoOptimal {N Ω : Type*} [MeasurableSpace Ω] [Fintype N]
    (I : CardinalInstance N Ω) (A : Allocation N Ω) : Prop :=
  SocialChoice.FairDivision.CardinalInstance.IsParetoOptimal
    I.toGenericCardinalInstance A

def SocialChoice.FairDivision.Divisible.CardinalInstance.utilitarianWelfare EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Divisible.Instance

Utilitarian welfare for a divisible cardinal instance.

noncomputable def utilitarianWelfare {N Ω : Type*}
    [MeasurableSpace Ω] [Fintype N]
    (I : CardinalInstance N Ω) (A : Allocation N Ω) : ℝ :=
  SocialChoice.FairDivision.CardinalInstance.utilitarianWelfare
    I.toGenericCardinalInstance A

def SocialChoice.FairDivision.Divisible.CardinalInstance.egalitarianWelfare EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Divisible.Instance

Egalitarian welfare for a divisible cardinal instance.

noncomputable def egalitarianWelfare {N Ω : Type*}
    [MeasurableSpace Ω] [Fintype N] [Nonempty N]
    (I : CardinalInstance N Ω) (A : Allocation N Ω) : ℝ :=
  SocialChoice.FairDivision.CardinalInstance.egalitarianWelfare
    I.toGenericCardinalInstance A

Modules: EconCSLib.SocialChoice.FairDivision.Divisible.Instance

Divisible Cardinal Instance

A divisible cardinal instance assigns each agent a real-valued utility for every measurable cake piece: $$ \mathrm{utility} : N \to \mathrm{Set}\ \Omega \to \mathbb{R}. $$

In Lean: structure SocialChoice.FairDivision.Divisible.CardinalInstance N Ω.

Bridges

toGenericCardinalInstance — view as a generic real-valued cardinal fair-division instance ([[social_choice.fair_division.cardinal_instance]]) over share type $\mathrm{Set}\ \Omega$ and resource $\mathrm{Set.univ}$.
toShareInstance — compose with inducedSharePref to get the underlying divisible ordinal instance ([[social_choice.fair_division.divisible.ordinal_instance]]).

Instance-keyed fairness and welfare

A complete set of instance-keyed wrappers re-exports the generic predicates:

IsEnvyFree A, IsProportional n A, IsEquitable A, IsParetoOptimal A — fairness / efficiency predicates pinned to the current instance's utility and feasibility.
utilitarianWelfare A, egalitarianWelfare A — welfare aggregations ([[social_choice.fair_division.utilitarian_welfare]], [[social_choice.fair_division.egalitarian_welfare]]).

All wrappers are definitional passes through to the corresponding generic predicates with $I.\mathrm{utility}$ and feasibility supplied from the instance.

References

[AGT Chapter 13] Nisan, Roughgarden, Tardos, and Vazirani, Algorithmic Game Theory. Cardinal valuations in cake-cutting.

Used by

Divisible Measure Instance

Divisible Cardinal Instance

Bridges

Instance-keyed fairness and welfare

References

Used by

Also in