Documentation

Lean 4 Proof

theorem autocorr_monotone {tau_0 T₁ T₂ Tstar : ℝ}
    (htau : 0 < tau_0) (hTs : 0 < Tstar)
    (hT1 : T₁ < Tstar) (hT2 : T₂ < Tstar) (h12 : T₁ ≤ T₂) :
    adjustmentTimescale tau_0 T₁ Tstar ≤ adjustmentTimescale tau_0 T₂ Tstar :=
  adjustmentTimescale_monotone htau hTs hT1 hT2 h12

Dependency Graph

Location

thesis/CESProofs/Dynamics/FluctuationResponse.lean:133

Module Section

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

In the same file