Documentation

Lean 4 Proof

theorem effectiveCurvatureKeff_pos (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {T Tstar : ℝ} (_hT : 0 ≤ T) (hTs : 0 < Tstar) (hTlt : T < Tstar) :
    0 < effectiveCurvatureKeff J ρ T Tstar := by
  simp only [effectiveCurvatureKeff]
  apply mul_pos (curvatureK_pos hJ hρ)
  rw [lt_max_iff]
  right
  rw [sub_pos, div_lt_one hTs]
  exact hTlt

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/Defs.lean:188

Module Section

Core definitions for the Lean formalization of Paper 2:

In the same file