hasDerivAt_deriv_of_contDiffTwo

formal source

  35  rw [contDiff_succ_iff_deriv] at h_diff'
  36  exact h_diff'.2.2.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
  37
  38private lemma hasDerivAt_deriv_of_contDiffTwo {Hf : ℝ → ℝ}
  39    (h_diff : ContDiff ℝ 2 Hf) (x : ℝ) :
  40    HasDerivAt (deriv Hf) (deriv (deriv Hf) x) x := by
  41  exact (contDiffTwo_differentiable_deriv h_diff).differentiableAt.hasDerivAt
  42
  43/-- Differentiate the d'Alembert equation once in the second variable. -/
  44theorem dAlembert_first_deriv_of_contDiff
  45    (Hf : ℝ → ℝ)
  46    (h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u)
  47    (h_diff : ContDiff ℝ 2 Hf) :
  48    ∀ t u, deriv Hf (t + u) - deriv Hf (t - u) = 2 * Hf t * deriv Hf u := by
  49  intro t u
  50  have h_diff1 : Differentiable ℝ Hf := contDiffTwo_differentiable h_diff
  51  have h_plus :
  52      HasDerivAt (fun v => Hf (t + v)) (deriv Hf (t + u)) u := by
  53    have h_inner : HasDerivAt (fun v => t + v) 1 u := by
  54      simpa using (hasDerivAt_const u t).add (hasDerivAt_id u)
  55    simpa using (h_diff1.differentiableAt (x := t + u)).hasDerivAt.comp u h_inner
  56  have h_minus :
  57      HasDerivAt (fun v => Hf (t - v)) (-deriv Hf (t - u)) u := by
  58    have h_inner : HasDerivAt (fun v => t - v) (-1) u := by
  59      simpa using (hasDerivAt_const u t).sub (hasDerivAt_id u)
  60    simpa using (h_diff1.differentiableAt (x := t - u)).hasDerivAt.comp u h_inner
  61  have h_left :
  62      HasDerivAt (fun v => Hf (t + v) + Hf (t - v))
  63        (deriv Hf (t + u) - deriv Hf (t - u)) u := by
  64    simpa using h_plus.add h_minus
  65  have h_const : HasDerivAt (fun _ : ℝ => 2 * Hf t) 0 u :=
  66    hasDerivAt_const u (2 * Hf t)
  67  have h_right :
  68      HasDerivAt (((fun _ : ℝ => 2 * Hf t) * Hf)) (2 * (Hf t * deriv Hf u)) u := by