Documentation

Lean 4 Proof

theorem keff_slope_above (J : ℕ) (ρ T h Tstar : ℝ)
    (hTs : 0 < Tstar) (hT : Tstar ≤ T) (hTh : Tstar ≤ T + h) :
    effectiveCurvatureKeff J ρ (T + h) Tstar -
     effectiveCurvatureKeff J ρ T Tstar = 0 := by
  rw [effectiveCurvatureKeff_above_critical J ρ (T + h) Tstar hTs hTh,
      effectiveCurvatureKeff_above_critical J ρ T Tstar hTs hT]
  ring

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/PhaseTransition.lean:95

Module Section

Phase Transition at T* (Gap #8)

In the same file