191def StabilityEstimate (H : ℝ → ℝ) (T a : ℝ) (bounds : StabilityBounds H T) : Prop :=
proof body
Definition body.
192 ∀ h : ℝ, 0 < h → h ≤ T → 193 ∀ t : ℝ, |t| ≤ T - h → 194 |H t - Real.cosh (Real.sqrt a * t)| ≤ 195 (δ_error bounds.ε bounds.B bounds.K h / a) * (Real.cosh (Real.sqrt a * |t|) - 1) 196 197/-- The ODE intermediate step: from the defect bound, we derive H'' - a·H is small. 198 199This is equation (7.3) in the paper: 200 |H''(t) - a·H(t)| ≤ δ(h) for |t| ≤ T - h -/
used by (7)
From the project-wide theorem graph. These declarations reference this one in their body.