Documentation

Lean 4 Proof

theorem transitionWidth_decreasing {J₁ J₂ : ℕ}
    (hJ1 : 0 < J₁) (h : J₁ ≤ J₂) :
    transitionWidth J₂ ≤ transitionWidth J₁ := by
  simp only [transitionWidth]
  exact one_div_le_one_div_of_le
    (Real.sqrt_pos_of_pos (Nat.cast_pos.mpr hJ1))
    (Real.sqrt_le_sqrt (Nat.cast_le.mpr h))

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/PhaseTransition.lean:254

Module Section

Phase Transition at T* (Gap #8)

In the same file