cosh_second_deriv_eq

formal source

 397  simp only [g, hf] at hgt hht
 398  linarith
 399
 400theorem cosh_second_deriv_eq : ∀ t, deriv (deriv (fun x => Real.cosh x)) t = Real.cosh t := by
 401  intro t
 402  have h1 : deriv (fun x => Real.cosh x) = Real.sinh := Real.deriv_cosh
 403  rw [h1]
 404  have h2 : deriv Real.sinh = Real.cosh := Real.deriv_sinh
 405  exact congrFun h2 t
 406
 407theorem cosh_initials : Real.cosh 0 = 1 ∧ deriv (fun x => Real.cosh x) 0 = 0 := by
 408  constructor
 409  · simp [Real.cosh_zero]
 410  · have h := Real.deriv_cosh
 411    simp only [h, Real.sinh_zero]
 412
 413/-- **Theorem (ODE Cosh Uniqueness)**: The unique solution to H'' = H with H(0) = 1, H'(0) = 0 is cosh. -/
 414theorem ode_cosh_uniqueness_contdiff (H : ℝ → ℝ)
 415    (h_diff : ContDiff ℝ 2 H)
 416    (h_ode : ∀ t, deriv (deriv H) t = H t)
 417    (h_H0 : H 0 = 1)
 418    (h_H'0 : deriv H 0 = 0) :
 419    ∀ t, H t = Real.cosh t := by
 420  let g := fun t => H t - Real.cosh t
 421  have hg_diff : ContDiff ℝ 2 g := h_diff.sub Real.contDiff_cosh
 422  have hg_ode : ∀ t, deriv (deriv g) t = g t := by
 423    intro t
 424    have h1 : deriv g = fun s => deriv H s - deriv Real.cosh s := by
 425      ext s; apply deriv_sub
 426      · exact (h_diff.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)).differentiableAt
 427      · exact Real.differentiable_cosh.differentiableAt
 428    have h2 : deriv (deriv g) t = deriv (deriv H) t - deriv (deriv Real.cosh) t := by
 429      have hH_diff1 : ContDiff ℝ 1 (deriv H) := by
 430        rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff