Documentation

Lean 4 Proof

theorem curvatureK_factorization (J : ℝ) (ρ : ℝ) :
    curvatureKReal J ρ = (1 - ρ) * ((J - 1) / J) := by
  simp [curvatureKReal]; ring

Dependency Graph

Location

thesis/CESProofs/EntryExit/CurvatureInJ.lean:123

Module Section

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

In the same file