HasTemperateGrowth — Mathlib

English

A function has temperate growth if it is smooth and all iterated derivatives are polynomially bounded.

Русский

Функция имеет temperate growth, если она гладкая и все её итеративные производные имеют полиномиальные ограничения.

LaTeX

$$$\mathrm{Function.HasTemperateGrowth}(f) = (\mathrm{ContDiff}(\mathbb{R},\infty, f) \wedge \forall n, \exists k,C, \forall x, \|\iteratedFDeriv\,^n f(x)\| \le C (1+\|x\|)^k)$$$

Lean4

/-- A function is called of temperate growth if it is smooth and all iterated derivatives are
polynomially bounded. -/
def _root_.Function.HasTemperateGrowth (f : E → F) : Prop :=
  ContDiff ℝ ∞ f ∧ ∀ n : ℕ, ∃ (k : ℕ) (C : ℝ), ∀ x, ‖iteratedFDeriv ℝ n f x‖ ≤ C * (1 + ‖x‖) ^ k

Похожие утверждения