theorem ConeSupport.clm_norm_le_sum_basis {n : ℕ} (L : E n →L[ℝ] ℂ) : ‖L‖ ≤ ∑ i : Fin n, ‖L (EuclideanSpace.single i 1)‖

For a continuous linear functional on E n = EuclideanSpace ℝ (Fin n), the operator norm is bounded by the sum of the absolute values on the standard basis vectors.

theorem ConeSupport.norm_iteratedFDeriv_fderiv_le_sum {n m : ℕ} (f : E n → ℂ) (hf : ContDiff ℝ (↑⊤) f) (x : E n) : ‖iteratedFDeriv ℝ m (fderiv ℝ f) x‖ ≤ ∑ i : Fin n, ‖iteratedFDeriv ℝ m (fun (y : E n) => (fderiv ℝ f y) (EuclideanSpace.single i 1)) x‖

The norm of the iterated derivative of fderiv f at x is bounded by the sum over the standard basis directions eᵢ of the iterated-derivative norms of the directional derivative y ↦ ⟨df y, eᵢ⟩.

theorem ConeSupport.temperedConvolution_iteratedFDeriv_polynomial_growth {n : ℕ} (u : TemperedDistribution (E n) ℂ) (φ : SchwartzMap (E n) ℂ) (m : ℕ) : ∃ (k : ℕ) (C : ℝ), ∀ (x : E n), ‖iteratedFDeriv ℝ m (DifferentialOperators.temperedConvolution u φ) x‖ ≤ C * (1 + ‖x‖) ^ k

All iterated derivatives of u ∗ φ for a tempered distribution u and Schwartz φ have polynomial growth: there exist k and C so that ‖∂^m(u ∗ φ)(x)‖ ≤ C (1 + ‖x‖)^k.

theorem ConeSupport.schwartzConvolution_eq_integral {n : ℕ} (u : TemperedDistribution (E n) ℂ) (φ θ : SchwartzMap (E n) ℂ) : (schwartzConvolution u φ) θ = ∫ (x : E n), θ x • DifferentialOperators.temperedConvolution u φ x

Pairing identity: testing the Schwartz convolution u ∗ φ against a Schwartz function θ equals the integral of θ against the pointwise tempered convolution.

theorem ConeSupport.schwartzConvolution_eq_temperateGrowth {n : ℕ} (u : TemperedDistribution (E n) ℂ) (φ : SchwartzMap (E n) ℂ) : ∃ (g : E n → ℂ), Function.HasTemperateGrowth g ∧ ∀ (θ : SchwartzMap (E n) ℂ), (schwartzConvolution u φ) θ = ∫ (x : E n), θ x • g x

The Schwartz convolution u ∗ φ is represented as integration against a smooth function g of polynomial (temperate) growth.

theorem ConeSupport.smulLeftCLM_schwartzConvolution_eq_schwartz {n : ℕ} (u : TemperedDistribution (E n) ℂ) (φ : SchwartzMap (E n) ℂ) (ψ : E n → ℂ) (hψ_smooth : ContDiff ℝ (↑⊤) ψ) (hψ_compact : HasCompactSupport ψ) : ∃ (f : SchwartzMap (E n) ℂ), (TemperedDistribution.smulLeftCLM ℂ ψ) (schwartzConvolution u φ) = (SchwartzMap.toTemperedDistributionCLM (E n) ℂ MeasureTheory.volume) f

For any smooth compactly supported cutoff ψ, the product ψ · (u ∗ φ) is represented by a Schwartz function.

theorem ConeSupport.isSmoothNear_schwartzConvolution {n : ℕ} (u : TemperedDistribution (E n) ℂ) (φ : SchwartzMap (E n) ℂ) (x₀ : E n) : IsSmoothNear (schwartzConvolution u φ) x₀

The Schwartz convolution u ∗ φ is smooth near every point: a cutoff times it agrees with a Schwartz function on a neighbourhood of any point.

theorem ConeSupport.singularSupport_schwartzConvolution_eq_empty {n : ℕ} (u : TemperedDistribution (E n) ℂ) (φ : SchwartzMap (E n) ℂ) : singularSupport (schwartzConvolution u φ) = ∅

The singular support of u ∗ φ is empty: the convolution is smooth everywhere.

theorem ConeSupport.coneSingularSupport_schwartzConvolution_subset {n : ℕ} (u : TemperedDistribution (E n) ℂ) (φ : SchwartzMap (E n) ℂ) : coneSingularSupport (schwartzConvolution u φ) ⊆ Sum.inr '' ConicSingularSupportSphere u

The cone singular support of u ∗ φ is contained in the spherical (direction-at-infinity) part inherited from the conic singular support sphere of u.