dAlembert_stability

formal source

 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|) -/
 273def CostStabilityEstimate (F : ℝ → ℝ) (T a : ℝ) (δ : ℝ) : Prop :=
 274  ∀ x : ℝ, Real.exp (-(T)) < x → x < Real.exp T →
 275  |F x - Cost.Jcost x| ≤ (δ / a) * (Real.cosh (Real.sqrt a * |Real.log x|) - 1)
 276
 277/-- Transfer stability from H to F via F(x) = H(log x) - 1. -/
 278def CostStabilityTransferHypothesis
 279    (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T) (bounds : StabilityBounds H T) : Prop :=
 280  StabilityEstimate H T hyp.curvature bounds →
 281    ∀ (h : ℝ) (hh_pos : 0 < h) (hh_le : h ≤ T),
 282      ∀ x : ℝ, Real.exp (-(T - h)) < x → x < Real.exp (T - h) →
 283        |H (Real.log x) - 1 - Cost.Jcost x| ≤
 284          (δ_error bounds.ε bounds.B bounds.K h / hyp.curvature) *