Documentation

Lean 4 Proof

theorem variance_monotone {sigma0_sq T₁ T₂ Tstar : ℝ}
    (hsigma : 0 < sigma0_sq) (hTs : 0 < Tstar)
    (_hT1 : T₁ < Tstar) (_hT2 : T₂ < Tstar) (h12 : T₁ ≤ T₂) :
    varianceAtFriction sigma0_sq T₁ Tstar ≤
    varianceAtFriction sigma0_sq T₂ Tstar := by
  simp only [varianceAtFriction]
  apply div_le_div_of_nonneg_left (le_of_lt hsigma)
  · rw [sub_pos, div_lt_one hTs]; linarith
  · apply sub_le_sub_left
    exact div_le_div_of_nonneg_right h12 (le_of_lt hTs)

Dependency Graph

Location

thesis/CESProofs/Dynamics/FluctuationResponse.lean:166

Module Section

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

In the same file