Lean declarations

structure SocialChoice.FairDivision.Divisible.CakeValuation EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Divisible.Valuation
An abstract cake valuation assigns a value in `V` to each agent-piece pair.
```
structure CakeValuation (N Ω V : Type*) where
  /-- The valuation function: agent × cake-piece → value. -/
  val : N → Set Ω → V
```
def SocialChoice.FairDivision.Divisible.IsNormalized EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Divisible.Valuation
A normalized cake valuation: each agent values the whole cake at exactly `1`.
```
def IsNormalized {N Ω V : Type*} [One V] (cv : CakeValuation N Ω V) : Prop :=
  ∀ i : N, cv.val i Set.univ = 1
```

Modules: EconCSLib.SocialChoice.FairDivision.Divisible.Valuation

Cake Valuation

A cake valuation assigns a value in some ordered value type $V$ to each agent–piece pair $(i, S)$ with $S \subseteq \Omega$: $$ \mathrm{val} : N \to \mathrm{Set}\ \Omega \to V. $$

In Lean: structure SocialChoice.FairDivision.Divisible.CakeValuation N Ω V carrying a single field val.

The value type $V$ stays polymorphic because the canonical instance — measure-based valuations ([[social_choice.fair_division.divisible.measure_valuation]]) — takes values in ENNReal, while real-valued bundled interfaces use $\mathbb{R}$.

Normalization

A cake valuation is normalized if every agent values the whole cake at $1$: $$ \forall i \in N,\ \mathrm{val}(i, \Omega) = 1. $$

In Lean: IsNormalized, requiring [One V].

For a measure-valuation $\mu_i$, normalization is equivalent to each $\mu_i$ being a probability measure ([[social_choice.fair_division.divisible.normalized_iff_probability]]).

Normalized cake valuations are the standard setting for comparing proportionality bounds, MMS values, and welfare aggregates across agents.

References

[AGT Chapter 13] Nisan, Roughgarden, Tardos, and Vazirani, Algorithmic Game Theory. Valuations on cake pieces.
Robertson, J. M. and Webb, W. A. (1998). Cake-Cutting Algorithms.

Cake Valuation

Normalization

References

Used by

Also in