lemma
proved
tactic proof
isCalibratedLimit_of_isCalibrated
show as:
view Lean formalization →
formal statement (Lean)
656lemma isCalibratedLimit_of_isCalibrated
657 (F : ℝ → ℝ) (hNorm : IsNormalized F)
658 (_h_diff : ContDiff ℝ 2 (H F)) (h_deriv0 : deriv (H F) 0 = 0)
659 (h_log : HasLogCurvature (H F) (deriv (deriv (H F)) 0))
660 (h_calib : IsCalibrated F) :
661 IsCalibratedLimit F := by
proof body
Tactic-mode proof.
662 have hNorm' : F 1 = 0 := by simpa [IsNormalized] using hNorm
663 have h_H0 : H F 0 = 1 := by simp [H, G, hNorm']
664 have h_d2 : deriv (deriv (H F)) 0 = 1 := by
665 -- H = G + 1, so second derivatives at 0 agree
666 have hderiv : deriv (H F) = deriv (G F) := by
667 funext t
668 change deriv (fun y => G F y + 1) t = deriv (G F) t
669 simpa using (deriv_add_const (f := G F) (x := t) (c := (1 : ℝ)))
670 have hderiv2 : deriv (deriv (H F)) = deriv (deriv (G F)) := congrArg deriv hderiv
671 have hderiv2_at0 : deriv (deriv (H F)) 0 = deriv (deriv (G F)) 0 :=
672 congrArg (fun g => g 0) hderiv2
673 simpa [IsCalibrated] using hderiv2_at0.trans h_calib
674 simpa [IsCalibratedLimit, h_d2] using h_log
675