Documentation

Lean 4 Proof

theorem powerMean_eq_scaled_lpNorm {ρ : ℝ} (hρ : ρ ≠ 0) {x : Fin J → ℝ}
    (hx : ∀ j, 0 ≤ x j) :
    powerMean J ρ hρ x = (1 / ↑J : ℝ) ^ (1 / ρ) * lpNorm J ρ x := by
  simp only [powerMean, lpNorm]
  have habsrw : ∀ j, |x j| ^ ρ = (x j) ^ ρ := fun j => by rw [abs_of_nonneg (hx j)]
  simp_rw [habsrw]
  rw [mul_rpow (by positivity : (0 : ℝ) ≤ 1 / ↑J)
               (Finset.sum_nonneg (fun j _ => rpow_nonneg (hx j) ρ))]

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:416

Module Section

Economics extensions for CES formalization:

In the same file