Documentation

Lean 4 Proof

def criticalFrictionReal (J : ℝ) (ρ c d_sq : ℝ) : ℝ :=
  2 * (J - 1) * c ^ 2 * d_sq / curvatureKReal J ρ

Dependency Graph

Used by

Location

thesis/CESProofs/EntryExit/Defs.lean:41

Module Section

Core definitions for the Lean formalization of Paper 1c:

In the same file