theorem TemperedDistributions.schwartz_iff_weightedDeriv_bounded {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} (hsmooth : ContDiff ℝ (↑⊤) f) : (∀ (k n : ℕ), ∃ (C : ℝ), ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C) ↔ ∀ (k n : ℕ), n ≤ k → ∃ (C : ℝ), ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C

Melrose Lemma 7.1: equivalence between the two standard ways of characterising Schwartz decay of a smooth function. The "polynomial weight" formulation (bounded ‖x‖^k ‖∂^n f(x)‖ for all k, n) is equivalent to the "(1 + ‖x‖)-weight" formulation, restricted to indices satisfying n ≤ k.

theorem TemperedDistributions.schwartz_weightedDeriv_bounded {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : SchwartzMap E F) (k n : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C

For any Schwartz function f, each weighted derivative norm (1 + ‖x‖)^k ‖∂^n f(x)‖ admits an explicit nonnegative bound expressed via the Schwartz seminorms of f.