EconCSLib.SocialChoice.FairDivision.Fairness

Shared fairness and efficiency predicates for the standard cardinal no-externality fair-division layer.

Only genuinely share-generic notions belong here. Item-removal notions such as EF1/EFX and cake-specific measurability or contiguity conditions belong in lower specialized modules.

def SocialChoice.FairDivision.IsEnvyFree {N : Type u_1} {S : Type u_2} (u : N → S → ℝ) (A : Allocation N S) : Prop

Envy-free: every agent weakly prefers their own share to every other agent's share.

Equations

• SocialChoice.FairDivision.IsEnvyFree u A = ∀ (i j : N), u i (A j) ≤ u i (A i)

def SocialChoice.FairDivision.IsProportional {N : Type u_1} {S : Type u_2} (n : ℕ) (whole : S) (u : N → S → ℝ) (A : Allocation N S) : Prop

Proportional: each agent values their share at least 1 / n of a distinguished whole share, stated without division.

Equations

• SocialChoice.FairDivision.IsProportional n whole u A = ∀ (i : N), u i whole ≤ ↑n * u i (A i)

def SocialChoice.FairDivision.IsEquitable {N : Type u_1} {S : Type u_2} (u : N → S → ℝ) (A : Allocation N S) : Prop

Equitable: all agents obtain the same utility from their own shares.

Equations

• SocialChoice.FairDivision.IsEquitable u A = ∀ (i j : N), u i (A i) = u j (A j)

def SocialChoice.FairDivision.IsParetoOptimal {N : Type u_1} {S : Type u_2} (feasible : Allocation N S → Prop) (u : N → S → ℝ) (A : Allocation N S) : Prop

Pareto optimal: there is no feasible allocation that weakly improves every agent and strictly improves at least one.

Equations

• SocialChoice.FairDivision.IsParetoOptimal feasible u A = ¬∃ (B : SocialChoice.FairDivision.Allocation N S), feasible B ∧ (∀ (i : N), u i (A i) ≤ u i (B i)) ∧ ∃ (i : N), u i (A i) < u i (B i)