EconCSLib.SocialChoice.FairDivision.Indivisible.Instance

Bundled semantic interfaces for indivisible-goods fair division.

This file sits above the raw indivisible allocation layer. It keeps Allocation N G := N → Finset G and IsAllocation as the low-level feasibility vocabulary, while exposing canonical bundled instance types for ordinal, cardinal, and additive indivisible-goods problems.

structure SocialChoice.FairDivision.Indivisible.Instance (N : Type u_1) (G : Type u_2) : Type (max u_1 u_2)

An ordinal indivisible-goods instance.

allGoods is the finite set of goods to allocate. Each agent ranks bundles of goods, represented as Finset G.

• allGoods : Finset G

  The goods that must be allocated.

• sharePref : N → Pref (Finset G)

  Each agent's ordinal preference over bundles.

def SocialChoice.FairDivision.Indivisible.Instance.feasible {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] (I : Instance N G) (A : Allocation N G) : Prop

Feasibility for an indivisible instance: an allocation partitions I.allGoods.

Equations

• I.feasible A = SocialChoice.FairDivision.Indivisible.IsAllocation I.allGoods A

def SocialChoice.FairDivision.Indivisible.Instance.toShareInstance {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] (I : Instance N G) : ShareInstance N (Finset G) (Finset G)

View an indivisible ordinal instance as a generic no-externality fair-division share instance.

Equations

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

structure SocialChoice.FairDivision.Indivisible.CardinalInstance (N : Type u_1) (G : Type u_2) : Type (max u_1 u_2)

A real-valued cardinal indivisible-goods instance.

• allGoods : Finset G

  The goods that must be allocated.

• utility : N → Finset G → ℝ

  Utility assigned by each agent to each bundle.

def SocialChoice.FairDivision.Indivisible.CardinalInstance.toValuation {N : Type u_1} {G : Type u_2} (I : CardinalInstance N G) : Valuation N G

The raw valuation induced by a cardinal indivisible instance.

Equations

• I.toValuation = { val := I.utility }

def SocialChoice.FairDivision.Indivisible.CardinalInstance.feasible {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] (I : CardinalInstance N G) (A : Allocation N G) : Prop

Feasibility for a cardinal indivisible instance.

Equations

• I.feasible A = SocialChoice.FairDivision.Indivisible.IsAllocation I.allGoods A

def SocialChoice.FairDivision.Indivisible.CardinalInstance.toGenericCardinalInstance {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] (I : CardinalInstance N G) : FairDivision.CardinalInstance N (Finset G) (Finset G)

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

Equations

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

def SocialChoice.FairDivision.Indivisible.CardinalInstance.toShareInstance {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] (I : CardinalInstance N G) : ShareInstance N (Finset G) (Finset G)

View an indivisible 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.Indivisible.CardinalInstance.IsEnvyFree {N : Type u_1} {G : Type u_2} (I : CardinalInstance N G) (A : Allocation N G) : Prop

Envy-freeness for an indivisible cardinal instance.

Equations

• I.IsEnvyFree A = SocialChoice.FairDivision.Indivisible.IsEnvyFree I.toValuation A

def SocialChoice.FairDivision.Indivisible.CardinalInstance.IsEF1 {N : Type u_1} {G : Type u_2} [DecidableEq G] (I : CardinalInstance N G) (A : Allocation N G) : Prop

Envy-freeness up to one good for an indivisible cardinal instance.

Equations

• I.IsEF1 A = SocialChoice.FairDivision.Indivisible.IsEF1 I.toValuation A

def SocialChoice.FairDivision.Indivisible.CardinalInstance.IsEFX {N : Type u_1} {G : Type u_2} [DecidableEq G] (I : CardinalInstance N G) (A : Allocation N G) : Prop

Envy-freeness up to any good for an indivisible cardinal instance.

Equations

• I.IsEFX A = SocialChoice.FairDivision.Indivisible.IsEFX I.toValuation A

def SocialChoice.FairDivision.Indivisible.CardinalInstance.IsProportional {N : Type u_1} {G : Type u_2} (I : CardinalInstance N G) (n : ℕ) (A : Allocation N G) : Prop

Proportionality for an indivisible cardinal instance, relative to the instance's full set of goods.

Equations

• I.IsProportional n A = SocialChoice.FairDivision.Indivisible.IsProportional n I.toValuation I.allGoods A

def SocialChoice.FairDivision.Indivisible.CardinalInstance.IsEquitable {N : Type u_1} {G : Type u_2} (I : CardinalInstance N G) (A : Allocation N G) : Prop

