Documentation

Lean 4 Proof

theorem landau_at_minimizer (t : ℝ) :
    landauPotential t (max 0 (-t)) = -(max 0 (-t)) ^ 2 / 2 := by
  unfold landauPotential
  by_cases ht : 0 ≤ t
  · rw [max_eq_left (by linarith : -t ≤ 0)]; ring
  · push_neg at ht
    rw [max_eq_right (by linarith : 0 ≤ -t)]; ring

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/PhaseTransition.lean:202

Module Section

Phase Transition at T* (Gap #8)

In the same file