isCalibratedLimit_of_isCalibrated

formal source

 653    _ = H 0 + deriv H 0 * x + (deriv (deriv H) 0) / 2 * x^2 := by
 654          simp [Nat.factorial_one, mul_comm, mul_left_comm, mul_assoc, div_eq_mul_inv]
 655
 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
 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
 676lemma isCalibrated_of_isCalibratedLimit
 677  (F : ℝ → ℝ) (hNorm : IsNormalized F)
 678  (h_diff : ContDiff ℝ 2 (H F)) (h_deriv0 : deriv (H F) 0 = 0)
 679  (h_log : HasLogCurvature (H F) (deriv (deriv (H F)) 0))
 680  (h_limit : IsCalibratedLimit F) :
 681  IsCalibrated F := by
 682  have hNorm' : F 1 = 0 := by simpa [IsNormalized] using hNorm
 683  have h_H0 : H F 0 = 1 := by simp [H, G, hNorm']
 684  have h_eq : deriv (deriv (H F)) 0 = 1 :=
 685    tendsto_nhds_unique h_log h_limit
 686  -- transfer from H back to G