Lean 4 Proof

theorem variance_divergence {sigma0_sq T Tstar : ℝ}
    (hsigma : 0 < sigma0_sq) (hTs : 0 < Tstar) (hTlt : T < Tstar) :
    0 < varianceAtFriction sigma0_sq T Tstar := by
  simp only [varianceAtFriction]
  apply div_pos hsigma
  rw [sub_pos, div_lt_one hTs]
  exact hTlt

Dependency Graph

Location

thesis/CESProofs/Dynamics/FluctuationResponse.lean:157

Module Section

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

In the same file