theorem
proved
tactic proof
cost_stability_calibrated
show as:
view Lean formalization →
formal statement (Lean)
315theorem cost_stability_calibrated
316 (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T)
317 (h_a1 : hyp.curvature = 1)
318 (bounds : StabilityBounds H T)
319 (h_stab : StabilityEstimate H T hyp.curvature bounds)
320 (h_transfer : CostStabilityTransferHypothesis H T hyp bounds)
321 (h : ℝ) (hh_pos : 0 < h) (hh_le : h ≤ T) :
322 ∀ x : ℝ, Real.exp (-(T - h)) < x → x < Real.exp (T - h) →
323 |H (Real.log x) - 1 - Cost.Jcost x| ≤
324 δ_error bounds.ε bounds.B bounds.K h * Cost.Jcost x := by
proof body
Tactic-mode proof.
325 intro x hx_lo hx_hi
326 have h_main := cost_stability_transfer H T hyp bounds h_stab h_transfer h hh_pos hh_le x hx_lo hx_hi
327 simp only [h_a1, Real.sqrt_one, one_mul, div_one] at h_main
328 -- Need to show cosh(|log x|) - 1 = J(x) when x > 0
329 have hx_pos : 0 < x := by linarith [Real.exp_pos (-(T-h))]
330 have hJ : Cost.Jcost x = Real.cosh (Real.log x) - 1 := by
331 have h1 := Cost.Jcost_exp_cosh (Real.log x)
332 simp only [Real.exp_log hx_pos] at h1
333 exact h1
334 have h_cosh : Real.cosh (Real.log x) - 1 = Cost.Jcost x := by
335 symm
336 exact hJ
337 simpa [h_cosh] using h_main
338
339/-! ## Zero Defect Implies Exact Solution -/
340
341/-- When the defect is exactly zero, H is an exact cosh solution. -/