dAlembert_solution_even

formal source

 108  H 0 = 1 ∧ ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u
 109
 110/-- D'Alembert solutions are even. -/
 111theorem dAlembert_solution_even (H : ℝ → ℝ) (h : IsDAlembertSolution H) :
 112    Function.Even H := by
 113  have h0 := h.1
 114  have heq := h.2
 115  intro u
 116  have := heq 0 u
 117  simp only [zero_add, zero_sub, h0, two_mul] at this
 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)