Documentation

Lean 4 Proof

theorem landau_minimizer_optimal (t m : ℝ) (hm : 0 ≤ m) :
    landauPotential t (max 0 (-t)) ≤ landauPotential t m := by
  unfold landauPotential
  by_cases ht : 0 ≤ t
  · -- Super-critical: minimizer is 0, V(0) = 0 ≤ V(m)
    rw [max_eq_left (by linarith : -t ≤ 0)]
    nlinarith [sq_nonneg m, mul_nonneg ht hm]
  · -- Sub-critical: V(m) - V(-t) = (m+t)²/2 ≥ 0
    push_neg at ht
    rw [max_eq_right (by linarith : 0 ≤ -t)]
    nlinarith [sq_nonneg (m + t), neg_sq t]

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/PhaseTransition.lean:221

Module Section

Phase Transition at T* (Gap #8)

In the same file