Documentation

Lean 4 Proof

theorem curvature_is_aversion_times_diversity (J : ℕ) (ρ : ℝ) :
    curvatureK J ρ = inequalityAversion ρ * ((↑J - 1) / ↑J) := by
  simp only [curvatureK, inequalityAversion]; ring

Dependency Graph

Location

thesis/CESProofs/Applications/SocialWelfare.lean:68

Module Section

CES as Atkinson Social Welfare Function

In the same file