English
For any k,n there exists a bound c≥0 such that ∥x∥^k ∥iteratedFDeriv^n f x∥ ≤ c for all x in E.
Русский
Для любых k,n существует неотрицанная граница c такая, что ∥x∥^k ∥iteratedFDeriv^n f x∥ ≤ c для всех x ∈ E.
LaTeX
$$$ \exists c\in\mathbb{R}, c \ge 0 \wedge \forall x, \|x\|^k \|iteratedFDeriv\_\mathbb{R}^n f x\| \le c $$$
Lean4
/-- All derivatives of a Schwartz function are rapidly decaying. -/
theorem decay (f : 𝓢(E, F)) (k n : ℕ) : ∃ C : ℝ, 0 < C ∧ ∀ x, ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C :=
by
rcases f.decay' k n with ⟨C, hC⟩
exact ⟨max C 1, by positivity, fun x => (hC x).trans (le_max_left _ _)⟩