theorem
proved
tactic proof
dAlembert_first_deriv_of_contDiff
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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
75 change deriv (fun v => Hf (t + v) + Hf (t - v)) u =
76 deriv (((fun _ : ℝ => 2 * Hf t) * Hf)) u at h_deriv_eq
77 rw [h_left.deriv, h_right.deriv] at h_deriv_eq
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)`. -/