Documentation

Lean 4 Proof

theorem keff_continuous (J : ℕ) (ρ Tstar : ℝ) :
    Continuous (fun T => effectiveCurvatureKeff J ρ T Tstar) := by
  unfold effectiveCurvatureKeff
  exact continuous_const.mul
    (continuous_const.max (continuous_const.sub (continuous_id.div_const _)))

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/PhaseTransition.lean:69

Module Section

Phase Transition at T* (Gap #8)

In the same file