StabilityFromODEHypothesis

formal source

 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)
 256    (h_ode : ODEApproximationHypothesis H T hyp bounds)
 257    (h_stab : StabilityFromODEHypothesis H T hyp bounds) :
 258    StabilityEstimate H T hyp.curvature bounds := by
 259  have h_ode' := ode_approximation_from_defect H T hyp bounds h_ode
 260  exact stability_from_ode_approx H T hyp bounds h_ode' h_stab
 261
 262/-! ## Corollary 7.1: Stability for the Cost Functional -/
 263
 264/-- **Corollary 7.1 (Cost Functional Stability)**
 265
 266Let F(x) := H(log x) - 1 on ℝ₊, where H satisfies the stability hypotheses.
 267
 268If a is close to 1 and δ(h) is small, then F is uniformly close to the
 269canonical cost J(x) = cosh(log x) - 1 on compact subintervals of (0, ∞).
 270
 271When a = 1, the estimate simplifies to:
 272  |F(x) - J(x)| ≤ δ(h) · J(|x|) -/