ode_cosh_uniqueness

formal source

 495  intro _ _
 496  exact Real.differentiable_cosh
 497
 498theorem ode_cosh_uniqueness (H : ℝ → ℝ)
 499    (h_ODE : ∀ t, deriv (deriv H) t = H t)
 500    (h_H0 : H 0 = 1)
 501    (h_H'0 : deriv H 0 = 0)
 502    (h_cont_hyp : ode_regularity_continuous_hypothesis H)
 503    (h_diff_hyp : ode_regularity_differentiable_hypothesis H)
 504    (h_bootstrap_hyp : ode_linear_regularity_bootstrap_hypothesis H) :
 505    ∀ t, H t = Real.cosh t := by
 506  have h_cont : Continuous H := h_cont_hyp h_ODE
 507  have h_diff : Differentiable ℝ H := h_diff_hyp h_ODE h_cont
 508  have h_C2 : ContDiff ℝ 2 H := h_bootstrap_hyp h_ODE h_cont h_diff
 509  exact ode_cosh_uniqueness_contdiff H h_C2 h_ODE h_H0 h_H'0
 510
 511/-- **Aczél's Theorem (continuous d'Alembert solutions are smooth).**
 512
 513    This is a classical result in functional equations theory:
 514    continuous solutions to f(x+y) + f(x-y) = 2f(x)f(y) with f(0) = 1
 515    are analytic and equal to cosh(λx) for some λ ∈ ℝ.
 516
 517    Reference: Aczél, "Lectures on Functional Equations" (1966), Chapter 3.
 518
 519    The full formalization would require:
 520    - Proving that measurable solutions are continuous (automatic continuity)
 521    - Using Taylor expansion around 0 to show analyticity
 522    - Applying the Cauchy functional equation theory
 523
 524    For now, this is stated as a hypothesis that follows from Aczél's theorem. -/
 525def dAlembert_continuous_implies_smooth_hypothesis (H : ℝ → ℝ) : Prop :=
 526  H 0 = 1 → Continuous H → (∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) → ContDiff ℝ ⊤ H
 527
 528/-- **d'Alembert to ODE derivation.**