ode_cos_unit_uniqueness

formal source

 107
 108/-- **Unit-frequency cosine uniqueness**: a C² solution of `f'' = -f`
 109with `f(0)=1` and `f'(0)=0` is `cos`. -/
 110theorem ode_cos_unit_uniqueness (f : ℝ → ℝ)
 111    (h_diff : ContDiff ℝ 2 f)
 112    (h_ode : ∀ t, deriv (deriv f) t = -(f t))
 113    (h_f0 : f 0 = 1) (h_f'0 : deriv f 0 = 0) :
 114    ∀ t, f t = Real.cos t := by
 115  let g := fun t => f t - Real.cos t
 116  have hg_diff : ContDiff ℝ 2 g := h_diff.sub Real.contDiff_cos
 117  have hDf : Differentiable ℝ f :=
 118    h_diff.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
 119  have hg_ode : ∀ t, deriv (deriv g) t = -(g t) := by
 120    intro t
 121    have h1 : deriv g = fun s => deriv f s - deriv Real.cos s :=
 122      funext fun s => deriv_sub hDf.differentiableAt Real.differentiable_cos.differentiableAt
 123    have hDf1 : ContDiff ℝ 1 (deriv f) := by
 124      rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff
 125      exact (contDiff_succ_iff_deriv.mp h_diff).2.2
 126    have hDcos1 : ContDiff ℝ 1 (deriv Real.cos) := by
 127      rw [Real.deriv_cos']; exact Real.contDiff_sin.neg
 128    have h2 : deriv (deriv g) t = deriv (deriv f) t - deriv (deriv Real.cos) t := by
 129      rw [h1]
 130      exact deriv_sub
 131        (hDf1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt)
 132        (hDcos1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt)
 133    rw [h2, h_ode t]
 134    have : deriv (deriv Real.cos) t = -(Real.cos t) := by
 135      have h_dcos : deriv Real.cos = fun x => -Real.sin x := Real.deriv_cos'
 136      rw [h_dcos]
 137      exact (Real.hasDerivAt_sin t).neg.deriv
 138    rw [this]
 139    ring
 140  have hg0 : g 0 = 0 := by simp [g, h_f0, Real.cos_zero]