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

stability_calibrated

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)

 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

proof body

Term-mode proof.

 309  intro t ht
 310  have h_main := h_stab h hh_pos hh_le t ht
 311  simp only [h_a1, Real.sqrt_one, one_mul, div_one] at h_main
 312  exact h_main
 313
 314/-- When a = 1, the cost stability simplifies to |F(x) - J(x)| ≤ δ · J(x). -/

depends on (15)

Lean names referenced from this declaration's body.