Documentation

Lean 4 Proof

theorem surplus_loss_is_welfare_loss {ρ H : ℝ} {J : ℕ} :
    surplusLoss ρ H J = inequalityAversion ρ * (H - 1 / ↑J) := by
  simp only [surplusLoss, inequalityAversion]

Dependency Graph

Location

thesis/CESProofs/Applications/SocialWelfare.lean:226

Module Section

CES as Atkinson Social Welfare Function

In the same file