StabilityEstimate

formal source

 188  |H(t) - cosh(√a·t)| ≤ (δ(h)/a) · (cosh(√a·|t|) - 1)
 189
 190When a = 1 and δ(h) is small, this shows H ≈ cosh on compact intervals. -/
 191def StabilityEstimate (H : ℝ → ℝ) (T a : ℝ) (bounds : StabilityBounds H T) : Prop :=
 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 -/
 201def ODEApproximation (H : ℝ → ℝ) (T a : ℝ) (bounds : StabilityBounds H T) : Prop :=
 202  ∀ h : ℝ, 0 < h → h ≤ T →
 203  ∀ t : ℝ, |t| ≤ T - h →
 204  |deriv (deriv H) t - a * H t| ≤ δ_error bounds.ε bounds.B bounds.K h
 205
 206/-- **Key Lemma**: Taylor expansion + defect bound implies ODE approximation.
 207
 208From the integral form of Taylor's theorem:
 209  H(t+h) + H(t-h) = 2H(t) + h²H''(t) + O(h³)
 210
 211Combined with the defect identity:
 212  H(t+h) + H(t-h) = 2H(t)H(h) + Δ(t,h)
 213
 214We get:
 215  h²H''(t) ≈ 2H(t)(H(h) - 1) + Δ(t,h)
 216
 217For small h, H(h) ≈ 1 + (a/2)h², so:
 218  h²H''(t) ≈ a·h²·H(t) + Δ(t,h) + O(h³)
 219
 220Dividing by h² gives the ODE approximation. -/
 221def ODEApproximationHypothesis