Documentation

Lean 4 Proof

theorem intensification_rate {sigma0_sq T Tstar : ℝ}
    (_hTs : 0 < Tstar) (_hTlt : T < Tstar) :
    varianceAtFriction sigma0_sq T Tstar =
    sigma0_sq * (1 / (1 - T / Tstar)) := by
  simp only [varianceAtFriction, div_eq_mul_inv, one_mul]

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/FluctuationResponse.lean:241

Module Section

Results 8-16: Variance-Response Identity and Early Warning

In the same file