dAlembert_solution_deriv_zero

formal source

 118  linarith
 119
 120/-- D'Alembert solutions satisfy H'(0) = 0 if differentiable. -/
 121theorem dAlembert_solution_deriv_zero (H : ℝ → ℝ) (h : IsDAlembertSolution H)
 122    (hDiff : DifferentiableAt ℝ H 0) :
 123    deriv H 0 = 0 := by
 124  have hEven := dAlembert_solution_even H h
 125  exact even_deriv_at_zero H hEven hDiff
 126
 127/-! ## Classification of Solutions -/
 128
 129/-- The classification theorem for d'Alembert equation (Aczél).
 130
 131Continuous solutions to H(t+u) + H(t-u) = 2·H(t)·H(u) with H(0) = 1 are:
 1321. H(t) = 1 (constant)
 1332. H(t) = cos(αt) for some α ∈ ℂ
 1343. H(t) = cosh(αt) for some α ∈ ℝ
 135
 136With the calibration H''(0) = 1, only H = cosh survives. -/
 137theorem dAlembert_classification (H : ℝ → ℝ)
 138    (h : IsDAlembertSolution H)
 139    (hCont : Continuous H)
 140    (hCalib : deriv (deriv H) 0 = 1)
 141    -- Regularity hypotheses (from Aczél theory)
 142    (hSmooth : dAlembert_continuous_implies_smooth_hypothesis H)
 143    (hODE : dAlembert_to_ODE_hypothesis H)
 144    (hODECont : ode_regularity_continuous_hypothesis H)
 145    (hODEDiff : ode_regularity_differentiable_hypothesis H)
 146    (hBoot : ode_linear_regularity_bootstrap_hypothesis H) :
 147    ∀ t, H t = cosh t :=
 148  dAlembert_cosh_solution H h.1 hCont h.2 hCalib hSmooth hODE hODECont hODEDiff hBoot
 149
 150/-! ## The Inevitability Argument -/
 151