Documentation

Lean 4 Proof

theorem effectiveCurvatureKeff_nonneg (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    (T Tstar : ℝ) :
    0 ≤ effectiveCurvatureKeff J ρ T Tstar := by
  simp only [effectiveCurvatureKeff]
  apply mul_nonneg
  · exact le_of_lt (curvatureK_pos hJ hρ)
  · exact le_max_left 0 _

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/Defs.lean:164

Module Section

Core definitions for the Lean formalization of Paper 2:

In the same file