theorem
proved
cosh_satisfies_continuous
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cost.FunctionalEquation on GitHub at line 489.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
486 exact Real.contDiff_cosh
487
488/-- cosh is continuous. -/
489theorem cosh_satisfies_continuous : ode_regularity_continuous_hypothesis Real.cosh := by
490 intro _
491 exact Real.continuous_cosh
492
493/-- cosh is differentiable. -/
494theorem cosh_satisfies_differentiable : ode_regularity_differentiable_hypothesis Real.cosh := by
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: