Documentation

Lean 4 Proof

theorem curvatureK_real_one (ρ : ℝ) :
    curvatureK_real 1 ρ = 0 := by
  simp [curvatureK_real]

Dependency Graph

Location

thesis/CESProofs/EntryExit/CurvatureInJ.lean:61

Module Section

Paper 1c, Section 2: K(J) as the Network Engine

In the same file