Documentation

Lean 4 Proof

theorem atkinsonIndex_nonneg_equal_weights (J : ℕ) (hJ : 0 < J)
    {ρ : ℝ} (hρ_pos : 0 < ρ) (hρ_lt : ρ < 1)
    (c : Fin J → ℝ) (hc : ∀ j, 0 < c j) :
    -- Power mean of order ρ ≤ arithmetic mean (power mean inequality)
    powerMean J ρ (ne_of_gt hρ_pos) c ≤ (1 / ↑J) * ∑ j : Fin J, c j := by
  exact powerMean_le_arithMean hρ_pos hρ_lt.le (ne_of_gt hρ_pos) (fun j => (hc j).le) hJ

Dependency Graph

Location

thesis/CESProofs/Applications/SocialWelfare.lean:142

Module Section

CES as Atkinson Social Welfare Function

In the same file