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

The principal symbol of P (a polynomial in the cotangent variables of order m) evaluated at a real covector ξ ∈ ℝⁿ, viewed as a complex number by inclusion ℝ ↪ ℂ.

theorem DifferentialOperators.continuous_evalPrincipalSymbolReal {n : ℕ} (m : ℕ) (P : MvPolynomial (Fin n) ℂ) : Continuous (evalPrincipalSymbolReal m P)

The real-evaluation of the principal symbol ξ ↦ σ_m(P)(ξ) is continuous in ξ ∈ ℝⁿ, since it is a polynomial composed with the coordinate-wise inclusion ℝ ↪ ℂ.

theorem DifferentialOperators.eval_homogeneous_smul {n : ℕ} (m : ℕ) (P : MvPolynomial (Fin n) ℂ) (t : ℂ) (ξ : Fin n → ℂ) : (MvPolynomial.eval fun (i : Fin n) => t * ξ i) (principalSymbol n m P) = t ^ m * (MvPolynomial.eval ξ) (principalSymbol n m P)

Homogeneity of the principal symbol: scaling the variable by t multiplies the value of the principal symbol of degree m by t^m. Used to reduce the elliptic lower bound on ℝⁿ to a lower bound on the unit sphere.

theorem DifferentialOperators.sphere_nonempty_of_pos {n : ℕ} (hn : 0 < n) : (Metric.sphere 0 1).Nonempty

The unit sphere of Fin n → ℝ is nonempty whenever n > 0, since this guarantees the underlying space has nontrivial points of unit norm.

theorem DifferentialOperators.elliptic_lower_bound_sphere {n : ℕ} (m : ℕ) (P : MvPolynomial (Fin n) ℂ) (hP : IsElliptic n m P) (hn : 0 < n) : ∃ (c : ℝ), 0 < c ∧ ∀ (ξ : Fin n → ℝ), ‖ξ‖ = 1 → c ≤ ‖evalPrincipalSymbolReal m P ξ‖

Sphere version of the elliptic lower bound: for any elliptic polynomial P of order m, the principal symbol is bounded below in modulus by a positive constant on the unit sphere. Proved by extracting a minimizer of the continuous function ‖σ_m(P)(ξ)‖ on the compact sphere and noting that the minimum is nonzero by ellipticity.

theorem DifferentialOperators.elliptic_lower_bound {n : ℕ} (m : ℕ) (P : MvPolynomial (Fin n) ℂ) (hP : IsElliptic n m P) (hn : 0 < n) : ∃ (c : ℝ), 0 < c ∧ ∀ (ξ : Fin n → ℝ), c * ‖ξ‖ ^ m ≤ ‖evalPrincipalSymbolReal m P ξ‖

Elliptic lower bound on all of ℝⁿ: for an elliptic operator of order m, there exists a positive constant c such that c · ‖ξ‖^m ≤ ‖σ_m(P)(ξ)‖ for every ξ ∈ ℝⁿ. Proved by combining the sphere lower bound with the homogeneity σ_m(P)(tξ) = t^m σ_m(P)(ξ).