English
Let E and F be normed spaces and f: E → F. Then f has temperate growth if and only if f is smooth of all orders and for every order n there exists a natural number k such that the nth iterated derivative of f satisfies a global bound of the form ‖iteratedFDeriv ℝ n f x‖ ≤ C (1 + ‖x‖)^k for some constant C and all x ∈ E; equivalently, iteratedFDeriv ℝ n f = O_top ((1 + ‖x‖)^k).
Русский
Пусть E и F — нормированные пространства, f: E → F. Тогда f имеет темперированный рост тогда и только тогда, когда f бесконечно дифференцируема и для каждого порядка n существует число k ∈ ℕ такое, что n-я производная по итерации удовлетворяет глобовому ограничению ‖D^n f(x)‖ ≤ C (1 + ‖x‖)^k для всех x ∈ E; эквивалентно D^n f = O_top((1 + ‖x‖)^k).
LaTeX
$$$f:\\;E\\to F$ has\\ temperate growth\\iff \\; \\text{ContDiff}_{\\mathbb{R}}^{\\infty} f\\;\\wedge\\; \\forall n\\in\\mathbb{N},\\ \\exists k\\in\\mathbb{N},\\ iteratedFDeriv_{\\mathbb{R}}^n f =O_{\\top}\\!\\big(\\lambda x:\\; (1+\\|x\\|)^k\\big).$$$
Lean4
/-- A function has temperate growth if and only if it is smooth and its `n`-th iterated
derivative is `O((1 + ‖x‖) ^ k)` for some `k : ℕ` (depending on `n`).
Note that the `O` here is with respect to the `⊤` filter, meaning that the bound holds everywhere.
TODO: when `E` is finite dimensional, this is equivalent to the derivatives being `O(‖x‖ ^ k)`
as `‖x‖ → ∞`.
-/
theorem _root_.Function.hasTemperateGrowth_iff_isBigO {f : E → F} :
f.HasTemperateGrowth ↔ ContDiff ℝ ∞ f ∧ ∀ n, ∃ k, iteratedFDeriv ℝ n f =O[⊤] (fun x ↦ (1 + ‖x‖) ^ k) :=
by
simp_rw [Asymptotics.isBigO_top]
congrm ContDiff ℝ ∞ f ∧ (∀ n, ∃ k C, ∀ x, _ ≤ C * ?_)
rw [norm_pow, Real.norm_of_nonneg (by positivity)]
