cos_dAlembert

formal source

 261  exact cos_second_deriv_eq
 262
 263/-- cos satisfies the d'Alembert equation. -/
 264theorem cos_dAlembert : ∀ t u, Real.cos (t+u) + Real.cos (t-u) = 2 * Real.cos t * Real.cos u := by
 265  intro t u
 266  rw [Real.cos_add, Real.cos_sub]
 267  ring
 268
 269/-- **Main Theorem (d'Alembert Cosine Solution)**:
 270
 271d'Alembert equation + calibration H''(0) = -1 ⟹ H = cos.
 272
 273This is the "Angle T5" theorem, parallel to the "Cost T5" theorem
 274`dAlembert_cosh_solution` in `Cost.FunctionalEquation`. -/
 275theorem dAlembert_cos_solution
 276    (H : ℝ → ℝ)
 277    (h_one : H 0 = 1)
 278    (h_cont : Continuous H)
 279    (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
 280    (h_deriv2_zero : deriv (deriv H) 0 = -1)
 281    (h_smooth_hyp : dAlembert_continuous_implies_smooth_hypothesis_neg H)
 282    (h_ode_hyp : dAlembert_to_ODE_hypothesis_neg H)
 283    (h_cont_hyp : ode_regularity_continuous_hypothesis_neg H)
 284    (h_diff_hyp : ode_regularity_differentiable_hypothesis_neg H)
 285    (h_bootstrap_hyp : ode_linear_regularity_bootstrap_hypothesis_neg H) :
 286    ∀ t, H t = Real.cos t := by
 287  -- d'Alembert + calibration → ODE H'' = -H
 288  have h_ode : ∀ t, deriv (deriv H) t = -H t := h_ode_hyp h_one h_cont h_dAlembert h_deriv2_zero
 289  -- d'Alembert → H is even
 290  have h_even : Function.Even H := Cost.FunctionalEquation.dAlembert_even H h_one h_dAlembert
 291  -- Even + differentiable → H'(0) = 0
 292  have h_deriv_zero : deriv H 0 = 0 := by
 293    have h_smooth := h_smooth_hyp h_one h_cont h_dAlembert
 294    have h_diff : DifferentiableAt ℝ H 0 := h_smooth.differentiable (by decide : (⊤ : WithTop ℕ∞) ≠ 0) |>.differentiableAt