Documentation

Lean 4 Proof

theorem keff_slope_below (J : ℕ) (ρ T h Tstar : ℝ)
    (hTs : 0 < Tstar) (hT : T < Tstar) (hTh : T + h < Tstar)
    (hh : h ≠ 0) :
    (effectiveCurvatureKeff J ρ (T + h) Tstar -
     effectiveCurvatureKeff J ρ T Tstar) / h =
      -(curvatureK J ρ / Tstar) := by
  rw [keff_below_critical J ρ (T + h) Tstar hTs hTh,
      keff_below_critical J ρ T Tstar hTs hT]
  have hTs_ne := ne_of_gt hTs
  field_simp
  ring

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/PhaseTransition.lean:82

Module Section

Phase Transition at T* (Gap #8)

In the same file