`aczel_dAlembert_smooth`

proved

show as: view math explainer →

module: IndisputableMonolith.Cost.AczelClass
domain: Cost
line: 47 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cost.AczelClass on GitHub at line 47.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  44
  45/-- Smoothness of continuous d'Alembert solutions, parameterized by an
  46`AczelSmoothnessPackage` instance. -/
  47theorem aczel_dAlembert_smooth [AczelSmoothnessPackage] (H : ℝ → ℝ)
  48    (h_one : H 0 = 1)
  49    (h_cont : Continuous H)
  50    (h_dAlembert : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
  51    ContDiff ℝ ⊤ H :=
  52  AczelSmoothnessPackage.smooth_of_dAlembert H h_one h_cont h_dAlembert
  53
  54end FunctionalEquation
  55end Cost
  56end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.