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

J_log_second_deriv_at_zero

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)

 103theorem J_log_second_deriv_at_zero : deriv (deriv J_log) 0 = 1 := by

proof body

Tactic-mode proof.

 104  -- J_log(t) = cosh(t) - 1
 105  -- J_log'(t) = sinh(t)
 106  -- J_log''(t) = cosh(t)
 107  -- J_log''(0) = cosh(0) = 1
 108  have h1 : deriv J_log = Real.sinh := by
 109    ext t
 110    unfold J_log
 111    rw [deriv_sub_const, Real.deriv_cosh]
 112  rw [h1, Real.deriv_sinh]
 113  exact Real.cosh_zero
 114
 115/-- **HYPOTHESIS**: Quadratic approximation of cosh(x) has a tight fourth-order bound.
 116    For |x| < 1, the Taylor remainder satisfies |cosh x - 1 - x²/2| ≤ x⁴/20.
 117    Proof follows from bounding the series Σ x^(2n)/(2n)! by its first term and a geometric tail. -/

used by (1)

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

depends on (11)

Lean names referenced from this declaration's body.