Documentation

Lean 4 Proof

theorem criticalFriction_linear_in_J {J ρ c d_sq : ℝ}
    (hJ : 1 < J) (hρ : ρ ≠ 1) :
    criticalFrictionReal J ρ c d_sq = 2 * J * c ^ 2 * d_sq / (1 - ρ) :=
  criticalFrictionReal_eq J ρ c d_sq hJ hρ

Dependency Graph

Location

thesis/CESProofs/EntryExit/CurvatureInJ.lean:90

Module Section

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

In the same file