cos_initials

formal source

 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
 149      apply deriv_sub
 150      · exact (h_diff.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)).differentiableAt
 151      · exact Real.differentiable_cos.differentiableAt
 152    have h2 : deriv (deriv g) t = deriv (deriv H) t - deriv (deriv (fun x => Real.cos x)) t := by
 153      have hH_diff1 : ContDiff ℝ 1 (deriv H) := by
 154        rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff
 155        rw [contDiff_succ_iff_deriv] at h_diff
 156        exact h_diff.2.2
 157      have hcos_diff1 : ContDiff ℝ 1 (deriv (fun x => Real.cos x)) := by
 158        simpa [Real.deriv_cos] using (Real.contDiff_sin.neg)
 159      rw [h1]
 160      apply deriv_sub