pith. machine review for the scientific record. sign in
lemma proved tactic proof

isCalibrated_of_isCalibratedLimit

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)

 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

proof body

Tactic-mode proof.

 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). -/

depends on (26)

Lean names referenced from this declaration's body.