Documentation

Lean 4 Proof

theorem effectiveCurvatureKeff_zero_friction (J : ℕ) (ρ Tstar : ℝ)
    (_hTs : 0 < Tstar) :
    effectiveCurvatureKeff J ρ 0 Tstar = curvatureK J ρ := by
  simp only [effectiveCurvatureKeff, zero_div, sub_zero]
  rw [max_eq_right (zero_le_one), mul_one]

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/Defs.lean:145

Module Section

Core definitions for the Lean formalization of Paper 2:

In the same file