Documentation

Lean 4 Proof

theorem autocorr_divergence {tau_0 T Tstar : ℝ}
    (htau : 0 < tau_0) (hTs : 0 < Tstar) (hTlt : T < Tstar) :
    0 < adjustmentTimescale tau_0 T Tstar :=
  adjustmentTimescale_diverges htau hTs hTlt

Dependency Graph

Location

thesis/CESProofs/Dynamics/FluctuationResponse.lean:127

Module Section

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

In the same file