ode_cosh_uniqueness_contdiff

formal source

 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
 431        rw [contDiff_succ_iff_deriv] at h_diff
 432        exact h_diff.2.2
 433      have hcosh_diff1 : ContDiff ℝ 1 (deriv Real.cosh) := by
 434        rw [Real.deriv_cosh]; exact Real.contDiff_sinh
 435      rw [h1]; apply deriv_sub
 436      · exact hH_diff1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt
 437      · exact hcosh_diff1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt
 438    rw [h2, h_ode t, cosh_second_deriv_eq t]
 439  have hg0 : g 0 = 0 := by simp [g, h_H0, Real.cosh_zero]
 440  have hg'0 : deriv g 0 = 0 := by
 441    have h1 : deriv g 0 = deriv H 0 - deriv Real.cosh 0 := by
 442      apply deriv_sub
 443      · exact (h_diff.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)).differentiableAt
 444      · exact Real.differentiable_cosh.differentiableAt