isCalibrated_of_isCalibratedLimit

formal source

 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
 687  have hderiv : deriv (H F) = deriv (G F) := by
 688    funext t
 689    change deriv (fun y => G F y + 1) t = deriv (G F) t
 690    simpa using (deriv_add_const (f := G F) (x := t) (c := (1 : ℝ)))
 691  have hderiv2 : deriv (deriv (H F)) = deriv (deriv (G F)) := congrArg deriv hderiv
 692  have hderiv2_at0 : deriv (deriv (H F)) 0 = deriv (deriv (G F)) 0 :=
 693    congrArg (fun g => g 0) hderiv2
 694  simpa [IsCalibrated] using hderiv2_at0.symm.trans h_eq
 695
 696/-- **Composition Law (Equation 1.1)**:
 697F(xy) + F(x/y) = 2·F(x)·F(y) + 2·F(x) + 2·F(y) for all x, y > 0.
 698
 699This is the Recognition Composition Law (RCL). -/
 700def SatisfiesCompositionLaw (F : ℝ → ℝ) : Prop :=
 701  ∀ x y : ℝ, 0 < x → 0 < y →
 702    F (x * y) + F (x / y) = 2 * F x * F y + 2 * F x + 2 * F y
 703
 704/-- **Lemma 2.1**: If F is reciprocal, then G(t) = F(e^t) is even. -/
 705theorem reciprocal_implies_G_even (F : ℝ → ℝ) (hRecip : IsReciprocalCost F) :
 706    Function.Even (G F) :=