Equitability for an indivisible cardinal instance.

Equations

• I.IsEquitable A = SocialChoice.FairDivision.Indivisible.IsEquitable I.toValuation A

def SocialChoice.FairDivision.Indivisible.CardinalInstance.IsMaxminShare {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] (I : CardinalInstance N G) (A : Allocation N G) : Prop

Maximin-share guarantee for an indivisible cardinal instance.

Equations

• I.IsMaxminShare A = SocialChoice.FairDivision.Indivisible.IsMaxminShare I.toValuation I.allGoods A

def SocialChoice.FairDivision.Indivisible.CardinalInstance.IsParetoOptimal {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] (I : CardinalInstance N G) (A : Allocation N G) : Prop

Pareto optimality for an indivisible cardinal instance.

Equations

• I.IsParetoOptimal A = SocialChoice.FairDivision.Indivisible.IsParetoOptimal I.toValuation I.allGoods A

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

Utilitarian welfare for an indivisible cardinal instance.

Equations

• I.utilitarianWelfare A = SocialChoice.FairDivision.Indivisible.utilitarianWelfare I.toValuation A

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

Egalitarian welfare for an indivisible cardinal instance.

Equations

• I.egalitarianWelfare A = SocialChoice.FairDivision.Indivisible.egalitarianWelfare I.toValuation A

def SocialChoice.FairDivision.Indivisible.CardinalInstance.IsUtilitarianOptimal {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] (I : CardinalInstance N G) (A : Allocation N G) : Prop

Utilitarian optimality for an indivisible cardinal instance.

Equations

• I.IsUtilitarianOptimal A = SocialChoice.FairDivision.Indivisible.IsUtilitarianOptimal I.toValuation I.allGoods A

def SocialChoice.FairDivision.Indivisible.CardinalInstance.IsMaxmin {N : Type u_1} {G : Type u_2} [Fintype N] [Nonempty N] [DecidableEq G] (I : CardinalInstance N G) (A : Allocation N G) : Prop

Maximin social-welfare optimality for an indivisible cardinal instance.

Equations

• I.IsMaxmin A = SocialChoice.FairDivision.Indivisible.IsMaxmin I.toValuation I.allGoods A

structure SocialChoice.FairDivision.Indivisible.AdditiveInstance (N : Type u_1) (G : Type u_2) : Type (max u_1 u_2)

An additive indivisible-goods instance, represented by per-item weights.

• allGoods : Finset G

  The goods that must be allocated.

• weight : N → G → ℝ

  Per-agent, per-good weights.

def SocialChoice.FairDivision.Indivisible.AdditiveInstance.toAdditiveValuation {N : Type u_1} {G : Type u_2} (I : AdditiveInstance N G) : AdditiveValuation N G

The raw additive valuation induced by additive per-item weights.

Equations

• I.toAdditiveValuation = { weight := I.weight }

def SocialChoice.FairDivision.Indivisible.AdditiveInstance.toValuation {N : Type u_1} {G : Type u_2} (I : AdditiveInstance N G) : Valuation N G

The abstract valuation induced by additive per-item weights.

Equations

• I.toValuation = I.toAdditiveValuation.toValuation

def SocialChoice.FairDivision.Indivisible.AdditiveInstance.toCardinalInstance {N : Type u_1} {G : Type u_2} (I : AdditiveInstance N G) : CardinalInstance N G

The cardinal instance induced by additive per-item weights.

Equations

• I.toCardinalInstance = { allGoods := I.allGoods, utility := I.toValuation.val }

def SocialChoice.FairDivision.Indivisible.AdditiveInstance.toGenericCardinalInstance {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] (I : AdditiveInstance N G) : FairDivision.CardinalInstance N (Finset G) (Finset G)

View an additive indivisible instance as a generic real-valued cardinal fair-division instance.

Equations

• I.toGenericCardinalInstance = I.toCardinalInstance.toGenericCardinalInstance

def SocialChoice.FairDivision.Indivisible.AdditiveInstance.toShareInstance {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] (I : AdditiveInstance N G) : ShareInstance N (Finset G) (Finset G)

View an additive indivisible instance as the induced generic ordinal no-externality instance.

Equations

• I.toShareInstance = I.toGenericCardinalInstance.toShareInstance

Instance-relative fairness wrappers

def SocialChoice.FairDivision.Indivisible.AdditiveInstance.IsEnvyFree {N : Type u_1} {G : Type u_2} (I : AdditiveInstance N G) (A : Allocation N G) : Prop

Envy-freeness for an additive indivisible instance.

