dAlembert_first_deriv_of_contDiff

formal source

  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
  69    simpa [mul_assoc] using h_const.mul ((h_diff1.differentiableAt (x := u)).hasDerivAt)
  70  have h_eq :
  71      (fun v => Hf (t + v) + Hf (t - v)) = ((fun _ : ℝ => 2 * Hf t) * Hf) := by
  72    funext v
  73    simpa [Pi.mul_apply, mul_assoc] using h_dAlembert t v
  74  have h_deriv_eq := congrArg (fun f : ℝ → ℝ => deriv f u) h_eq