theorem DifferentialOperators.schwartzTranslateReflect_decay {n : ℕ} (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) (x : EuclideanSpace ℝ (Fin n)) (k l : ℕ) : ∃ (C : ℝ), ∀ (y : EuclideanSpace ℝ (Fin n)), ‖y‖ ^ k * ‖iteratedFDeriv ℝ l (fun (z : EuclideanSpace ℝ (Fin n)) => φ (x - z)) y‖ ≤ C

Schwartz decay of the translated–reflected function y ↦ φ(x − y): for every multi-index orders k, l, the weighted derivative norm is uniformly bounded in y.

noncomputable def DifferentialOperators.schwartzTranslateReflect {n : ℕ} (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) (x : EuclideanSpace ℝ (Fin n)) : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ

The Schwartz function y ↦ φ(x − y) obtained by translating and reflecting a Schwartz function φ by x.

noncomputable def DifferentialOperators.temperedConvolution {n : ℕ} (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) : EuclideanSpace ℝ (Fin n) → ℂ

Convolution of a tempered distribution u with a Schwartz function φ: pointwise (u ∗ φ)(x) = ⟨u, φ(x − ·)⟩.

theorem DifferentialOperators.hormander_convolution_smooth {n : ℕ} (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) : ContDiff ℝ (↑⊤) (temperedConvolution u φ)

Hörmander Theorem 4.1.1 (Melrose Theorem 11.6) — smoothness: the convolution u ∗ φ of a tempered distribution with a Schwartz function is C^∞.

theorem DifferentialOperators.hormander_convolution_polynomial_growth {n : ℕ} (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) : ∃ (C : ℝ) (k : ℕ), 0 < C ∧ ∀ (x : EuclideanSpace ℝ (Fin n)), ‖temperedConvolution u φ x‖ ≤ C * (1 + ‖x‖ ^ 2) ^ (↑k / 2)

The convolution u ∗ φ has polynomial growth: there exist C > 0 and k : ℕ with ‖(u ∗ φ)(x)‖ ≤ C · ⟨x⟩^k.

theorem DifferentialOperators.hormander_convolution_deriv_right {n : ℕ} (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) (m x : EuclideanSpace ℝ (Fin n)) : lineDeriv ℝ (temperedConvolution u φ) x m = temperedConvolution u (LineDeriv.lineDerivOp m φ) x

Differentiating the convolution on the right: ∂_m (u ∗ φ)(x) = (u ∗ (∂_m φ))(x).

theorem DifferentialOperators.hormander_convolution_deriv_left {n : ℕ} (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) (m x : EuclideanSpace ℝ (Fin n)) : temperedConvolution ((TemperedDistributions.distribDerivCLM m) u) φ x = lineDeriv ℝ (temperedConvolution u φ) x m

Differentiating the convolution on the left equals differentiating on the right: ((∂_m u) ∗ φ)(x) = ∂_m (u ∗ φ)(x).

theorem DifferentialOperators.tempered_vanishing_outside_dsupport {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (u : TemperedDistribution E F) (ψ : SchwartzMap E ℂ) (hψ : HasCompactSupport ⇑ψ) (hψ_disj : Disjoint (tsupport ⇑ψ) (Distribution.dsupport ⇑u)) : u ψ = 0

A tempered distribution u vanishes on a compactly supported Schwartz test function whose support is disjoint from the distributional support of u.

theorem DifferentialOperators.hormander_convolution_support {n : ℕ} (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) (hφ : HasCompactSupport ⇑φ) : Function.support (temperedConvolution u φ) ⊆ Distribution.dsupport ⇑u + tsupport ⇑φ

Support of u ∗ φ (when φ has compact support) is contained in dsupport u + tsupport φ.