CostStabilityEstimate

formal source

 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) *
 285          (Real.cosh (Real.sqrt hyp.curvature * |Real.log x|) - 1)
 286
 287theorem cost_stability_transfer
 288    (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T) (bounds : StabilityBounds H T)
 289    (h_stab : StabilityEstimate H T hyp.curvature bounds)
 290    (h_transfer : CostStabilityTransferHypothesis H T hyp bounds)
 291    (h : ℝ) (hh_pos : 0 < h) (hh_le : h ≤ T) :
 292    ∀ x : ℝ, Real.exp (-(T - h)) < x → x < Real.exp (T - h) →
 293    |H (Real.log x) - 1 - Cost.Jcost x| ≤
 294      (δ_error bounds.ε bounds.B bounds.K h / hyp.curvature) *
 295      (Real.cosh (Real.sqrt hyp.curvature * |Real.log x|) - 1) := by
 296  exact h_transfer h_stab h hh_pos hh_le
 297
 298/-! ## Special Case: a = 1 (Standard Calibration) -/
 299
 300/-- When a = 1 (standard RS calibration), the stability estimate simplifies. -/
 301theorem stability_calibrated
 302    (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T)
 303    (h_a1 : hyp.curvature = 1)