theorem
proved
tactic proof
dAlembert_second_deriv_at_zero_of_contDiff
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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
112 simpa [mul_assoc] using h_const.mul (hasDerivAt_deriv_of_contDiffTwo h_diff 0)
113 have h_deriv_eq := congrArg (fun f : ℝ → ℝ => deriv f 0) h_first
114 change deriv (fun u => deriv Hf (t + u) - deriv Hf (t - u)) 0 =
115 deriv (((fun _ : ℝ => 2 * Hf t) * deriv Hf)) 0 at h_deriv_eq
116 rw [h_left_raw.deriv, h_right.deriv] at h_deriv_eq
117 linarith
118
119/-- A `C²` d'Alembert solution with calibrated second derivative satisfies `H'' = H`. -/