structure DifferentialOperators.SmoothCutoff (n : ℕ) : Type

A smooth radial cutoff on Fin n → ℝ: a continuous function taking values in [0, 1] that is identically 1 on the closed unit ball and has compact support. Used to remove the singularity of 1/P_m(ξ) at the origin in the parametrix construction.

• toFun : (Fin n → ℝ) → ℝ
• eq_one_near_zero (ξ : Fin n → ℝ) : ‖ξ‖ ≤ 1 → self.toFun ξ = 1
• hasCompactSupport : HasCompactSupport self.toFun
• nonneg (ξ : Fin n → ℝ) : 0 ≤ self.toFun ξ
• le_one (ξ : Fin n → ℝ) : self.toFun ξ ≤ 1
• continuous_toFun : Continuous self.toFun

noncomputable def DifferentialOperators.parametrixSymbol {n : ℕ} (m : ℕ) (P : MvPolynomial (Fin n) ℂ) (φ : SmoothCutoff n) : (Fin n → ℝ) → ℂ

The parametrix symbol associated to a polynomial P of order m and a smooth cutoff φ: q(ξ) = (1 − φ(ξ)) / P_m(ξ) where P_m is the principal symbol, with the convention q(ξ) = 0 wherever the principal symbol vanishes.

theorem DifferentialOperators.parametrixSymbol_eq_zero_near_zero {n : ℕ} (m : ℕ) (P : MvPolynomial (Fin n) ℂ) (φ : SmoothCutoff n) (ξ : Fin n → ℝ) (hξ : ‖ξ‖ ≤ 1) : parametrixSymbol m P φ ξ = 0

The parametrix symbol vanishes on the closed unit ball, since the cutoff φ is identically 1 there.

theorem DifferentialOperators.parametrixSymbol_bound {n : ℕ} (m : ℕ) (P : MvPolynomial (Fin n) ℂ) (φ : SmoothCutoff n) (hP : IsElliptic n m P) (hn : 0 < n) : ∃ (C : ℝ), 0 < C ∧ ∀ (ξ : Fin n → ℝ), ‖parametrixSymbol m P φ ξ‖ ≤ C / ‖ξ‖ ^ m

For an elliptic polynomial P of order m, the parametrix symbol is bounded by C / ‖ξ‖^m outside the support of the cutoff. The constant C comes from the elliptic lower bound on the principal symbol.

theorem DifferentialOperators.continuous_parametrixSymbol {n : ℕ} (m : ℕ) (P : MvPolynomial (Fin n) ℂ) (φ : SmoothCutoff n) (hP : IsElliptic n m P) : Continuous (parametrixSymbol m P φ)

The parametrix symbol is continuous on all of Fin n → ℝ: locally constant zero on the unit ball, and continuous as (1 − φ)/P_m away from it (using ellipticity to ensure P_m ≠ 0).

theorem DifferentialOperators.parametrixSymbol_polynomial_decay {n : ℕ} (m : ℕ) (P : MvPolynomial (Fin n) ℂ) (φ : SmoothCutoff n) (hP : IsElliptic n m P) (hn : 0 < n) : ∃ (C : ℝ), 0 < C ∧ ∀ (ξ : Fin n → ℝ), ‖parametrixSymbol m P φ ξ‖ ≤ C * (1 + ‖ξ‖)⁻¹ ^ m

The parametrix symbol decays like (1 + ‖ξ‖)^{-m}: a uniform polynomial decay estimate, which is the relevant tempered-symbol bound.

theorem DifferentialOperators.elliptic_parametrix_construction {n m : ℕ} {P : MvPolynomial (Fin n) ℂ} (hP : IsElliptic n m P) : ∃ (F : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ), IsParametrix P F ∧ singularSupport F ⊆ {0}

Existence of a parametrix for an elliptic constant-coefficient differential operator (cf. Melrose, parametrix construction): for every elliptic polynomial P there exists a tempered distribution F that is a parametrix for P and whose singular support is contained in {0}.