theorem
proved
cosh_satisfies_bootstrap
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Cost.FunctionalEquation on GitHub at line 484.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
481ODE theory (Picard-Lindelöf). -/
482
483/-- cosh satisfies the ODE regularity bootstrap. -/
484theorem cosh_satisfies_bootstrap : ode_linear_regularity_bootstrap_hypothesis Real.cosh := by
485 intro _ _ _
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