dAlembert_to_ODE_hypothesis

formal source

 532    Proof sketch: Differentiate H(t+u) + H(t-u) = 2H(t)H(u) twice with respect to u,
 533    then set u = 0 to get H''(t) = H''(0) · H(t). With calibration H''(0) = 1, this
 534    gives H''(t) = H(t). -/
 535def dAlembert_to_ODE_hypothesis (H : ℝ → ℝ) : Prop :=
 536  H 0 = 1 → Continuous H → (∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) →
 537    deriv (deriv H) 0 = 1 → ∀ t, deriv (deriv H) t = H t
 538
 539/-- cosh satisfies the d'Alembert smoothness hypothesis. -/
 540theorem cosh_dAlembert_smooth : dAlembert_continuous_implies_smooth_hypothesis Real.cosh := by
 541  intro _ _ _
 542  exact Real.contDiff_cosh
 543
 544/-- cosh satisfies the d'Alembert to ODE hypothesis. -/
 545theorem cosh_dAlembert_to_ODE : dAlembert_to_ODE_hypothesis Real.cosh := by
 546  intro _ _ _ _
 547  exact cosh_second_deriv_eq
 548
 549theorem dAlembert_cosh_solution
 550    (H : ℝ → ℝ)
 551    (h_one : H 0 = 1)
 552    (h_cont : Continuous H)
 553    (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
 554    (h_deriv2_zero : deriv (deriv H) 0 = 1)
 555    (h_smooth_hyp : dAlembert_continuous_implies_smooth_hypothesis H)
 556    (h_ode_hyp : dAlembert_to_ODE_hypothesis H)
 557    (h_cont_hyp : ode_regularity_continuous_hypothesis H)
 558    (h_diff_hyp : ode_regularity_differentiable_hypothesis H)
 559    (h_bootstrap_hyp : ode_linear_regularity_bootstrap_hypothesis H) :
 560    ∀ t, H t = Real.cosh t := by
 561  have h_ode : ∀ t, deriv (deriv H) t = H t := h_ode_hyp h_one h_cont h_dAlembert h_deriv2_zero
 562  have h_even : Function.Even H := dAlembert_even H h_one h_dAlembert
 563  have h_deriv_zero : deriv H 0 = 0 := by
 564    have h_smooth := h_smooth_hyp h_one h_cont h_dAlembert
 565    have h_diff : DifferentiableAt ℝ H 0 := h_smooth.differentiable (by decide : (⊤ : WithTop ℕ∞) ≠ 0) |>.differentiableAt