Documentation

Lean 4 Proof

theorem susceptibility_exponent_one (sigma0_sq T Tstar : ℝ)
    (hTs : 0 < Tstar) (hT : T < Tstar) :
    varianceAtFriction sigma0_sq T Tstar =
      sigma0_sq * (1 - T / Tstar)⁻¹ := by
  rw [intensification_rate (by linarith) (by linarith)]
  rw [one_div]

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/PhaseTransition.lean:156

Module Section

Phase Transition at T* (Gap #8)

In the same file