EconCSLib.SocialChoice.FairDivision.Cardinal

Cardinal enrichments of the shared fair-division layer.

The primary interface here is the standard no-externality model CardinalInstance, where each agent assigns a real value to an individual share. It is independent from the ordinal ShareInstance layer; bridges derive ordinal preferences from utility when needed.

structure SocialChoice.FairDivision.CardinalInstance (N : Type u_1) (R : Type u_2) (S : Type u_3) : Type (max (max u_1 u_2) u_3)

A real-valued cardinal fair-division instance in the standard no-externality model.

• resource : R

  Resource-side data for the instance.

• feasible : Allocation N S → Prop

  Feasible allocations for the given resource data.

• utility : N → S → ℝ

  Utility assigned by each agent to each individual share.

def SocialChoice.FairDivision.CardinalInstance.inducedSharePref {N : Type u_1} {R : Type u_2} {S : Type u_3} (I : CardinalInstance N R S) : N → Pref S

The share preference induced by a cardinal utility, using the convention that higher utility means weakly better.

Equations

• I.inducedSharePref i = { rel := fun (s t : S) => I.utility i t ≤ I.utility i s, prop := ⋯ }

def SocialChoice.FairDivision.CardinalInstance.toShareInstance {N : Type u_1} {R : Type u_2} {S : Type u_3} (I : CardinalInstance N R S) : ShareInstance N R S

Convert a cardinal instance to the induced ordinal no-externality instance.

Equations

• I.toShareInstance = { resource := I.resource, feasible := I.feasible, sharePref := I.inducedSharePref }

def SocialChoice.FairDivision.CardinalInstance.UtilityRepresentsSharePref {N : Type u_1} {R : Type u_2} {S : Type u_3} (I₁ : ShareInstance N R S) (I₂ : CardinalInstance N R S) : Prop

An ordinal share instance is represented by a cardinal instance when its weak share preferences agree with the utility-induced weak order.

Equations

• SocialChoice.FairDivision.CardinalInstance.UtilityRepresentsSharePref I₁ I₂ = ∀ (i : N) (s t : S), (I₁.sharePref i).rel s t ↔ I₂.utility i t ≤ I₂.utility i s

Instance-relative fairness and welfare wrappers

def SocialChoice.FairDivision.CardinalInstance.IsEnvyFree {N : Type u_1} {R : Type u_2} {S : Type u_3} (I : CardinalInstance N R S) (A : Allocation N S) : Prop

Envy-freeness for a cardinal instance.

Equations

• I.IsEnvyFree A = SocialChoice.FairDivision.IsEnvyFree I.utility A

def SocialChoice.FairDivision.CardinalInstance.IsProportional {N : Type u_1} {R : Type u_2} {S : Type u_3} (I : CardinalInstance N R S) (n : ℕ) (whole : S) (A : Allocation N S) : Prop

Proportionality for a cardinal instance, relative to a distinguished whole share and a supplied population size.

Equations

• I.IsProportional n whole A = SocialChoice.FairDivision.IsProportional n whole I.utility A

def SocialChoice.FairDivision.CardinalInstance.IsEquitable {N : Type u_1} {R : Type u_2} {S : Type u_3} (I : CardinalInstance N R S) (A : Allocation N S) : Prop

Equitability for a cardinal instance.

Equations

• I.IsEquitable A = SocialChoice.FairDivision.IsEquitable I.utility A

def SocialChoice.FairDivision.CardinalInstance.IsParetoOptimal {N : Type u_1} {R : Type u_2} {S : Type u_3} (I : CardinalInstance N R S) (A : Allocation N S) : Prop

Pareto optimality for a cardinal instance, using the instance feasibility predicate.

Equations

• I.IsParetoOptimal A = SocialChoice.FairDivision.IsParetoOptimal I.feasible I.utility A

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

Utilitarian welfare for a cardinal instance.

Equations

• I.utilitarianWelfare A = SocialChoice.FairDivision.utilitarianWelfare I.utility A

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

Egalitarian welfare for a cardinal instance.

Equations

• I.egalitarianWelfare A = SocialChoice.FairDivision.egalitarianWelfare I.utility A

def SocialChoice.FairDivision.CardinalInstance.IsUtilitarianOptimal {N : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype N] (I : CardinalInstance N R S) (A : Allocation N S) : Prop

Utilitarian optimality for a cardinal instance, using the instance feasibility predicate.

Equations

• I.IsUtilitarianOptimal A = SocialChoice.FairDivision.IsUtilitarianOptimal I.feasible I.utility A

def SocialChoice.FairDivision.CardinalInstance.IsMaxmin {N : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype N] [Nonempty N] (I : CardinalInstance N R S) (A : Allocation N S) : Prop

Maximin optimality for a cardinal instance, using the instance feasibility predicate.

Equations

• I.IsMaxmin A = SocialChoice.FairDivision.IsMaxmin I.feasible I.utility A