ode_cos_uniqueness_contdiff

formal source

 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
 161      · exact hH_diff1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt
 162      · exact hcos_diff1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt
 163    rw [h2, h_ode t, cos_second_deriv_eq t]
 164    ring
 165  have hg0 : g 0 = 0 := by
 166    simp [g, h_H0, Real.cos_zero]
 167  have hg'0 : deriv g 0 = 0 := by