pith. machine review for the scientific record. sign in
def definition def or abbrev

ODEApproximation

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 201def ODEApproximation (H : ℝ → ℝ) (T a : ℝ) (bounds : StabilityBounds H T) : Prop :=

proof body

Definition body.

 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. -/

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (16)

Lean names referenced from this declaration's body.