ode_diagonalization

formal source

 288  exact hcomp.deriv
 289
 290/-- Diagonalization of the ODE f'' = f into f' ± f components. -/
 291lemma ode_diagonalization (f : ℝ → ℝ)
 292    (h_diff2 : ContDiff ℝ 2 f)
 293    (h_ode : ∀ t, deriv (deriv f) t = f t) :
 294    (∀ t, deriv (fun s => deriv f s - f s) t = -(deriv f t - f t)) ∧
 295    (∀ t, deriv (fun s => deriv f s + f s) t = deriv f t + f t) := by
 296  have h_diff1 : Differentiable ℝ f := h_diff2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
 297  have h_deriv_contdiff : ContDiff ℝ 1 (deriv f) := by
 298    rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff2
 299    rw [contDiff_succ_iff_deriv] at h_diff2
 300    exact h_diff2.2.2
 301  have h_diff_deriv : Differentiable ℝ (deriv f) := h_deriv_contdiff.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
 302  constructor
 303  · intro t
 304    have h1 : deriv (fun s => deriv f s - f s) t = deriv (deriv f) t - deriv f t := by
 305      apply deriv_sub h_diff_deriv.differentiableAt h_diff1.differentiableAt
 306    rw [h1, h_ode t]
 307    ring
 308  · intro t
 309    have h2 : deriv (fun s => deriv f s + f s) t = deriv (deriv f) t + deriv f t := by
 310      apply deriv_add h_diff_deriv.differentiableAt h_diff1.differentiableAt
 311    rw [h2, h_ode t]
 312    ring
 313
 314/-- If g' = -g and g(0) = 0, then g = 0. -/
 315lemma deriv_neg_self_zero (g : ℝ → ℝ)
 316    (h_diff : Differentiable ℝ g)
 317    (h_deriv : ∀ t, deriv g t = -g t)
 318    (h_g0 : g 0 = 0) :
 319    ∀ t, g t = 0 := by
 320  have h_const : ∀ t, deriv (fun s => g s * Real.exp s) t = 0 := by
 321    intro t