Documentation

Lean 4 Proof

theorem network_scaling_linear (hJ : 0 < J) {c : ℝ} (hc : 0 < c) :
    unnormCES J 1 (symmetricPoint J c) = ↑J * c := by
  rw [network_scaling hJ (by norm_num : (1 : ℝ) ≠ 0) hc]
  simp

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:735

Module Section

## Network Scaling Results

In the same file