`AczelSmoothnessPackage`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cost.AczelClass on GitHub at line 37.

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

  34A concrete `instance` is provided in `IndisputableMonolith.Cost.AczelProof`
  35via the unconditional `dAlembert_contDiff_top` theorem in
  36`IndisputableMonolith.Cost.AczelTheorem`. -/
  37class AczelSmoothnessPackage : Prop where
  38  smooth_of_dAlembert :
  39    ∀ (H : ℝ → ℝ),
  40      H 0 = 1 →
  41      Continuous H →
  42      (∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) →
  43      ContDiff ℝ ⊤ H
  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.