Documentation

Lean 4 Proof

theorem powerMean_symmetricPoint {J : ℕ} (hJ : 0 < J) {ρ : ℝ} (hρ : ρ ≠ 0)
    {c : ℝ} (hc : 0 < c) :
    powerMean J ρ hρ (symmetricPoint J c) = c := by
  simp only [powerMean, symmetricPoint]
  have hJr : (0 : ℝ) < ↑J := Nat.cast_pos.mpr hJ
  have hJne : (J : ℝ) ≠ 0 := ne_of_gt hJr
  -- Simplify the sum: ∑ j : Fin J, c ^ ρ = ↑J * c ^ ρ
  rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin]
  -- ↑J • c^ρ = ↑J * c^ρ
  rw [nsmul_eq_mul]
  -- (1/↑J * (↑J * c^ρ))^(1/ρ) = (c^ρ)^(1/ρ)
  rw [one_div, inv_mul_cancel_left₀ hJne]
  -- (c^ρ)^(1/ρ) = c^(ρ · (1/ρ)) = c^1 = c
  rw [← rpow_mul hc.le, mul_one_div_cancel hρ, rpow_one]

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/Defs.lean:123

Module Section

Core definitions for the Lean formalization of Paper 1:

In the same file