EconCSLib.SocialChoice.FairDivision.Divisible.Valuation

Valuation-side infrastructure for divisible goods (cake cutting).

This file contains the abstract cake-valuation interface, the standard measure-based specialization, and normalization vocabulary.

structure SocialChoice.FairDivision.Divisible.CakeValuation (N : Type u_1) (Ω : Type u_2) (V : Type u_3) : Type (max (max u_1 u_2) u_3)

An abstract cake valuation assigns a value in V to each agent-piece pair.

• val : N → Set Ω → V

  The valuation function: agent × cake-piece → value.

def SocialChoice.FairDivision.Divisible.MeasureValuation {N : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] (μ : N → MeasureTheory.Measure Ω) : CakeValuation N Ω ENNReal

A measure-based cake valuation: each agent's value for a piece is given by their personal measure μ i on the cake Ω.

Equations

• SocialChoice.FairDivision.Divisible.MeasureValuation μ = { val := fun (i : N) (S : Set Ω) => (μ i) S }

@[simp]

theorem SocialChoice.FairDivision.Divisible.MeasureValuation.val_empty {N : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] (μ : N → MeasureTheory.Measure Ω) (i : N) : (MeasureValuation μ).val i ∅ = 0

The value of the empty piece is zero.

theorem SocialChoice.FairDivision.Divisible.MeasureValuation.val_union {N : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] (μ : N → MeasureTheory.Measure Ω) (i : N) (S T : Set Ω) (hdisj : Disjoint S T) (ht : MeasurableSet T) : (MeasureValuation μ).val i (S ∪ T) = (MeasureValuation μ).val i S + (MeasureValuation μ).val i T

For disjoint measurable sets, MeasureValuation is additive.

theorem SocialChoice.FairDivision.Divisible.MeasureValuation.val_iUnion {N : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] (μ : N → MeasureTheory.Measure Ω) [Countable N] (i : N) (A : Allocation N Ω) (hdisj : ∀ (j k : N), j ≠ k → Disjoint (A j) (A k)) (hmeas : ∀ (j : N), MeasurableSet (A j)) : (MeasureValuation μ).val i (⋃ (j : N), A j) = ∑' (j : N), (MeasureValuation μ).val i (A j)

For a countably-indexed pairwise-disjoint family of measurable sets, MeasureValuation is countably additive (tsum).

def SocialChoice.FairDivision.Divisible.IsNormalized {N : Type u_1} {Ω : Type u_2} {V : Type u_3} [One V] (cv : CakeValuation N Ω V) : Prop

A normalized cake valuation: each agent values the whole cake at exactly 1.

Equations

• SocialChoice.FairDivision.Divisible.IsNormalized cv = ∀ (i : N), cv.val i Set.univ = 1

theorem SocialChoice.FairDivision.Divisible.IsNormalized.iff_isProbabilityMeasure {N : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] (μ : N → MeasureTheory.Measure Ω) : IsNormalized (MeasureValuation μ) ↔ ∀ (i : N), MeasureTheory.IsProbabilityMeasure (μ i)

For MeasureValuation, normalization is equivalent to every agent's measure being a probability measure.