Documentation

Lean 4 Proof

theorem landau_gives_keff (J : ℕ) (ρ T Tstar : ℝ) :
    curvatureK J ρ * max 0 (-(T / Tstar - 1)) =
      effectiveCurvatureKeff J ρ T Tstar := by
  simp [effectiveCurvatureKeff, neg_sub]

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/PhaseTransition.lean:236

Module Section

Phase Transition at T* (Gap #8)

In the same file