theorem SchwartzMap.seminorm_translate_sub_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (φ : SchwartzMap E ℂ) (k n : ℕ) (h : E) (hh : ‖h‖ ≤ 1) : (SchwartzMap.seminorm ℂ k n) ((compSubConstCLM ℂ h) φ - φ) ≤ 2 ^ k * ((Finset.Iic (k, n + 1)).sup fun (m : ℕ × ℕ) => SchwartzMap.seminorm ℂ m.1 m.2) φ * ‖h‖

Quantitative continuity of translation on Schwartz space: for any (k, n), the Schwartz (k,n)-seminorm of the difference τ_h φ − φ is controlled linearly by ‖h‖ for ‖h‖ ≤ 1, with constant given by a finite supremum of Schwartz seminorms of φ. Used to deduce continuity of h ↦ τ_h φ in h.

theorem SchwartzMap.compSubConstCLM_sub_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (φ : SchwartzMap E ℂ) (x x₀ : E) : (compSubConstCLM ℂ x) φ - (compSubConstCLM ℂ x₀) φ = (compSubConstCLM ℂ x₀) ((compSubConstCLM ℂ (x - x₀)) φ - φ)

Cocycle identity for Schwartz translation: the difference of two translates of φ at points x and x₀ factors through translation by x₀ of the difference τ_{x − x₀} φ − φ.