The principal symbol of a polynomial P of (assumed) order m:
the degree-m homogeneous component of P.
Instances For
Unfolding lemma: principalSymbol n m P = homogeneousComponent m P.
A polynomial P(ξ) (of order m) is elliptic if its principal
symbol P_m(ξ) does not vanish for any nonzero real vector ξ ∈ ℝⁿ.
(See Melrose, Definition 11.11.)
Instances For
The Fourier symbol P(2πiξ) of the differential operator P(D),
viewed as a function ℝⁿ → ℂ.
Instances For
The constant-coefficient differential operator P(D) acting on
tempered distributions, defined as the Fourier multiplier with symbol
P(2πiξ).
Instances For
A tempered distribution E is a fundamental solution of P(D)
if P(D) E = δ₀.
Instances For
Theorem 11.4 (Melrose). Every nonzero constant-coefficient differential
operator P(D) admits a tempered fundamental solution.
A tempered distribution u is smooth near a point x₀ if there
exists an open neighbourhood U of x₀ on which u is represented by a
smooth function (under pairing with Schwartz functions supported in U).
Instances For
The singular support of u: the set of points x₀ near which
u fails to be smooth.
Instances For
u vanishes on the set U if it sends every test function
supported in U to zero.
Instances For
Locality of P(D). If u vanishes on the open set U, then so
does P(D) u.
Partition of u by a temperate cutoff: for any χ of temperate
growth, χ · u + (1 - χ) · u = u.
If χ is a smooth temperate cutoff supported in an open set U on
which u is represented by a smooth function f, then χ · u is
globally smooth — represented by χ · f.
If χ ≡ 1 on the open set V, then (1 - χ) · u vanishes on
V.
Smooth cutoff in an open set. Around any point x₀ of an open
set U, there is a smooth temperate function χ vanishing outside U
and equal to 1 on a smaller open neighbourhood of x₀.
Cutoff decomposition near a smooth point. If u is smooth near
x₀, then u = v + w where v is globally smooth and w vanishes
on an open neighbourhood U of x₀.
The sum of a globally smooth distribution v and one (w) that
vanishes on a neighbourhood U of x₀ is smooth near x₀.
If u vanishes on the open set U, then u is smooth at every
point of U (with smooth representative 0).
If u is globally smooth (represented by a smooth f), then
P(D) u is also globally smooth — represented by an explicit smooth g
(the classical action of P(D) on f).
P(D) preserves smoothness at every point. If u is smooth at
every point, then so is P(D) u.
Singular support is contracted by P(D):
singsupp(P(D) u) ⊆ singsupp u.
Scalar multiplication is sequentially weakly continuous in 𝓢':
if u j → u₀, then c · u j → c · u₀.
Addition is sequentially weakly continuous in 𝓢':
if u j → u₀ and u' j → u₀', then u j + u' j → u₀ + u₀'.
P(D) is sequentially weakly continuous: weakly convergent sequences
of distributions are taken to weakly convergent sequences.
Left multiplication by a function g (as a CLM on 𝓢') is
sequentially weakly continuous.
Combined weak continuity package. Packaging the four preceding
weak-continuity results into one statement; this is the conjunction
recorded as proposition_11_2 (Melrose, Proposition 11.2).
Alias of DifferentialOperators.tendsto_smul_add_diffOp_smulLeft.
Combined weak continuity package. Packaging the four preceding
weak-continuity results into one statement; this is the conjunction
recorded as proposition_11_2 (Melrose, Proposition 11.2).
A tempered distribution F is a parametrix for P(D) if
P(D) F - δ₀ has empty singular support, i.e. it is smooth everywhere.
(See Melrose, Definition 11.8.)
Instances For
P(D) is hypoelliptic if it admits a parametrix F whose
singular support is contained in {0}.
Instances For
Existence of a smooth compactly-supported cutoff equal to 1 near
the origin. Used to localise parametrices near 0.
If φ is a smooth compactly-supported temperate function, then
φ · F has compact distributional support contained in tsupport φ.
Singular support contracts under left multiplication:
singsupp(φ · F) ⊆ singsupp F for φ a smooth temperate function.
A smooth function f that represents the tempered distribution u on
an open set U necessarily has temperate growth — a consequence of u
itself being a tempered distribution and standard local-to-global growth
estimates.
The pointwise product φ · f of a Schwartz function and a smooth
function f of temperate growth is integrable.
Smoothness near a point is closed under subtraction: if a and b
are smooth near x₀, then so is a - b.
If F is a parametrix for P(D) with singular support ⊆ {0} and
φ ≡ 1 on a neighbourhood of 0, then φ · F is also a parametrix.
Cutting F by φ does not destroy the parametrix property — the
"tail" (1 - φ) · F is globally smooth.
Compact support arrangement. Any parametrix with singular support
in {0} can be replaced by a parametrix F' of compact distributional
support (and unchanged singular support). Achieved by multiplying with a
smooth compactly-supported cutoff φ that equals 1 near 0.
Smooth-remainder splitting. For any u, the parametrix identity
gives a decomposition u = v + w with v = P(D) F - δ₀ ∗ … = ψ globally
smooth (when F has compact d-support and is a parametrix).
Pseudolocal estimate (distributional convolution form). For any
parametrix F with compact d-support, the singular support of u is
contained in singsupp F + singsupp(P(D) u).
Subtracted-identity version of the pseudolocal estimate. Removing
the smooth remainder ψ = P(D)F - δ₀, the singular support of u - ψ
satisfies the same convolution bound.
Parametrix singular support bound. For a parametrix F with
compact d-support, singsupp u ⊆ singsupp F + singsupp(P(D) u).
Singular support bound for the remainder. Splitting u = v + w
with v globally smooth, the singular support of w is bounded by
singsupp F + singsupp(P(D) u).
Parametrix convolution identity assembled from the previous
lemmas: there is a smooth-plus-remainder decomposition u = v + w such
that singsupp w ⊆ singsupp F + singsupp(P(D) u).
Parametrix inversion (pointwise). If P(D) has a parametrix F
with singular support ⊆ {0}, then for any u and any point x, if
P(D) u is smooth near x, so is u.
Theorem 11.9 (Melrose), easy direction. If P(D) is hypoelliptic
then for any tempered distribution u, singsupp u ⊆ singsupp (P(D) u):
wherever P(D) u is smooth, so is u.
Theorem 11.9 (Melrose). For a hypoelliptic operator P(D),
singsupp u = singsupp (P(D) u). Combining the inclusion
singsupp (P(D) u) ⊆ singsupp u (always true) with the parametrix-based
reverse inclusion.
Inverse Fourier transform of a temperate-growth symbol exists as a
temperate-growth function F such that pairing Q with φ̌ equals pairing
F with φ. (Auxiliary input to the Plancherel argument.)
Auxiliary: any Cᵏ function that agrees with F away from a small
ball around 0 exists — in fact F itself is Cᵏ and the conclusion is
trivial in this formulation.
Plancherel/Sobolev step. For any k, there is a Cᵏ function g
representing the inverse Fourier transform of Q whenever paired with
Schwartz functions whose Fourier transform vanishes near the origin.
Plancherel / local Sobolev regularity. The Fourier multiplier
Q · δ₀ is represented, against Schwartz functions vanishing on a
neighbourhood of 0, by a Cᵏ function g.
Fundamental lemma of the calculus of variations (distributional
form). Two continuous functions agreeing distributionally against all
Schwartz test functions supported in an open set U agree pointwise on
U.
Whitney-type extension. A function smooth on an open set U
extends to a globally smooth function on ℝⁿ agreeing with the original
on U.
A distribution T represented by a Cᵏ function on U for every
k ∈ ℕ is in fact represented by a C^∞ function on U.
Local smoothness of Q · δ₀ away from 0. If Q has temperate
growth, then Q · δ₀ is represented by a smooth function on a small open
neighbourhood of any nonzero point x₀.
Elliptic parametrix is smooth away from the origin. If P is
elliptic and Q is a temperate-growth symbol, then the distribution
Q · δ₀ is smooth near every nonzero point — a key step in constructing
the parametrix used to prove ellipticity implies hypoellipticity.
Dominance of the principal symbol. For an elliptic polynomial P
of order m, there is a radius R past which the contribution of the
lower-order terms P - P_m to the Fourier symbol is dominated in norm by
the principal-symbol contribution.
Non-vanishing of the symbol at large frequencies. A corollary of
principal-symbol dominance: for an elliptic P there is R > 0 such that
P(2πiξ) ≠ 0 whenever ‖ξ‖ > R.
Existence of an elliptic parametrix cutoff function. For an
elliptic polynomial P, there is a smooth compactly-supported cutoff
φ : ℝⁿ → ℂ which equals 1 on a neighbourhood of the (compact) zero set
of the Fourier symbol of P. The function 1 - φ then vanishes near the
zeros of P̂ and allows us to invert P̂ everywhere modulo a smooth
remainder.
Smoothness of the Fourier symbol. The map
ξ ↦ P(2πiξ) : ℝⁿ → ℂ is C^∞.
Smoothness of the parametrix symbol at zeros of P̂. At a point
ξ₀ where the Fourier symbol of P vanishes (and where the cutoff φ
equals 1 on a neighbourhood), the regularised symbol
(1 - φ(ξ)) · P̂(ξ)⁻¹ is smooth — locally it is identically zero.
Uniform bound on derivatives of 1/P̂ at infinity. For an elliptic
polynomial P, every derivative of order k of the reciprocal symbol
ξ ↦ 1/P̂(ξ) is bounded uniformly on {‖ξ‖ > R} for some R > 0.
Polynomial bound on derivatives of the parametrix symbol. Each
iterated derivative of the regularised symbol
(1 - φ(ξ)) · P̂(ξ)⁻¹ is bounded by C · (1 + ‖ξ‖)^N for some N and
C, witnessing its temperate growth.
Temperate growth of the parametrix symbol. Combining smoothness
and the polynomial bound on derivatives, the regularised symbol
(1 - φ(ξ)) · P̂(ξ)⁻¹ has temperate growth — the property needed to apply
it as a Fourier multiplier to tempered distributions.
Parametrix symbol/cutoff data package for an elliptic operator.
Combines the existence of the cutoff φ, the regularised symbol
Q = (1 - φ) · P̂⁻¹, its temperate growth, and the fact that the
distribution Q(D) δ₀ is smooth at every nonzero point.
Temperate growth of the Fourier symbol. The polynomial symbol
ξ ↦ P(2πiξ) has temperate growth.
Compactly-supported multipliers give globally smooth distributions.
If the Fourier multiplier φ is smooth and compactly supported, then
φ(D) δ₀ = ℱ^{-1} φ is a Schwartz function, hence smooth near every
point.
Full parametrix symbol data for an elliptic operator. A polished
version of elliptic_parametrix_cutoff_data that also records the
temperate growth of the original Fourier symbol and the smoothness of both
distributions φ(D) δ₀ and Q(D) δ₀.
Q(D) δ₀ is a parametrix. Given symbol data (Q, φ) with
Q · P̂ = 1 - φ and φ(D) δ₀ smooth everywhere, the difference
P(D) (Q(D) δ₀) - δ₀ equals -φ(D) δ₀ and is therefore smooth near every
point. In particular Q(D) δ₀ is a parametrix for P(D).
Pointwise singular-support bound for an elliptic parametrix. Any
parametrix F for an elliptic operator P(D) is smooth at every nonzero
point. Proven by comparing F to the explicit Fourier-multiplier
parametrix F₀ = Q(D) δ₀ via parametrix_inversion_isSmoothNear.
Existence of a parametrix for an elliptic operator. Every elliptic
constant-coefficient P(D) admits a parametrix, constructed as
F = Q(D) δ₀ with the regularised symbol Q.
Singular-support bound for an elliptic parametrix. Every parametrix
F for an elliptic P(D) has singular support contained in {0}.
Existence of a parametrix with controlled singular support.
Combining existence and the singular-support bound: every elliptic P(D)
has a parametrix F whose singular support is contained in {0}. This is
exactly the hypothesis required by IsHypoelliptic.
Theorem 11.12 (Melrose). Every elliptic constant-coefficient
operator P(D) is hypoelliptic: it admits a parametrix with singular
support ⊆ {0}.
A smooth function vanishing at infinity (with all derivatives):
a smooth complex-valued function on ℝⁿ whose iterated derivatives of
every order tend to zero on the cocompact filter. Used as the target class
for Liouville-type uniqueness results for the Laplacian.
- toFun : EuclideanSpace ℝ (Fin n) → ℂ
- iteratedFDeriv_zero_at_infty' (m : ℕ) : Filter.Tendsto (fun (x : EuclideanSpace ℝ (Fin n)) => ‖iteratedFDeriv ℝ m self.toFun x‖) (Filter.cocompact (EuclideanSpace ℝ (Fin n))) (nhds 0)
Instances For
SmoothZeroAtInfty is coercible to a function via its underlying
toFun field, with the obvious injectivity.
Pointwise equality of SmoothZeroAtInfty functions implies equality.
Smoothness of the underlying function of a SmoothZeroAtInfty.
For every order m, the norm of the m-th iterated derivative of a
SmoothZeroAtInfty function tends to zero on the cocompact filter.
The Laplacian polynomial P(X) = Σⱼ Xⱼ², whose associated
constant-coefficient differential operator is the Laplacian
Δ = Σⱼ ∂ⱼ² (up to the usual (2πi)² factor coming from the Fourier
normalisation).
Instances For
The Laplacian as a continuous linear operator on tempered
distributions, defined via the constant-coefficient differential operator
machinery applied to laplacianPoly.
Instances For
Smoothness of polynomial evaluation. Evaluating a real multivariate
polynomial on the coordinates of ℝⁿ yields a C^∞ function.
Smoothness of 1/P(ξ) at non-vanishing points. Wherever the
polynomial P does not vanish, the function ξ ↦ 1/P(ξ) is C^∞.
Explicit derivative of 1/P(ξ). At any non-vanishing point, the
Fréchet derivative of ξ ↦ 1/P(ξ) equals -P(ξ)⁻² · dP(ξ).
Norm bound for the derivative of 1/P(ξ). Combining the explicit
formula with the multiplicativity of norms,
‖d(1/P)(ξ)‖ ≤ ‖dP(ξ)‖ / ‖P(ξ)‖².
Recursive identity for higher derivatives of 1/P. The norm of the
(k+1)-th iterated derivative of 1/P equals the norm of the k-th
iterated derivative of its first derivative.
Non-degeneracy of the Laplacian polynomial. For n ≥ 1,
Σⱼ Xⱼ² is nonzero in ℂ[X₀, …, X_{n-1}].
The classical Laplacian relation between smooth functions
f, g : ℝⁿ → ℂ: g(x) = -Σⱼ ∂_j² f(x) for every x. (The convention sign
comes from the Fourier multiplier -|2πξ|² of Δ.)
Instances For
Integration-by-parts formula for the Laplacian on a smooth
representative. If a tempered distribution u_td is represented by a
smooth function u vanishing at infinity (with all derivatives), then for
every Schwartz test function φ, applying the distributional Laplacian
equals the integral of φ against the classical Laplacian -Σⱼ ∂_j² u.
A continuous function is determined by its pairing with Schwartz
functions. If the classical Laplacian -Σⱼ ∂_j² u and a Schwartz
function f agree as integrands against every Schwartz φ, then they
agree pointwise.
Distributional Laplacian equals classical Laplacian (pointwise).
For smooth u vanishing at infinity (along with all derivatives) and
Schwartz f, if the distributional Laplacian of u equals f, then
f = -Σⱼ ∂_j² u pointwise.
Mean-value gradient bound for a harmonic function. For a smooth
harmonic function u : ℝⁿ → ℂ bounded in absolute value by C, the
Fréchet derivative at any point a satisfies the gradient estimate
‖du(a)‖ ≤ n · C / R for every R > 0.
Bounded harmonic functions have vanishing gradient. Letting R → ∞
in the gradient estimate forces du(x) = 0 at every point.
Liouville's theorem (smooth version). A bounded smooth harmonic
function on ℝⁿ is constant.
Uniqueness for the Poisson equation. Among smooth functions on
ℝⁿ (n ≥ 3) that vanish at infinity, the Laplacian determines the
function uniquely: if Δu₁ = Δu₂ = f then u₁ = u₂.
Uniqueness for Δ u = f with Schwartz right-hand side, among
distributional solutions represented by smooth functions vanishing at
infinity (i.e. in C₀^∞).
A tempered distribution u is smooth on the set s if there
is a globally smooth g : E → ℂ such that u φ = ∫ φ g for every
Schwartz function φ with tsupport φ ⊆ s.
Instances For
The singular support of u: complement of the union of all open
sets on which u is represented by a smooth function.
Instances For
A tempered distribution v has compact distributional support if
its dsupport is a compact subset of the underlying space.
Instances For
Continuity of translation on Schwartz space. The map
x ↦ ψ(· - x) from E to 𝓢(E, ℂ) is continuous.
The n-th iterated derivative of z ↦ fderiv f z h factors through
the application map T ↦ T h.
Norm bound: ‖∂ⁿ (z ↦ Df(z)·h)‖ ≤ ‖∂ⁿ⁺¹ f‖ · ‖h‖.
Taylor remainder estimate. For a C² map g, the first-order
Taylor remainder is O(‖h‖²) with constant given by a bound on the second
derivative.
Taylor remainder estimate in Schwartz seminorms. The
(k, n)-seminorm of the first-order Taylor remainder
ψ(· - h) - ψ + Dψ · h is O(‖h‖²), with the implicit constant a fixed
linear combination of (k, n+2)-seminorms of ψ.
Schwartz Taylor remainder is o(h). Pushing the Taylor remainder
through a continuous linear map L gives a o(h) quantity as h → 0,
which is what's needed to establish Fréchet differentiability of
x ↦ L (ψ(· - x)).
Inductive step for smoothness of x ↦ L(ψ(· - x)). Given that
the same conclusion holds at level n for every ψ, the function
x ↦ L(ψ(· - x)) has an n-times continuously differentiable derivative
at every point.
Smoothness of translation in Schwartz. For any continuous linear
map L : 𝓢(E, ℂ) →L[ℂ] F, the map x ↦ L(φ(· - x)) is C^∞ on E.
Smoothness of the distributional convolution v ∗ φ. For v a
tempered distribution with compact dsupport and φ Schwartz, the
function x ↦ v(φ(· - x)) is smooth.
A distribution with compact dsupport vanishes on the complement
of a compact set (namely K = dsupport v).
Multiplying a Schwartz function by a smooth compactly-supported real
cutoff χ produces another Schwartz function χ · f.
Instances For
Evaluation lemma for the cutoff product:
(cutoffMul χ … f) y = χ y • f y.
Function-level identity for the cutoff product:
⇑(cutoffMul χ … f) = fun y => χ y • f y.
Zero-weight Schwartz seminorms are translation-invariant. Since
(0, m)-seminorms involve no polynomial weight, the translated function
φ(· - x) has the same (0, m)-seminorm as φ.
Cutoff–translation seminorm bound. Bounded uniformly in the
translation parameter x, the (k, n)-Schwartz seminorm of the cutoff of
φ(· - x) is controlled by a fixed finite supremum of seminorms of φ.
Schwartz seminorm bound for v ∗ φ. For v with compact
distributional support, the (k, n)-Schwartz seminorm of the convolution
x ↦ v(φ(· - x)) is bounded by a fixed sup of seminorms of φ.
Rapid decay of v ∗ φ. For v with compact dsupport, all
iterated derivatives of x ↦ v(φ(· - x)) decay faster than any
polynomial. Stated with weight (1 + ‖x‖)^N.
Schwartz decay of v ∗ φ. For v with compact dsupport, the
function x ↦ v(φ(· - x)) satisfies the Schwartz decay bounds
‖x‖^k · ‖∂ⁿ …‖ ≤ C.
The convolution of a compactly-dsupport-ed tempered distribution
v with a Schwartz function φ, viewed itself as a Schwartz function:
(v ∗ φ)(x) := v(φ(· - x)).
Instances For
Evaluation lemma: (v ∗ φ)(x) = v(φ(· - x)).
The convolution (v ∗ ·) is additive in the Schwartz argument.
The convolution (v ∗ ·) is ℂ-linear in the Schwartz argument.
The convolution φ ↦ v ∗ φ is a continuous map
𝓢(E, ℂ) → 𝓢(E, ℂ), established via boundedness of seminorms.
Convolution with a compactly-dsupport-ed distribution is a CLM.
For any such v, there exists a continuous linear self-map T on
𝓢(E, ℂ) with (T φ) x = v(φ(· - x)).
Polynomial growth bound. The evaluation of a multivariate
polynomial Q of total degree d at points of ℝⁿ is bounded by a
constant times (1 + ‖ξ‖)^d.
A smooth function with compact support automatically belongs to the Schwartz class; this packages the conversion.
Existence of a parametrix cutoff. For an elliptic polynomial P,
there is a smooth compactly-supported function φ equal to 1 exactly on
the (compact) zero set of the symbol polySymbol n P.
Parametrix symbol has temperate growth. The symbol
(1 - φ(ξ)) · P(2πiξ)⁻¹, with φ a parametrix cutoff and P elliptic,
has temperate growth and is smooth — hence valid as a Fourier multiplier
symbol.
Existence of a parametrix symbol for an elliptic operator. For
elliptic P, there is a temperate-growth symbol Q and a Schwartz
function ψ with P(2πiξ) · Q(ξ) = 1 - ψ(ξ). This is the symbolic
identity behind P(D) ∘ Q(D) = Id - smoothing.