noncomputable def DifferentialOperators.ellipticParametrix {n : ℕ} (m : ℕ) (P : MvPolynomial (Fin n) ℂ) (hP : IsElliptic n m P) : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ

An elliptic parametrix for the constant-coefficient differential operator with symbol P: a tempered distribution E such that P(D) E - δ₀ is smooth and E has singular support at the origin only. Existence is provided by parametrix_exists_with_singSupp.

theorem DifferentialOperators.ellipticParametrix_isParametrix {n : ℕ} (m : ℕ) (P : MvPolynomial (Fin n) ℂ) (hP : IsElliptic n m P) : IsParametrix P (ellipticParametrix m P hP)

The chosen elliptic parametrix is indeed a parametrix for P: it satisfies P(D) (ellipticParametrix m P hP) = δ₀ + ω for some smooth ω.

theorem DifferentialOperators.ellipticParametrix_singularSupport {n : ℕ} (m : ℕ) (P : MvPolynomial (Fin n) ℂ) (hP : IsElliptic n m P) : singularSupport (ellipticParametrix m P hP) ⊆ {0}

The singular support of the elliptic parametrix is contained in {0}, reflecting that elliptic parametrices have a singularity only at the origin.

theorem DifferentialOperators.elliptic_isHypoelliptic {n : ℕ} (m : ℕ) (P : MvPolynomial (Fin n) ℂ) (hP : IsElliptic n m P) : IsHypoelliptic P

Elliptic operators are hypoelliptic: this packages the existence of a parametrix with singular support at the origin, which implies that solutions of P(D) u = f have the same singular support as f.