def DifferentialOperators.IsSmooth {n : ℕ} (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : Prop

A tempered distribution u is smooth if it is represented by integration against a smooth function f : ℝⁿ → ℂ, i.e. u(ψ) = ∫ ψ · f for all Schwartz test functions ψ.

def DifferentialOperators.IsSmoothCutoff {n : ℕ} (φ : EuclideanSpace ℝ (Fin n) → ℂ) : Prop

A smooth cutoff function: a C^∞ complex-valued function on ℝⁿ with compact support.

def DifferentialOperators.singSupp {n : ℕ} (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : Set (EuclideanSpace ℝ (Fin n))

The singular support of a tempered distribution u: the set of points x₀ for which no smooth cutoff function φ with φ x₀ ≠ 0 makes the localised distribution φ · u smooth.

theorem DifferentialOperators.cutoff_identity_near {n : ℕ} (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (x₀ : EuclideanSpace ℝ (Fin n)) (hx : x₀ ∉ singSupp u) : ∃ (φ : EuclideanSpace ℝ (Fin n) → ℂ), IsSmoothCutoff φ ∧ (∃ (U : Set (EuclideanSpace ℝ (Fin n))), IsOpen U ∧ x₀ ∈ U ∧ ∀ y ∈ U, φ y = 1) ∧ IsSmooth ((TemperedDistribution.smulLeftCLM ℂ φ) u)

Near any point outside the singular support of u, one can choose a smooth cutoff φ that equals 1 on a neighbourhood of the point and such that φ · u is smooth.

theorem DifferentialOperators.smul_decomposition {n : ℕ} (φ : EuclideanSpace ℝ (Fin n) → ℂ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : (TemperedDistribution.smulLeftCLM ℂ φ) u + (TemperedDistribution.smulLeftCLM ℂ (1 - φ)) u = u

Partition of unity decomposition for distributions: any tempered distribution u splits as φ · u + (1 - φ) · u = u for any smooth function φ.

theorem DifferentialOperators.constCoeffDiffOp_preserves_smooth {n : ℕ} (P : MvPolynomial (Fin n) ℂ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hu : IsSmooth u) : IsSmooth ((constCoeffDiffOp n P) u)

A constant-coefficient differential operator P(D) maps smooth distributions to smooth distributions: if u is represented by a smooth function then so is P(D) u.

theorem DifferentialOperators.locality_vanishing {n : ℕ} (P : MvPolynomial (Fin n) ℂ) (φ ψ : EuclideanSpace ℝ (Fin n) → ℂ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hψ : IsSmoothCutoff ψ) (hsup : ∀ (x : EuclideanSpace ℝ (Fin n)), ψ x ≠ 0 → φ x = 1) : (TemperedDistribution.smulLeftCLM ℂ ψ) ((constCoeffDiffOp n P) ((TemperedDistribution.smulLeftCLM ℂ (1 - φ)) u)) = 0

Locality of differential operators: if the cutoff ψ is supported where φ = 1, then ψ · P(D) ((1 - φ) · u) = 0 because 1 - φ vanishes on the support of ψ.

theorem DifferentialOperators.smul_cutoff_smooth {n : ℕ} (ψ : EuclideanSpace ℝ (Fin n) → ℂ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hψ : IsSmoothCutoff ψ) (hu : IsSmooth u) : IsSmooth ((TemperedDistribution.smulLeftCLM ℂ ψ) u)

Multiplication by a smooth cutoff preserves smoothness of distributions: if u is smooth and ψ is a smooth compactly supported function, then ψ · u is smooth.

theorem DifferentialOperators.exists_cutoff_in_open {n : ℕ} (U : Set (EuclideanSpace ℝ (Fin n))) (hU : IsOpen U) (x₀ : EuclideanSpace ℝ (Fin n)) (hx : x₀ ∈ U) : ∃ (ψ : EuclideanSpace ℝ (Fin n) → ℂ), IsSmoothCutoff ψ ∧ ψ x₀ ≠ 0 ∧ ∀ (y : EuclideanSpace ℝ (Fin n)), ψ y ≠ 0 → y ∈ U

For any open set U and point x₀ ∈ U, there exists a smooth cutoff ψ with ψ x₀ ≠ 0 and whose support is contained in U.

theorem DifferentialOperators.singSupp_constCoeffDiffOp_subset {n : ℕ} (P : MvPolynomial (Fin n) ℂ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : singSupp ((constCoeffDiffOp n P) u) ⊆ singSupp u

Pseudolocal property of differential operators: a constant-coefficient differential operator does not enlarge the singular support, i.e. singSupp (P(D) u) ⊆ singSupp u. This is the key step in proving elliptic regularity.