Lean 4 Proof

theorem correlationLength_divergence (D τ₀ T Tstar : ℝ) :
    correlationLengthSq D τ₀ T Tstar =
      D * τ₀ * (1 - T / Tstar)⁻¹ := by
  simp [correlationLengthSq, adjustmentTimescale, div_eq_mul_inv, mul_assoc]

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/PhaseTransition.lean:178

Module Section

Phase Transition at T* (Gap #8)

In the same file