deriv_exp_neg

formal source

 277/-! ## ODE Uniqueness Infrastructure -/
 278
 279/-- Helper: derivative of exp(-s) is -exp(-s). -/
 280lemma deriv_exp_neg (t : ℝ) : deriv (fun s => Real.exp (-s)) t = -Real.exp (-t) := by
 281  have h := Real.hasDerivAt_exp (-t)
 282  have hc : HasDerivAt (fun s => -s) (-1) t := by
 283    have := hasDerivAt_neg (x := t)
 284    simp at this ⊢
 285    exact this
 286  have hcomp := h.comp t hc
 287  simp at hcomp
 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