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

hasDerivAt_sinhDivAlpha

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)

 107private lemma hasDerivAt_sinhDivAlpha (α : ℝ) (hα : α ≠ 0) (t : ℝ) :
 108    HasDerivAt (fun s => sinh (α * s) / α) (cosh (α * t)) t := by

proof body

Term-mode proof.

 109  have h1 : HasDerivAt (fun s => sinh (α * s)) (cosh (α * t) * α) t :=
 110    (hasDerivAt_sinh (α * t)).comp t (hasDerivAt_alpha_mul α t)
 111  convert h1.div_const α using 1
 112  field_simp
 113
 114/-- **Calibration Invariance**: G_α''(0) = 1 for every α ≠ 0.
 115    The unit-curvature condition is independent of the rescaling parameter. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (19)

Lean names referenced from this declaration's body.