Documentation

Lean 4 Proof

theorem recovery_divergence {t_rec_0 T Tstar : ℝ}
    (hrec : 0 < t_rec_0) (hTs : 0 < Tstar) (hTlt : T < Tstar) :
    0 < adjustmentTimescale t_rec_0 T Tstar :=
  adjustmentTimescale_diverges hrec hTs hTlt

Dependency Graph

Location

thesis/CESProofs/Dynamics/FluctuationResponse.lean:193

Module Section

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

In the same file