Documentation

Lean 4 Proof

theorem effectiveCurvatureKeff_above_critical (J : ℕ) (ρ T Tstar : ℝ)
    (hTs : 0 < Tstar) (hT : Tstar ≤ T) :
    effectiveCurvatureKeff J ρ T Tstar = 0 := by
  simp only [effectiveCurvatureKeff]
  have h : 1 - T / Tstar ≤ 0 := by
    rw [sub_nonpos]
    rwa [le_div_iff₀ hTs, one_mul]
  rw [max_eq_left h, mul_zero]

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/Defs.lean:154

Module Section

Core definitions for the Lean formalization of Paper 2:

In the same file