EconCSLib.SocialChoice.FairDivision.Welfare

Shared social-welfare objectives for the standard no-externality cardinal fair-division layer.

noncomputable def SocialChoice.FairDivision.utilitarianWelfare {N : Type u_1} {S : Type u_2} [Fintype N] (u : N → S → ℝ) (A : Allocation N S) : ℝ

Utilitarian welfare: the sum of agents' utilities from their own shares.

Equations

• SocialChoice.FairDivision.utilitarianWelfare u A = ∑ i : N, u i (A i)

noncomputable def SocialChoice.FairDivision.egalitarianWelfare {N : Type u_1} {S : Type u_2} [Fintype N] [Nonempty N] (u : N → S → ℝ) (A : Allocation N S) : ℝ

Egalitarian welfare: the minimum utility among agents.

Equations

• SocialChoice.FairDivision.egalitarianWelfare u A = Finset.univ.inf' ⋯ fun (i : N) => u i (A i)

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

Utilitarian optimality: no feasible allocation has larger utilitarian welfare.

Equations

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

def SocialChoice.FairDivision.IsMaxmin {N : Type u_1} {S : Type u_2} [Fintype N] [Nonempty N] (feasible : Allocation N S → Prop) (u : N → S → ℝ) (A : Allocation N S) : Prop

Maximin optimality: no feasible allocation has larger egalitarian welfare.

Equations

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

theorem SocialChoice.FairDivision.utilitarianWelfare_mono {N : Type u_1} {S : Type u_2} [Fintype N] (u : N → S → ℝ) (A B : Allocation N S) (h : ∀ (i : N), u i (A i) ≤ u i (B i)) : utilitarianWelfare u A ≤ utilitarianWelfare u B

Utilitarian welfare is monotone: pointwise improvement implies welfare improvement.

@[simp]

theorem SocialChoice.FairDivision.utilitarianWelfare_unique {N : Type u_1} {S : Type u_2} [Fintype N] [Unique N] (u : N → S → ℝ) (A : Allocation N S) : utilitarianWelfare u A = u default (A default)

For a unique agent, utilitarian welfare is just that agent's utility.

theorem SocialChoice.FairDivision.egalitarianWelfare_le {N : Type u_1} {S : Type u_2} [Fintype N] [Nonempty N] (u : N → S → ℝ) (A : Allocation N S) (i : N) : egalitarianWelfare u A ≤ u i (A i)

Egalitarian welfare is bounded above by each agent's utility.

theorem SocialChoice.FairDivision.nsmul_egalitarianWelfare_le_utilitarianWelfare {N : Type u_1} {S : Type u_2} [Fintype N] [Nonempty N] (u : N → S → ℝ) (A : Allocation N S) (hle : ∀ (i : N), egalitarianWelfare u A ≤ u i (A i)) : Fintype.card N • egalitarianWelfare u A ≤ utilitarianWelfare u A

Without division, egalitarian welfare is bounded above by utilitarian welfare multiplied by the number of agents.