Documentation

Lean 4 Proof

theorem network_scaling (hJ : 0 < J) {ρ : ℝ} (hρ : ρ ≠ 0)
    {c : ℝ} (hc : 0 < c) :
    unnormCES J ρ (symmetricPoint J c) = (↑J : ℝ) ^ (1 / ρ) * c :=
  unnormCES_symmetricPoint (show 0 < J from hJ) hρ hc

Dependency Graph

Used by

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:722

Module Section

## Network Scaling Results

In the same file