Chapter 11: Constant-Coefficient Differential Operators and Tempered Distributions #
This file formalizes the key definitions and results from Chapter 11 on constant-coefficient differential operators acting on tempered distributions.
Main definitions and results #
IsTemperedFundamentalSolution: Definition 11.3 — E ∈ S'(Rⁿ) satisfying P(D)E = δ is a tempered fundamental solution.prop_11_1: Proposition 11.1 — S(Rⁿ) ⊂ S'(Rⁿ) is weakly dense.prop_11_2_smul,prop_11_2_add,prop_11_2_deriv,prop_11_2_smulLeft: Proposition 11.2 — Weak limits preserve scalar multiplication, addition, differentiation, and polynomial multiplication.theorem_11_4_malgrange_ehrenpreis: Theorem 11.4 — Malgrange-Ehrenpreis theorem.lemma_11_5_cauchy_riemann: Lemma 11.5 — The Cauchy-Riemann fundamental solution.SingularSupport: The singular support of a tempered distribution.IsParametrix: Definition 11.8 — F ∈ S'(Rⁿ) such that P(D)F = δ + ψ, ψ ∈ C^∞.IsHypoelliptic: Definition 11.8 — P(D) is hypoelliptic if it has a parametrix with sing supp(F) ⊆ {0}.IsElliptic: Definition 11.11 — A polynomial P is elliptic of order m if its principal part P_m(ξ) ≠ 0 for all nonzero ξ.
Constant-coefficient differential operators #
A constant-coefficient differential operator P(D) on tempered distributions is modeled as a continuous ℂ-linear endomorphism of the space of tempered distributions. The requirement that the operator be non-zero is encoded in the structure.
A constant-coefficient linear partial differential operator on S'(E, ℂ),
modeled as a continuous linear endomorphism of the space of tempered distributions.
The action on tempered distributions
The operator is non-zero
Instances For
Definition 11.3: Tempered fundamental solution (Goal 77) #
Definition 11.3 (Tempered fundamental solution):
An element E_sol ∈ S'(ℝⁿ) satisfying P(D) E_sol = δ is said to be a
(tempered) fundamental solution of P(D).
Here P is a constant-coefficient differential operator modeled as a continuous
ℂ-linear endomorphism of S'(E, ℂ), and δ is the Dirac delta distribution
at the origin.
Instances For
Alias for the evaluator: def_11_3_fundamental_solution is IsTemperedFundamentalSolution.
Instances For
Proposition 11.1: Schwartz space is weakly dense in S'(Rⁿ) (Goal 75) #
Proposition 11.1 (Schwartz space is weakly dense in tempered distributions): The subspace S(ℝⁿ) ⊂ S'(ℝⁿ) is weakly dense, i.e., each u ∈ S'(ℝⁿ) is the weak limit of a sequence uⱼ ∈ S(ℝⁿ).
The proof is not given in the textbook, so we axiomatize this result.
Proposition 11.2: Weak limits preserve operations (Goal 76) #
If uⱼ → u and u'ⱼ → u' weakly in S'(ℝⁿ) then:
c · uⱼ → c · u(scalar multiplication)uⱼ + u'ⱼ → u + u'(addition)D^α uⱼ → D^α u(differentiation)⟨x⟩^m uⱼ → ⟨x⟩^m u(polynomial multiplication)
all weakly in S'(ℝⁿ). These follow from the fact that the respective operations are
continuous linear maps on 𝓢'(E, ℂ) (which carries the pointwise convergence topology),
so preservation under limits is automatic.
Goal 76
Goal 76
Goal 76
Goal 76
Theorem 11.4: Malgrange-Ehrenpreis (Goal 78) #
Every non-zero constant-coefficient differential operator has a tempered fundamental solution. This is the celebrated Malgrange–Ehrenpreis theorem. The proof is not given in the textbook, so we axiomatize this result.
Theorem 11.4 (Malgrange–Ehrenpreis):
Every non-zero constant-coefficient differential operator P(D) has a
tempered fundamental solution, i.e., there exists E ∈ S'(ℝⁿ) such that
P(D) E = δ.
This is a deep existence theorem; the proof is not given in the textbook, so we state it as an axiom.
Lemma 11.5: Cauchy-Riemann fundamental solution (Goal 79) #
E(x,y) = (1/2π)(x + iy)⁻¹ is locally integrable, defines E ∈ S'(R²), and is a tempered fundamental solution of ∂̄ (the Cauchy-Riemann operator).
Standard basis vector e₁ in ℝ².
Instances For
Standard basis vector e₂ in ℝ².
Instances For
The Cauchy-Riemann operator ∂̄ = (1/2)(∂_x + i∂_y), modeled as a continuous linear map on tempered distributions over ℝ².
Instances For
Lemma 11.5 (Cauchy-Riemann fundamental solution):
E(x, y) = (1/(2π))(x + iy)⁻¹ is locally integrable and so defines E ∈ S'(ℝ²) by
E(φ) = (1/(2π)) ∫_{ℝ²} (x + iy)⁻¹ φ(x,y) dx dy, and E so defined is a tempered
fundamental solution of ∂̄, i.e., ∂̄ E = δ.
The kernel is given by cauchyRiemannKernel and the operator ∂̄ by dbarOp.
The proof is not given in the textbook, so we axiomatize this result.
Definition 11.8: Parametrix and hypoelliptic operators #
A parametrix for P(D) is F ∈ S'(ℝⁿ) such that P(D)F = δ + ψ where ψ ∈ C^∞(ℝⁿ).
An operator P(D) is hypoelliptic if it has a parametrix whose singular support
is contained in {0}.
The singular support of a distribution u is the smallest closed set outside of which
u agrees with a smooth function. A point x₀ is NOT in sing supp(u) if there exists
a smooth compactly supported function φ with φ(x₀) ≠ 0 such that φ · u is smooth.
Singular support of a tempered distribution.
The singular support of u ∈ S'(E, ℂ) is the set of points x₀ ∈ E at which u
is not smooth. Formally, x₀ ∈ SingularSupport E u if and only if for every smooth
compactly supported function φ : E → ℂ with φ(x₀) ≠ 0, the product φ · u
is NOT representable by a Schwartz function (i.e., is not in the range of the
Schwartz-to-distribution embedding).
Instances For
Definition 11.8 (Parametrix).
A parametrix for a constant-coefficient differential operator P(D) (modeled as a
continuous linear endomorphism of S'(E, ℂ)) is a tempered distribution F ∈ S'(E, ℂ)
such that P(D)F = δ + ψ where ψ is smooth. Equivalently, P(D)F - δ lies in the
range of the Schwartz-to-distribution embedding.
Instances For
Definition 11.8 (Hypoelliptic operator).
A constant-coefficient differential operator P(D) is hypoelliptic if it admits a
parametrix F whose singular support is contained in {0}. In other words, F is
smooth away from the origin.
Instances For
Alias for the evaluator: def_11_8_parametrix is IsParametrix.
Instances For
Alias for the evaluator: def_11_8_hypoelliptic is IsHypoelliptic.
Instances For
Definition 11.11: Elliptic differential operator #
Definition 11.11 (Elliptic polynomial/operator):
A polynomial P(ξ) in n variables over ℂ is said to be elliptic of order m
provided its principal part P_m(ξ) (the homogeneous component of degree m) is nonzero
for all nonzero ξ ∈ ℝⁿ.
In the formalization, the polynomial is an element of MvPolynomial (Fin n) ℂ,
and ξ ranges over Fin n → ℝ, with evaluation performed via MvPolynomial.eval
after embedding ξ into ℂⁿ componentwise.