ODEApproximationHypothesis
plain-language theorem explainer
The declaration posits the ODE approximation |H''(t) - a H(t)| ≤ δ(ε,B,K,h) as an explicit hypothesis on a C³ even function normalized at zero. Stability analysts working with near-solutions to the d'Alembert equation cite it to convert uniform defect bounds into pointwise differential control before invoking the full stability estimate. The definition is a one-line wrapper that directly instantiates the ODEApproximation predicate at the supplied curvature.
Claim. Let $H:ℝ→ℝ$ and $T>0$. Assume $H$ is $C^3$, even, satisfies $H(0)=1$ and $H''(0)=a>0$, and obeys uniform bounds $|Δ_H(t,u)|≤ε$, $|H(t)|≤B$, $|H'''(t)|≤K$ on $[-T,T]$. Then $|H''(t)-a H(t)|≤δ(ε,B,K,h)$ holds for all $0<h≤T$ and $|t|≤T-h$.
background
The d'Alembert equation is $H(t+u)+H(t-u)=2H(t)H(u)$, with defect $Δ_H(t,u):=H(t+u)+H(t-u)-2H(t)H(u)$. StabilityHypotheses packages the standing assumptions: $H$ is $C^3$ on $[-T,T]$, even, normalized by $H(0)=1$, and has positive curvature $a=H''(0)$. StabilityBounds supplies the numerical controls: defect bounded by $ε≥0$, range bounded by $B>0$, and third derivative bounded by $K$.
proof idea
The definition is a one-line wrapper that returns the ODEApproximation predicate instantiated at hyp.curvature. No tactics or reductions occur inside the body; the predicate itself encodes the Taylor expansion of $H(t+h)+H(t-h)$ combined with the defect identity and the supplied bounds on $H'''$.
why it matters
It supplies the missing ODE-control hypothesis inside dAlembert_stability (Theorem 7.1) and is discharged by ode_approximation_from_defect. The step completes the passage from defect estimates to the differential inequality that yields the cosh-type stability bound, supporting the transfer from the Recognition Composition Law (via CostAlgebra.H) to local hyperbolic behavior on finite intervals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.