Documentation

Lean 4 Proof

theorem minimum_viable_friction {ρ c d_sq : ℝ} (hρ : ρ < 1) :
    criticalFrictionReal 2 ρ c d_sq = 4 * c ^ 2 * d_sq / (1 - ρ) := by
  rw [criticalFrictionReal_eq 2 ρ c d_sq (by norm_num) (by linarith)]
  ring

Dependency Graph

Location

thesis/CESProofs/EntryExit/CurvatureInJ.lean:110

Module Section

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

In the same file