Documentation

Lean 4 Proof

theorem powerMean_le_arithMean {ρ : ℝ} (hρ₀ : 0 < ρ) (hρ₁ : ρ ≤ 1) (hρne : ρ ≠ 0)
    {x : Fin J → ℝ} (hx : ∀ j, 0 ≤ x j) (hJ : 0 < J) :
    powerMean J ρ hρne x ≤ (1 / ↑J : ℝ) * ∑ j : Fin J, x j := by
  simp only [powerMean]
  have h_avg_nn : 0 ≤ (1 / ↑J) * ∑ j : Fin J, x j := by
    apply mul_nonneg (by positivity) (Finset.sum_nonneg (fun j _ => hx j))
  have h_inner_nn : 0 ≤ (1 / ↑J) * ∑ j : Fin J, (x j) ^ ρ := by
    apply mul_nonneg (by positivity) (Finset.sum_nonneg (fun j _ => rpow_nonneg (hx j) ρ))
  have h1ρ : 0 < 1 / ρ := div_pos one_pos hρ₀
  -- Jensen: (1/J) Sum x_j^rho le ((1/J) Sum x_j)^rho
  have hjen := jensen_ces_concave hρ₀ hρ₁ hx hJ
  -- Raise to 1/rho: inner^{1/rho} le (avg^rho)^{1/rho} = avg
  have key := rpow_le_rpow h_inner_nn hjen (le_of_lt h1ρ)
  rwa [← rpow_mul h_avg_nn, mul_one_div_cancel (ne_of_gt hρ₀), rpow_one] at key

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/Economics.lean:573

Module Section

Economics extensions for CES formalization:

In the same file