contDiffTwo_differentiable_deriv

formal source

  28    (h_diff : ContDiff ℝ 2 Hf) : Differentiable ℝ Hf := by
  29  exact h_diff.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
  30
  31private lemma contDiffTwo_differentiable_deriv {Hf : ℝ → ℝ}
  32    (h_diff : ContDiff ℝ 2 Hf) : Differentiable ℝ (deriv Hf) := by
  33  have h_diff' := h_diff
  34  rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff'
  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 :