Documentation

Lean 4 Proof

theorem utilitarian_at_rho_one (J : ℕ) (a : Fin J → ℝ) (c : Fin J → ℝ)
    (_ha_pos : ∀ j, 0 < a j) (_hc : ∀ j, 0 < c j) :
    atkinsonSWF J a 1 c = (∑ j : Fin J, a j * c j) ^ (1 : ℝ) := by
  simp only [atkinsonSWF, cesFun]
  congr 1
  · congr 1
    ext j
    rw [rpow_one]
  · norm_num

Dependency Graph

Location

thesis/CESProofs/Applications/SocialWelfare.lean:157

Module Section

CES as Atkinson Social Welfare Function

In the same file