ode_zero_uniqueness_neg

formal source

  99
 100/-- **Theorem (ODE Zero Uniqueness for f'' = -f)**:
 101The unique solution to f'' = -f with f(0) = 0 and f'(0) = 0 is f = 0. -/
 102theorem ode_zero_uniqueness_neg (f : ℝ → ℝ)
 103    (h_diff2 : ContDiff ℝ 2 f)
 104    (h_ode : ∀ t, deriv (deriv f) t = -f t)
 105    (h_f0 : f 0 = 0)
 106    (h_f'0 : deriv f 0 = 0) :
 107    ∀ t, f t = 0 := by
 108  intro t
 109  have hE := ode_neg_energy_constant f h_diff2 h_ode t
 110  have hzero : f t ^ 2 + (deriv f t) ^ 2 = 0 := by
 111    simpa [h_f0, h_f'0] using hE
 112  have hsq_nonneg : 0 ≤ f t ^ 2 := sq_nonneg (f t)
 113  have hderivsq_nonneg : 0 ≤ (deriv f t) ^ 2 := sq_nonneg (deriv f t)
 114  have hsq_zero : f t ^ 2 = 0 := by linarith
 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