Documentation

Lean 4 Proof

theorem atkinson_index_zero_at_equality (J : ℕ) (_hJ : 0 < J) (a : Fin J → ℝ)
    (_ha_pos : ∀ j, 0 < a j) (ha_sum : ∑ j : Fin J, a j = 1)
    {ρ : ℝ} (hρ : ρ ≠ 0) {c : ℝ} (hc : 0 < c) :
    atkinsonIndex J a (fun _ => c) ρ = 0 := by
  simp only [atkinsonIndex, atkinsonSWF, cesFun]
  -- Sum: Σ aⱼ · c^ρ = c^ρ · Σ aⱼ = c^ρ
  have hsum : ∑ j : Fin J, a j * c ^ ρ = c ^ ρ := by
    rw [← Finset.sum_mul]; simp [ha_sum]
  rw [hsum]
  -- (c^ρ)^{1/ρ} = c
  rw [← rpow_mul hc.le, mul_one_div_cancel hρ, rpow_one]
  -- Σ aⱼ · c = c
  have hmu : ∑ j : Fin J, a j * c = c := by
    rw [← Finset.sum_mul]; simp [ha_sum]
  rw [hmu, div_self (ne_of_gt hc), sub_self]

Dependency Graph

Location

thesis/CESProofs/Applications/SocialWelfare.lean:114

Module Section

CES as Atkinson Social Welfare Function

In the same file