EconCSLib.SocialChoice.FairDivision.Divisible.Instance

Bundled semantic interfaces for divisible-goods fair division.

This file sits above the raw divisible allocation layer. It keeps Divisible.Allocation N Ω := FairDivision.Allocation N (Set Ω) and Divisible.IsAllocation as the low-level feasibility vocabulary, while exposing canonical bundled instance types for ordinal, cardinal, and measure-based divisible-goods problems.

structure SocialChoice.FairDivision.Divisible.Instance (N : Type u_1) (Ω : Type u_2) : Type (max u_1 u_2)

An ordinal divisible-goods instance.

The cake is represented by the ambient measurable space Ω, and shares are subsets of Ω.

• sharePref : N → Pref (Set Ω)

  Each agent's ordinal preference over cake pieces.

def SocialChoice.FairDivision.Divisible.Instance.feasible {N : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] [Fintype N] (_I : Instance N Ω) (A : Allocation N Ω) : Prop

Feasibility for a divisible instance: an allocation is a measurable partition of the cake.

Equations

• _I.feasible A = SocialChoice.FairDivision.Divisible.IsAllocation A

def SocialChoice.FairDivision.Divisible.Instance.toShareInstance {N : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] [Fintype N] (I : Instance N Ω) : ShareInstance N (Set Ω) (Set Ω)

View a divisible ordinal instance as a generic no-externality fair-division share instance. The resource is the whole cake Set.univ.

Equations

• One or more equations did not get rendered due to their size.

structure SocialChoice.FairDivision.Divisible.CardinalInstance (N : Type u_1) (Ω : Type u_2) : Type (max u_1 u_2)

A real-valued cardinal divisible-goods instance.

• utility : N → Set Ω → ℝ

  Utility assigned by each agent to each cake piece.

def SocialChoice.FairDivision.Divisible.CardinalInstance.feasible {N : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] [Fintype N] (_I : CardinalInstance N Ω) (A : Allocation N Ω) : Prop

Feasibility for a cardinal divisible instance.

Equations

• _I.feasible A = SocialChoice.FairDivision.Divisible.IsAllocation A

def SocialChoice.FairDivision.Divisible.CardinalInstance.toGenericCardinalInstance {N : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] [Fintype N] (I : CardinalInstance N Ω) : FairDivision.CardinalInstance N (Set Ω) (Set Ω)

View a divisible cardinal instance as a generic real-valued cardinal fair-division instance. The resource is the whole cake Set.univ.

Equations

• One or more equations did not get rendered due to their size.

def SocialChoice.FairDivision.Divisible.CardinalInstance.toShareInstance {N : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] [Fintype N] (I : CardinalInstance N Ω) : ShareInstance N (Set Ω) (Set Ω)

View a divisible cardinal instance as the induced generic ordinal no-externality instance.

Equations

• I.toShareInstance = I.toGenericCardinalInstance.toShareInstance

Instance-relative fairness and welfare wrappers

def SocialChoice.FairDivision.Divisible.CardinalInstance.IsEnvyFree {N : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] [Fintype N] (I : CardinalInstance N Ω) (A : Allocation N Ω) : Prop

Envy-freeness for a divisible cardinal instance.

Equations

• I.IsEnvyFree A = I.toGenericCardinalInstance.IsEnvyFree A

def SocialChoice.FairDivision.Divisible.CardinalInstance.IsProportional {N : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] [Fintype N] (I : CardinalInstance N Ω) (n : ℕ) (A : Allocation N Ω) : Prop

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

Equations

• I.IsProportional n A = I.toGenericCardinalInstance.IsProportional n Set.univ A

def SocialChoice.FairDivision.Divisible.CardinalInstance.IsEquitable {N : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] [Fintype N] (I : CardinalInstance N Ω) (A : Allocation N Ω) : Prop

Equitability for a divisible cardinal instance.

Equations

• I.IsEquitable A = I.toGenericCardinalInstance.IsEquitable A

def SocialChoice.FairDivision.Divisible.CardinalInstance.IsParetoOptimal {N : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] [Fintype N] (I : CardinalInstance N Ω) (A : Allocation N Ω) : Prop

Pareto optimality for a divisible cardinal instance.

Equations

• I.IsParetoOptimal A = I.toGenericCardinalInstance.IsParetoOptimal A

noncomputable def SocialChoice.FairDivision.Divisible.CardinalInstance.utilitarianWelfare {N : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] [Fintype N] (I : CardinalInstance N Ω) (A : Allocation N Ω) : ℝ

Utilitarian welfare for a divisible cardinal instance.

Equations

