Documentation

Lean 4 Proof

theorem network_scaling_normalized (hJ : 0 < J) {ρ : ℝ} (hρ : ρ ≠ 0)
    {c : ℝ} (hc : 0 < c) :
    powerMean J ρ hρ (symmetricPoint J c) = c :=
  powerMean_symmetricPoint hJ hρ hc

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:729

Module Section

## Network Scaling Results

In the same file