noncomputable def DifferentialOperators.tempDistSchwartzConv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (u : TemperedDistribution E ℂ) (φ : SchwartzMap E ℂ) : E → ℂ

The convolution of a tempered distribution u with a Schwartz function φ, viewed as a function x ↦ ⟨u, φ(· - x)⟩ on E.

@[simp]

theorem DifferentialOperators.tempDistSchwartzConv_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (u : TemperedDistribution E ℂ) (φ : SchwartzMap E ℂ) (x : E) : tempDistSchwartzConv u φ x = u ((SchwartzMap.compSubConstCLM ℂ x) φ)

Pointwise unfolding of tempDistSchwartzConv: its value at x is u applied to the translated Schwartz function y ↦ φ(y - x).

theorem DifferentialOperators.tempDistSchwartzConv_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (u : TemperedDistribution E ℂ) (φ : SchwartzMap E ℂ) : ContDiff ℝ (↑⊤) (tempDistSchwartzConv u φ)

The convolution tempDistSchwartzConv u φ of a tempered distribution u with a Schwartz function φ is smooth (C^∞).

theorem DifferentialOperators.tempDistSchwartzConv_polynomial_growth {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (u : TemperedDistribution E ℂ) (φ : SchwartzMap E ℂ) : ∃ (k : ℕ) (C : ℝ), 0 ≤ C ∧ ∀ (x : E), ‖tempDistSchwartzConv u φ x‖ ≤ C * (1 + ‖x‖) ^ k

The convolution tempDistSchwartzConv u φ of a tempered distribution u with a Schwartz function φ has polynomial growth: there exist k : ℕ and C ≥ 0 such that ‖(u * φ)(x)‖ ≤ C (1 + ‖x‖)^k for all x.

theorem DifferentialOperators.tempDistSchwartzConv_deriv_right {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (u : TemperedDistribution E ℂ) (φ : SchwartzMap E ℂ) (x h : E) : (fderiv ℝ (tempDistSchwartzConv u φ) x) h = -tempDistSchwartzConv u ((SchwartzMap.postcompCLM ((ContinuousLinearMap.apply ℝ ℂ) h)) ((SchwartzMap.fderivCLM ℝ E ℂ) φ)) x

Differentiating the convolution u * φ of a tempered distribution and a Schwartz function with respect to the spatial variable: the directional derivative in direction h equals minus the convolution of u with the directional derivative of φ.

theorem DifferentialOperators.tempDistSchwartzConv_vanishes_away_from_support {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (u : TemperedDistribution E ℂ) (φ : SchwartzMap E ℂ) (x : E) (hdisjoint : Disjoint (tsupport fun (y : E) => φ (y - x)) (closure (Distribution.dsupport ⇑u))) : tempDistSchwartzConv u φ x = 0

If the support of y ↦ φ(y - x) is disjoint from the closure of the distributional support of u, then (u * φ)(x) = 0.

theorem DifferentialOperators.theorem_11_6_full {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 ∧ lineDeriv ℝ (temperedConvolution u φ) x m = temperedConvolution u (LineDeriv.lineDerivOp m φ) x) ∧ (HasCompactSupport ⇑φ → Function.support (temperedConvolution u φ) ⊆ Distribution.dsupport ⇑u + tsupport ⇑φ)

Full statement of Melrose's Theorem 11.6 for the convolution of a tempered distribution with a Schwartz function: the directional derivative in m can be moved either onto u or onto φ, and if φ is compactly supported the support of u * φ is contained in dsupport u + supp φ.

theorem DifferentialOperators.temperedConvolution_iterPartialDeriv_coord {n : ℕ} (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) (j : Fin n) (k : ℕ) (x : EuclideanSpace ℝ (Fin n)) : temperedConvolution (SobolevSpace.iteratedPartialDerivDistrib n j k u) φ x = temperedConvolution u (SchwartzRepresentation.iterSchwartzDerivCoord j k φ) x

Iterated coordinate-direction partial derivatives transfer between the distribution and the Schwartz factor of a tempered convolution: (∂_j^k u) * φ = u * (∂_j^k φ) pointwise on Euclidean space.