Documentation

Lean 4 Proof

theorem powerMean_homogDegOne {J : ℕ} (_hJ : 0 < J) {ρ : ℝ} (hρ : ρ ≠ 0)
    {x : Fin J → ℝ} (hx : ∀ j, 0 ≤ x j) {c : ℝ} (hc : 0 < c) :
    powerMean J ρ hρ (fun j => c * x j) = c * powerMean J ρ hρ x := by
  simp only [powerMean]
  have h1 : ∀ j, (c * x j) ^ ρ = c ^ ρ * (x j) ^ ρ := fun j =>
    mul_rpow (le_of_lt hc) (hx j)
  simp_rw [h1, ← Finset.mul_sum]
  rw [show (1 / ↑J : ℝ) * (c ^ ρ * ∑ j, (x j) ^ ρ) =
    c ^ ρ * ((1 / ↑J : ℝ) * ∑ j, (x j) ^ ρ) from by ring]
  rw [mul_rpow (rpow_nonneg (le_of_lt hc) ρ)
    (mul_nonneg (div_nonneg one_pos.le (Nat.cast_nonneg J))
      (Finset.sum_nonneg (fun j _ => rpow_nonneg (hx j) ρ)))]
  rw [← rpow_mul (le_of_lt hc), mul_one_div_cancel hρ, rpow_one]

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:646

Module Section

Economics extensions for CES formalization:

In the same file