theorem DifferentialOperators.constCoeffDiffOp_hasCompactSupport {n : ℕ} (P : MvPolynomial (Fin n) ℂ) (F : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hFcs : ∃ (K : Set (EuclideanSpace ℝ (Fin n))), IsCompact K ∧ ∀ (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ), (∀ y ∈ K, φ y = 0) → F φ = 0) : HasCompactSupport ((constCoeffDiffOp n P) F)

A constant-coefficient differential operator preserves compact support: if the tempered distribution F vanishes outside a compact K, then so does P(D) F.

theorem DifferentialOperators.delta_hasCompactSupport {n : ℕ} : HasCompactSupport (TemperedDistribution.delta 0)

The Dirac delta distribution δ_0 has compact support, namely {0}.

theorem DifferentialOperators.sub_hasCompactSupport {n : ℕ} (μ ν : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hμ : HasCompactSupport μ) (hν : HasCompactSupport ν) : HasCompactSupport (μ - ν)

Subtraction of two compactly supported distributions has compact support.

theorem DifferentialOperators.singularSupport_subset_sub_smooth {n : ℕ} (u v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hv_smooth : ∀ (y : EuclideanSpace ℝ (Fin n)), isSmoothNear v y) : singularSupport u ⊆ singularSupport (u - v)

Adding a globally smooth distribution does not enlarge the singular support: if v is smooth everywhere, then singularSupport u ⊆ singularSupport (u - v).

theorem DifferentialOperators.singularSupport_sub_smooth_subset {n : ℕ} (u v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hv_smooth : ∀ (y : EuclideanSpace ℝ (Fin n)), isSmoothNear v y) : singularSupport (u - v) ⊆ singularSupport u

Subtracting a globally smooth distribution does not enlarge the singular support, giving the reverse inclusion singularSupport (u - v) ⊆ singularSupport u.

theorem DifferentialOperators.parametrix_distribConvolution_singSupp_bound {n : ℕ} (P : MvPolynomial (Fin n) ℂ) (F : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hFparam : IsParametrix P F) (hFcs : ∃ (K : Set (EuclideanSpace ℝ (Fin n))), IsCompact K ∧ ∀ (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ), (∀ y ∈ K, φ y = 0) → F φ = 0) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hpsi_cs : HasCompactSupport ((constCoeffDiffOp n P) F - TemperedDistribution.delta 0)) : singularSupport (u - distribConvolution ((constCoeffDiffOp n P) F - TemperedDistribution.delta 0) u hpsi_cs) ⊆ singularSupport F + singularSupport ((constCoeffDiffOp n P) u)

Parametrix singular-support bound via distributional convolution: writing P(D) F = δ + ψ where ψ = P(D) F - δ has compact support, the singular support of u - ψ * u is contained in singularSupport F + singularSupport (P(D) u). This is the convolution form of the parametrix identity used in pseudolocal elliptic regularity.

theorem DifferentialOperators.parametrix_singSupp_u_bound {n : ℕ} (P : MvPolynomial (Fin n) ℂ) (F : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hFparam : IsParametrix P F) (hFcs : ∃ (K : Set (EuclideanSpace ℝ (Fin n))), IsCompact K ∧ ∀ (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ), (∀ y ∈ K, φ y = 0) → F φ = 0) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : singularSupport u ⊆ singularSupport F + singularSupport ((constCoeffDiffOp n P) u)

Pseudolocal elliptic regularity via the parametrix: for any tempered distribution u, singularSupport u ⊆ singularSupport F + singularSupport (P(D) u), where F is a parametrix for P. In particular, when Pu is smooth, u is smooth wherever F is smooth — the heart of the parametrix method.