Documentation

Lean 4 Proof

theorem powerMean_zero {J : ℕ} (_hJ : 0 < J) {ρ : ℝ} (hρ : ρ ≠ 0) :
    powerMean J ρ hρ (symmetricPoint J 0) = 0 := by
  simp only [powerMean, symmetricPoint, zero_rpow hρ, Finset.sum_const_zero,
             mul_zero, zero_rpow (one_div_ne_zero hρ)]

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/Emergence.lean:68

Module Section

Emergence results from Paper 1, Sections 3-5:

In the same file