theorem
proved
term proof
ode_cosh_uniqueness
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Term-mode proof.
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. -/