EconCSLib.SocialChoice.FairDivision.Divisible.Allocation

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

This file contains only the share/allocation representation and measurable partition predicates. Valuation-side material lives in Divisible.Valuation.

@[reducible, inline]

abbrev SocialChoice.FairDivision.Divisible.Allocation (N : Type u_1) (Ω : Type u_2) : Type (max u_1 u_2)

A divisible allocation assigns each agent i : N a piece (a measurable subset) of the cake Ω.

Equations

• SocialChoice.FairDivision.Divisible.Allocation N Ω = SocialChoice.FairDivision.Allocation N (Set Ω)

structure SocialChoice.FairDivision.Divisible.IsAllocation {N : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] [Fintype N] (A : Allocation N Ω) : Prop

A complete divisible allocation is a measurable partition of the cake.

• measurable (i : N) : MeasurableSet (A i)

  Each piece is a measurable set.

• disjoint (i j : N) : i ≠ j → Disjoint (A i) (A j)

  Distinct agents receive disjoint pieces.

• cover : ⋃ (i : N), A i = Set.univ

  Every point of the cake belongs to some agent's piece.

theorem SocialChoice.FairDivision.Divisible.IsAllocation.mem_iUnion {N : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] [Fintype N] {A : Allocation N Ω} (ha : IsAllocation A) (x : Ω) : ∃ (i : N), x ∈ A i

Every point of the cake belongs to the piece of some agent.

def SocialChoice.FairDivision.Divisible.IsContiguousAllocation {N : Type u_1} (A : Allocation N ℝ) : Prop

A contiguous allocation on ℝ: each agent's piece is an interval (an order-connected subset of ℝ).

Equations

• SocialChoice.FairDivision.Divisible.IsContiguousAllocation A = ∀ (i : N), (A i).OrdConnected