ODEApproximation

formal source

 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
 222    (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T) (bounds : StabilityBounds H T) : Prop :=
 223  ODEApproximation H T hyp.curvature bounds
 224
 225theorem ode_approximation_from_defect
 226    (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T) (bounds : StabilityBounds H T)
 227    (h_ode : ODEApproximationHypothesis H T hyp bounds) :
 228    ODEApproximation H T hyp.curvature bounds := by
 229  exact h_ode
 230
 231/-- **Key Lemma**: ODE approximation + Gronwall implies stability estimate.