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

deriv2_Jlog

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)

  34lemma deriv2_Jlog (t : ℝ) : deriv (deriv Jlog) t = cosh t := by

proof body

Tactic-mode proof.

  35  have h1 : deriv Jlog = sinh := by
  36    funext s; exact deriv_Jlog s
  37  rw [h1]
  38  exact (hasDerivAt_sinh t).deriv
  39
  40/-- The calibration theorem: second derivative at zero equals 1 -/

used by (1)

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

depends on (5)

Lean names referenced from this declaration's body.