Lean declarations

structure SocialChoice.FairDivision.Divisible.MeasureInstance EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Divisible.Instance
A measure-based divisible-goods instance.
```
structure MeasureInstance (N Ω : Type*) [MeasurableSpace Ω] where
  /-- Each agent's measure over cake pieces. -/
  measure : N → Measure Ω
```
def SocialChoice.FairDivision.Divisible.MeasureInstance.toCakeValuation EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Divisible.Instance
The raw cake valuation induced by a measure instance.
```
def toCakeValuation {N Ω : Type*} [MeasurableSpace Ω]
    (I : MeasureInstance N Ω) : CakeValuation N Ω ENNReal :=
  MeasureValuation I.measure
```
def SocialChoice.FairDivision.Divisible.MeasureInstance.toCardinalInstance EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Divisible.Instance
The real-valued cardinal instance induced by measure values.
```
noncomputable def toCardinalInstance {N Ω : Type*} [MeasurableSpace Ω]
    (I : MeasureInstance N Ω) : CardinalInstance N Ω where
  utility := fun i S => (I.measure i S).toReal
```

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

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

def SocialChoice.FairDivision.Divisible.MeasureInstance.IsEnvyFree EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Divisible.Instance
Envy-freeness for a measure-based divisible instance, stated in `ENNReal`.
```
def IsEnvyFree {N Ω : Type*} [MeasurableSpace Ω]
    (I : MeasureInstance N Ω) (A : Allocation N Ω) : Prop :=
  SocialChoice.FairDivision.Divisible.IsEnvyFree I.toCakeValuation A
```
def SocialChoice.FairDivision.Divisible.MeasureInstance.IsProportional EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Divisible.Instance
Proportionality for a measure-based divisible instance, stated in `ENNReal`.
```
def IsProportional {N Ω : Type*} [MeasurableSpace Ω]
    (I : MeasureInstance N Ω) (n : ℕ) (A : Allocation N Ω) : Prop :=
  SocialChoice.FairDivision.Divisible.IsProportional n I.toCakeValuation A
```
def SocialChoice.FairDivision.Divisible.MeasureInstance.IsEquitable EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Divisible.Instance
Equitability for a measure-based divisible instance, stated in `ENNReal`.
```
def IsEquitable {N Ω : Type*} [MeasurableSpace Ω]
    (I : MeasureInstance N Ω) (A : Allocation N Ω) : Prop :=
  SocialChoice.FairDivision.Divisible.IsEquitable I.toCakeValuation A
```
theorem SocialChoice.FairDivision.Divisible.MeasureInstance.IsEnvyFree.isProportional EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Divisible.Instance
Envy-freeness implies proportionality for complete measure-based divisible allocations.
```
theorem IsEnvyFree.isProportional {N Ω : Type*}
    [MeasurableSpace Ω] [Fintype N]
    (I : MeasureInstance N Ω)
    (A : Allocation N Ω)
    (ha : IsAllocation A)
    (hef : I.IsEnvyFree A) :
    I.IsProportional (Fintype.card N) A
```

Modules: EconCSLib.SocialChoice.FairDivision.Divisible.Instance

Divisible Measure Instance

A divisible measure instance equips each agent with a (typically finite, non-atomic) measure on the cake $\Omega$: $$ \mathrm{measure} : N \to \mathrm{Measure}\ \Omega. $$

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

Conversions

Three canonical conversions tie the measure-instance into the rest of the stack:

toCakeValuation — view the family as a cake valuation ([[social_choice.fair_division.divisible.measure_valuation]]) with $\mathrm{ENNReal}$ values.
toCardinalInstance — push the measures to real-valued utilities via .toReal, giving a divisible cardinal instance ([[social_choice.fair_division.divisible.cardinal_instance]]).
toShareInstance — compose with the cardinal-induced share preference to obtain a no-externality share instance.

Instance-keyed fairness predicates

Re-exports of the divisible fairness predicates ([[social_choice.fair_division.divisible.envy_free]]) keyed on the instance: IsEnvyFree A, IsProportional n A, IsEquitable A. These are stated in $\mathrm{ENNReal}$ (the natural ambient ring for measure values), with a translation to the real-valued cardinal form provided by [[social_choice.fair_division.divisible.measure_instance_ef_iff_real]].

The basic implication IsEnvyFree ⇒ IsProportional lifts directly from the cake-valuation level ([[social_choice.fair_division.divisible.ef_implies_proportional]]); the instance-level wrapper is MeasureInstance.IsEnvyFree.isProportional.

The existence theorems ([[social_choice.fair_division.divisible.measure_instance_existence]]) are stated at this layer.

References

[AGT Chapter 13] Nisan, Roughgarden, Tardos, and Vazirani, Algorithmic Game Theory. Measure-based cake-cutting instances.

Divisible Measure Instance

Conversions

Instance-keyed fairness predicates

References

Used by

Also in