Documentation

Lean 4 Proof

theorem no_tradeoff_welfare_interpretation {ρ₁ ρ₂ : ℝ} (J : ℕ) (hJ : 2 ≤ J)
    (_hρ₁ : ρ₁ < 1) (_hρ₂ : ρ₂ < 1) (h12 : ρ₁ < ρ₂) :
    -- (a) Lower ρ → higher K
    curvatureK J ρ₂ < curvatureK J ρ₁
    -- (b) Lower ρ → higher ε
    ∧ inequalityAversion ρ₂ < inequalityAversion ρ₁ := by
  constructor
  · simp only [curvatureK]
    have hJpos : (0 : ℝ) < ↑J := by exact_mod_cast (by omega : 0 < J)
    have hJge : (1 : ℝ) ≤ ↑J - 1 := by
      have : (2 : ℝ) ≤ ↑J := by exact_mod_cast hJ
      linarith
    rw [div_lt_div_iff_of_pos_right hJpos]
    exact mul_lt_mul_of_pos_right (by linarith) (by linarith)
  · exact lower_rho_more_averse h12

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/SocialWelfare.lean:91

Module Section

CES as Atkinson Social Welfare Function

In the same file