theorem
proved
ode_approximation_from_defect
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.DAlembert.Stability on GitHub at line 225.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
H -
of -
H -
T -
of -
ODEApproximation -
ODEApproximationHypothesis -
StabilityBounds -
StabilityHypotheses -
of -
of -
T -
of -
and
used by
formal source
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.
232
233If |H''(t) - a·H(t)| ≤ δ and H(0) = cosh(0) = 1, H'(0) = sinh(0) = 0,
234then the variation-of-parameters formula gives:
235
236 H(t) - cosh(√a·t) = ∫₀ᵗ (1/√a)·sinh(√a·(t-s))·r(s) ds
237
238where r(s) = H''(s) - a·H(s) satisfies |r(s)| ≤ δ.
239
240Bounding the integral gives:
241 |H(t) - cosh(√a·t)| ≤ (δ/a)·(cosh(√a·|t|) - 1) -/
242def StabilityFromODEHypothesis
243 (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T) (bounds : StabilityBounds H T) : Prop :=
244 ODEApproximation H T hyp.curvature bounds → StabilityEstimate H T hyp.curvature bounds
245
246theorem stability_from_ode_approx
247 (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T) (bounds : StabilityBounds H T)
248 (h_ode : ODEApproximation H T hyp.curvature bounds)
249 (h_stab : StabilityFromODEHypothesis H T hyp bounds) :
250 StabilityEstimate H T hyp.curvature bounds := by
251 exact h_stab h_ode
252
253/-- **Theorem 7.1 (Complete Statement)** -/
254theorem dAlembert_stability
255 (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T) (bounds : StabilityBounds H T)