Documentation

Lean 4 Proof

def powerMeanWeight (x : Fin J → ℝ) (ρ : ℝ) (j : Fin J) : ℝ :=
  (x j) ^ ρ / ∑ k : Fin J, (x k) ^ ρ

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/TenWayIdentity.lean:130

Module Section

Ten Views of a Single Object:

In the same file