dAlembert_second_deriv_at_zero_of_contDiff

formal source

  78  simpa [mul_assoc] using h_deriv_eq
  79
  80/-- Differentiate the first-derivative identity at `u = 0` to relate `H''(t)` to `H''(0)`. -/
  81theorem dAlembert_second_deriv_at_zero_of_contDiff
  82    (Hf : ℝ → ℝ)
  83    (h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u)
  84    (h_diff : ContDiff ℝ 2 Hf) :
  85    ∀ t, 2 * deriv (deriv Hf) t = 2 * Hf t * deriv (deriv Hf) 0 := by
  86  intro t
  87  have h_first :
  88      (fun u => deriv Hf (t + u) - deriv Hf (t - u)) =
  89        ((fun _ : ℝ => 2 * Hf t) * deriv Hf) := by
  90    funext u
  91    simpa [Pi.mul_apply, mul_assoc] using
  92      dAlembert_first_deriv_of_contDiff Hf h_dAlembert h_diff t u
  93  have h_plus :
  94      HasDerivAt (fun u => deriv Hf (t + u)) (deriv (deriv Hf) t) 0 := by
  95    have h_inner : HasDerivAt (fun u => t + u) 1 0 := by
  96      simpa using (hasDerivAt_const 0 t).add (hasDerivAt_id 0)
  97    simpa using (hasDerivAt_deriv_of_contDiffTwo h_diff (t + 0)).comp 0 h_inner
  98  have h_minus_raw :
  99      HasDerivAt (fun u => deriv Hf (t - u)) (-deriv (deriv Hf) t) 0 := by
 100    have h_inner : HasDerivAt (fun u => t - u) (-1) 0 := by
 101      simpa using (hasDerivAt_const 0 t).sub (hasDerivAt_id 0)
 102    simpa using (hasDerivAt_deriv_of_contDiffTwo h_diff (t - 0)).comp 0 h_inner
 103  have h_left_raw :
 104      HasDerivAt (fun u => deriv Hf (t + u) - deriv Hf (t - u))
 105        (deriv (deriv Hf) t + deriv (deriv Hf) t) 0 := by
 106    simpa using h_plus.sub h_minus_raw
 107  have h_const : HasDerivAt (fun _ : ℝ => 2 * Hf t) 0 0 :=
 108    hasDerivAt_const 0 (2 * Hf t)
 109  have h_right :
 110      HasDerivAt (((fun _ : ℝ => 2 * Hf t) * deriv Hf))
 111        (2 * (Hf t * deriv (deriv Hf) 0)) 0 := by