Equations

• I.IsEnvyFree A = SocialChoice.FairDivision.Indivisible.IsEnvyFree I.toValuation A

def SocialChoice.FairDivision.Indivisible.AdditiveInstance.IsEF1 {N : Type u_1} {G : Type u_2} [DecidableEq G] (I : AdditiveInstance N G) (A : Allocation N G) : Prop

Envy-freeness up to one good for an additive indivisible instance.

Equations

• I.IsEF1 A = SocialChoice.FairDivision.Indivisible.IsEF1 I.toValuation A

def SocialChoice.FairDivision.Indivisible.AdditiveInstance.IsEFX {N : Type u_1} {G : Type u_2} [DecidableEq G] (I : AdditiveInstance N G) (A : Allocation N G) : Prop

Envy-freeness up to any good for an additive indivisible instance.

Equations

• I.IsEFX A = SocialChoice.FairDivision.Indivisible.IsEFX I.toValuation A

def SocialChoice.FairDivision.Indivisible.AdditiveInstance.IsProportional {N : Type u_1} {G : Type u_2} (I : AdditiveInstance N G) (n : ℕ) (A : Allocation N G) : Prop

Proportionality for an additive indivisible instance.

Equations

• I.IsProportional n A = SocialChoice.FairDivision.Indivisible.IsProportional n I.toValuation I.allGoods A

def SocialChoice.FairDivision.Indivisible.AdditiveInstance.IsEquitable {N : Type u_1} {G : Type u_2} (I : AdditiveInstance N G) (A : Allocation N G) : Prop

Equitability for an additive indivisible instance.

Equations

• I.IsEquitable A = SocialChoice.FairDivision.Indivisible.IsEquitable I.toValuation A

def SocialChoice.FairDivision.Indivisible.AdditiveInstance.IsMaxminShare {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] (I : AdditiveInstance N G) (A : Allocation N G) : Prop

Maximin-share guarantee for an additive indivisible instance.

Equations

• I.IsMaxminShare A = SocialChoice.FairDivision.Indivisible.IsMaxminShare I.toValuation I.allGoods A

def SocialChoice.FairDivision.Indivisible.AdditiveInstance.IsParetoOptimal {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] (I : AdditiveInstance N G) (A : Allocation N G) : Prop

Pareto optimality for an additive indivisible instance.

Equations

• I.IsParetoOptimal A = SocialChoice.FairDivision.Indivisible.IsParetoOptimal I.toValuation I.allGoods A

noncomputable def SocialChoice.FairDivision.Indivisible.AdditiveInstance.utilitarianWelfare {N : Type u_1} {G : Type u_2} [Fintype N] (I : AdditiveInstance N G) (A : Allocation N G) : ℝ

Utilitarian welfare for an additive indivisible instance.

Equations

• I.utilitarianWelfare A = SocialChoice.FairDivision.Indivisible.utilitarianWelfare I.toValuation A

noncomputable def SocialChoice.FairDivision.Indivisible.AdditiveInstance.egalitarianWelfare {N : Type u_1} {G : Type u_2} [Fintype N] [Nonempty N] (I : AdditiveInstance N G) (A : Allocation N G) : ℝ

Egalitarian welfare for an additive indivisible instance.

Equations

• I.egalitarianWelfare A = SocialChoice.FairDivision.Indivisible.egalitarianWelfare I.toValuation A

def SocialChoice.FairDivision.Indivisible.AdditiveInstance.IsUtilitarianOptimal {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] (I : AdditiveInstance N G) (A : Allocation N G) : Prop

Utilitarian optimality for an additive indivisible instance.

Equations

• I.IsUtilitarianOptimal A = SocialChoice.FairDivision.Indivisible.IsUtilitarianOptimal I.toValuation I.allGoods A

def SocialChoice.FairDivision.Indivisible.AdditiveInstance.IsMaxmin {N : Type u_1} {G : Type u_2} [Fintype N] [Nonempty N] [DecidableEq G] (I : AdditiveInstance N G) (A : Allocation N G) : Prop

Maximin social-welfare optimality for an additive indivisible instance.

Equations

• I.IsMaxmin A = SocialChoice.FairDivision.Indivisible.IsMaxmin I.toValuation I.allGoods A

def SocialChoice.FairDivision.Indivisible.AdditiveInstance.feasible {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] (I : AdditiveInstance N G) (A : Allocation N G) : Prop

Feasibility for an additive indivisible instance.

Equations

• I.feasible A = SocialChoice.FairDivision.Indivisible.IsAllocation I.allGoods A