Documentation

Lean 4 Proof

theorem keff_at_critical (J : ℕ) (ρ Tstar : ℝ) (hTs : 0 < Tstar) :
    effectiveCurvatureKeff J ρ Tstar Tstar = 0 :=
  effectiveCurvatureKeff_above_critical J ρ Tstar Tstar hTs (le_refl _)

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/PhaseTransition.lean:46

Module Section

Phase Transition at T* (Gap #8)

In the same file