English
For f with temperate growth, there exists k such that for every n, the norm of the nth iterated derivative is bounded by C (1 + ‖x‖)^k uniformly in x.
Русский
Для функции f с темперированным ростом существует k such that для каждого n нормa n-й итеративной производной ограничена: ‖D^n f(x)‖ ≤ C (1+‖x‖)^k независимо от x.
LaTeX
$$$\\exists k\\in\\mathbb{N},\\ \\exists C\\ge 0:\\ \\forall N\\le n,\\ \\forall x:\\ ‖iteratedFDeriv\\mathbb{R}^N f\\,x‖ \\le C\\,(1+‖x‖)^k.$$$
Lean4
theorem _root_.Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform_aux {f : E → F}
(hf_temperate : f.HasTemperateGrowth) (n : ℕ) :
∃ (k : ℕ) (C : ℝ), 0 ≤ C ∧ ∀ N ≤ n, ∀ x : E, ‖iteratedFDeriv ℝ N f x‖ ≤ C * (1 + ‖x‖) ^ k :=
by
rcases hf_temperate.isBigO_uniform n with ⟨k, hk⟩
set F := fun x (N : Fin (n + 1)) ↦ iteratedFDeriv ℝ N f x
have : F =O[⊤] (fun x ↦ (1 + ‖x‖) ^ k) :=
by
simp_rw [F, isBigO_pi, Fin.forall_iff, Nat.lt_succ]
exact hk
rcases this.exists_nonneg with ⟨C, C_nonneg, hC⟩
simp (discharger := positivity) only [isBigOWith_top, Real.norm_of_nonneg, pi_norm_le_iff_of_nonneg, Fin.forall_iff,
Nat.lt_succ] at hC
exact ⟨k, C, C_nonneg, fun N hN x ↦ hC x N hN⟩
