cos_second_deriv_eq

formal source

 115  nlinarith [hsq_zero]
 116
 117/-- cos satisfies the ODE cos'' = -cos. -/
 118theorem cos_second_deriv_eq : ∀ t, deriv (deriv (fun x => Real.cos x)) t = -Real.cos t := by
 119  intro t
 120  have h1 : deriv (fun x => Real.cos x) = (fun x => -Real.sin x) := by
 121    funext x
 122    simpa using (Real.deriv_cos x)
 123  rw [h1]
 124  have hneg : deriv (fun x => -Real.sin x) t = -(deriv Real.sin t) := by
 125    simpa using (deriv_neg (f := Real.sin) (x := t))
 126  rw [hneg]
 127  simp [Real.deriv_sin]
 128
 129/-- cos has the correct initial conditions: cos(0) = 1, cos'(0) = 0. -/
 130theorem cos_initials : Real.cos 0 = 1 ∧ deriv (fun x => Real.cos x) 0 = 0 := by
 131  constructor
 132  · exact Real.cos_zero
 133  · rw [Real.deriv_cos]
 134    simp [Real.sin_zero]
 135
 136/-- **Theorem (ODE Cos Uniqueness)**: The unique solution to H'' = -H with H(0) = 1, H'(0) = 0 is cos. -/
 137theorem ode_cos_uniqueness_contdiff (H : ℝ → ℝ)
 138    (h_diff : ContDiff ℝ 2 H)
 139    (h_ode : ∀ t, deriv (deriv H) t = -H t)
 140    (h_H0 : H 0 = 1)
 141    (h_H'0 : deriv H 0 = 0) :
 142    ∀ t, H t = Real.cos t := by
 143  let g := fun t => H t - Real.cos t
 144  have hg_diff : ContDiff ℝ 2 g := h_diff.sub Real.contDiff_cos
 145  have hg_ode : ∀ t, deriv (deriv g) t = -g t := by
 146    intro t
 147    have h1 : deriv g = fun s => deriv H s - deriv (fun x => Real.cos x) s := by
 148      ext s