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

hasDerivAt_costAlphaLog_third

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)

  99private lemma hasDerivAt_costAlphaLog_third (α : ℝ) (hα : α ≠ 0) (t : ℝ) :
 100    HasDerivAt (deriv (deriv (CostAlphaLog α))) (α * sinh (α * t)) t := by

proof body

Tactic-mode proof.

 101  rw [deriv_deriv_costAlphaLog_eq α hα]
 102  have h_inner : HasDerivAt (fun x : ℝ => α * x) α t := by
 103    have h : HasDerivAt (fun x => x * α) α t := by
 104      simpa using (hasDerivAt_id t).mul_const α
 105    rwa [show (fun x : ℝ => x * α) = (fun x => α * x) from
 106      funext fun x => mul_comm x α] at h
 107  have h1 : HasDerivAt (fun s => cosh (α * s)) (sinh (α * t) * α) t :=
 108    (hasDerivAt_cosh (α * t)).comp t h_inner
 109  convert h1 using 1
 110  ring
 111

used by (1)

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

depends on (7)

Lean names referenced from this declaration's body.