English
If f has temperate growth, then for any N ∈ ℕ there exists k ∈ ℕ such that for all n ≤ N, the n-th derivative satisfies the global bound n-th derivative = O_top ((1 + ‖x‖)^k).
Русский
Если у функции f темперированный рост, то для любого N ∈ ℕ существует k ∈ ℕ, такой что для всех n ≤ N выполнено: n-я производная удовлетворяет глобальному ограничению ‖D^n f(x)‖ ≤ C (1 + ‖x‖)^k.
LaTeX
$$$\\text{If } f \\text{ has temperate growth, then } \\forall N\\in\\mathbb{N},\\ \\exists k\\in\\mathbb{N}:\\ \\forall n\\le N,\\ iteratedFDeriv_{\\mathbb{R}}^n f =O_{\\top}\\!\\big( x\\mapsto (1+\\|x\\|)^k \\big).$$$
Lean4
/-- If `f` as temperate growth, then for any `N : ℕ` one can find `k` such that *all* iterated
derivatives of `f` of order `≤ N` are `O((1 + ‖x‖) ^ k)`.
Note that the `O` here is with respect to the `⊤` filter, meaning that the bound holds everywhere.
-/
theorem _root_.Function.HasTemperateGrowth.isBigO_uniform {f : E → F} (hf_temperate : f.HasTemperateGrowth) (N : ℕ) :
∃ k, ∀ n ≤ N, iteratedFDeriv ℝ n f =O[⊤] (fun x ↦ (1 + ‖x‖) ^ k) :=
by
choose k hk using hf_temperate.isBigO
use (Finset.range (N + 1)).sup k
intro n hn
refine (hk n).trans (isBigO_of_le _ fun x ↦ ?_)
rw [Real.norm_of_nonneg (by positivity), Real.norm_of_nonneg (by positivity)]
gcongr
· simp
· exact Finset.le_sup (by simpa [← Finset.mem_range_succ_iff] using hn)
