Documentation

Lean 4 Proof

theorem criticalFriction_real_eq (J : ℝ) (ρ c d_sq : ℝ)
    (hJ : 1 < J) (hρ : ρ ≠ 1) :
    criticalFriction_real J ρ c d_sq = 2 * J * c ^ 2 * d_sq / (1 - ρ) := by
  simp only [criticalFriction_real, curvatureK_real]
  have hJne : J ≠ 0 := by linarith
  have h1ρ : (1 : ℝ) - ρ ≠ 0 := sub_ne_zero.mpr (Ne.symm hρ)
  have hJm1 : J - 1 ≠ 0 := by linarith
  field_simp [hJne, h1ρ, hJm1]

Dependency Graph

Location

thesis/CESProofs/EntryExit/Defs.lean:46

Module Section

Core definitions for the Lean formalization of Paper 1c:

In the same file