def
definition
CostStabilityTransferHypothesis
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.DAlembert.Stability on GitHub at line 278.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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)
304 (bounds : StabilityBounds H T)
305 (h_stab : StabilityEstimate H T hyp.curvature bounds)
306 (h : ℝ) (hh_pos : 0 < h) (hh_le : h ≤ T) :
307 ∀ t : ℝ, |t| ≤ T - h →
308 |H t - Real.cosh t| ≤ δ_error bounds.ε bounds.B bounds.K h * (Real.cosh |t| - 1) := by