Documentation

Lean 4 Proof

theorem slope_jump_pos (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {Tstar : ℝ} (hTs : 0 < Tstar) :
    0 < curvatureK J ρ / Tstar :=
  div_pos (curvatureK_pos hJ hρ) hTs

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/PhaseTransition.lean:122

Module Section

Phase Transition at T* (Gap #8)

In the same file