• I.utilitarianWelfare A = I.toGenericCardinalInstance.utilitarianWelfare A

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

Egalitarian welfare for a divisible cardinal instance.

Equations

• I.egalitarianWelfare A = I.toGenericCardinalInstance.egalitarianWelfare A

structure SocialChoice.FairDivision.Divisible.MeasureInstance (N : Type u_1) (Ω : Type u_2) [MeasurableSpace Ω] : Type (max u_1 u_2)

A measure-based divisible-goods instance.

• measure : N → MeasureTheory.Measure Ω

  Each agent's measure over cake pieces.

def SocialChoice.FairDivision.Divisible.MeasureInstance.toCakeValuation {N : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] (I : MeasureInstance N Ω) : CakeValuation N Ω ENNReal

The raw cake valuation induced by a measure instance.

Equations

• I.toCakeValuation = SocialChoice.FairDivision.Divisible.MeasureValuation I.measure

noncomputable def SocialChoice.FairDivision.Divisible.MeasureInstance.toCardinalInstance {N : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] (I : MeasureInstance N Ω) : CardinalInstance N Ω

The real-valued cardinal instance induced by measure values.

Equations

• I.toCardinalInstance = { utility := fun (i : N) (S : Set Ω) => ((I.measure i) S).toReal }

def SocialChoice.FairDivision.Divisible.MeasureInstance.feasible {N : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] [Fintype N] (_I : MeasureInstance N Ω) (A : Allocation N Ω) : Prop

Feasibility for a measure-based divisible instance. Like the ordinal and cardinal divisible cases, this depends only on the ambient cake: a feasible allocation is a measurable partition of Set.univ.

Equations

• _I.feasible A = SocialChoice.FairDivision.Divisible.IsAllocation A

noncomputable def SocialChoice.FairDivision.Divisible.MeasureInstance.toGenericCardinalInstance {N : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] [Fintype N] (I : MeasureInstance N Ω) : FairDivision.CardinalInstance N (Set Ω) (Set Ω)

View a measure instance as a generic real-valued cardinal fair-division instance.

Equations

• I.toGenericCardinalInstance = I.toCardinalInstance.toGenericCardinalInstance

noncomputable def SocialChoice.FairDivision.Divisible.MeasureInstance.toShareInstance {N : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] [Fintype N] (I : MeasureInstance N Ω) : ShareInstance N (Set Ω) (Set Ω)

View a measure instance as the induced generic ordinal no-externality instance.

Equations

• I.toShareInstance = I.toGenericCardinalInstance.toShareInstance

Instance-relative fairness wrappers

def SocialChoice.FairDivision.Divisible.MeasureInstance.IsEnvyFree {N : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] (I : MeasureInstance N Ω) (A : Allocation N Ω) : Prop

Envy-freeness for a measure-based divisible instance, stated in ENNReal.

Equations

• I.IsEnvyFree A = SocialChoice.FairDivision.Divisible.IsEnvyFree I.toCakeValuation A

theorem SocialChoice.FairDivision.Divisible.MeasureInstance.isEnvyFree_iff_toCardinalInstance_isEnvyFree {N : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] [Fintype N] (I : MeasureInstance N Ω) [∀ (i : N), MeasureTheory.IsFiniteMeasure (I.measure i)] (A : Allocation N Ω) : I.IsEnvyFree A ↔ I.toCardinalInstance.IsEnvyFree A

For finite measure instances, the raw ENNReal envy-freeness predicate agrees with the real-valued cardinal predicate induced by toReal.

def SocialChoice.FairDivision.Divisible.MeasureInstance.IsProportional {N : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] (I : MeasureInstance N Ω) (n : ℕ) (A : Allocation N Ω) : Prop

Proportionality for a measure-based divisible instance, stated in ENNReal.

Equations

• I.IsProportional n A = SocialChoice.FairDivision.Divisible.IsProportional n I.toCakeValuation A

def SocialChoice.FairDivision.Divisible.MeasureInstance.IsEquitable {N : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] (I : MeasureInstance N Ω) (A : Allocation N Ω) : Prop

Equitability for a measure-based divisible instance, stated in ENNReal.

Equations

• I.IsEquitable A = SocialChoice.FairDivision.Divisible.IsEquitable I.toCakeValuation A

theorem SocialChoice.FairDivision.Divisible.MeasureInstance.IsEnvyFree.isProportional {N : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] [Fintype N] (I : MeasureInstance N Ω) (A : Allocation N Ω) (ha : IsAllocation A) (hef : I.IsEnvyFree A) : I.IsProportional (Fintype.card N) A

Envy-freeness implies proportionality for complete measure-based divisible allocations.