theorem
proved
cos_dAlembert_to_ODE
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Measurement.RecognitionAngle.AngleFunctionalEquation on GitHub at line 259.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
256 exact Real.contDiff_cos
257
258/-- cos satisfies the d'Alembert to ODE hypothesis. -/
259theorem cos_dAlembert_to_ODE : dAlembert_to_ODE_hypothesis_neg Real.cos := by
260 intro _ _ _ _
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