Documentation

Lean 4 Proof

theorem complementarity_alignment {ρ₁ ρ₂ : ℝ} (J : ℕ) (hJ : 2 ≤ J)
    (hρ₁ : ρ₁ < 1) (hρ₂ : ρ₂ < 1) (h12 : ρ₁ < ρ₂) :
    -- (a) K₂ < K₁
    curvatureK J ρ₂ < curvatureK J ρ₁
    -- (b) ε₂ < ε₁
    ∧ inequalityAversion ρ₂ < inequalityAversion ρ₁ := by
  exact no_tradeoff_welfare_interpretation J hJ hρ₁ hρ₂ h12

Dependency Graph

Location

thesis/CESProofs/Applications/SocialWelfare.lean:240

Module Section

CES as Atkinson Social Welfare Function

In the same file