pith. machine review for the scientific record. sign in
theorem proved term proof

cost_stability_transfer

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Term-mode proof.

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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (14)

Lean names referenced from this declaration's body.