stability_from_ode_approx

formal source

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