theorem TemperedDistributions.SchwartzMap.seminorm_compSubConst_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (𝕜 : Type u_2) [RCLike 𝕜] [NormedSpace 𝕜 ℂ] [SMulCommClass ℝ 𝕜 ℂ] (k n : ℕ) (φ : SchwartzMap E ℂ) (x : E) : (SchwartzMap.seminorm 𝕜 k n) ((SchwartzMap.compSubConstCLM 𝕜 x) φ) ≤ (1 + ‖x‖) ^ k * 2 ^ k * ((Finset.Iic (k, n)).sup fun (m : ℕ × ℕ) => SchwartzMap.seminorm 𝕜 m.1 m.2) φ

Quantitative continuity of translation on Schwartz space: the (k, n)-th Schwartz seminorm of the translated Schwartz function φ(· − x) is bounded by (1 + ‖x‖)^k · 2^k times the supremum of the seminorms with indices in Iic (k, n).