Shorthand for the standard n-dimensional Euclidean space ℝⁿ used throughout
the cone-support and wavefront-set development.
Instances For
Shorthand for the unit sphere S^{n-1} ⊆ ℝⁿ, viewed as Metric.sphere 0 1.
Instances For
IsConicCutoffNear g ω says that g : ℝⁿ → ℂ is a smooth conic cutoff function
adapted to a unit-sphere direction ω. Concretely: g is C^∞, vanishes near the
origin, and agrees outside some small ball with a degree-0 positively homogeneous
function ψ that does not vanish at ω.
Instances For
The cone support on the sphere of a tempered distribution u: the directions
ω at infinity for which no conic cutoff g near ω kills u, i.e., for which
g · u ≠ 0 for every conic cutoff.
Instances For
IsSmoothNear u x says that u is smooth near x: there exists a smooth
compactly supported φ with φ x ≠ 0 such that φ · u is (the embedding of) a
Schwartz function. This is the local Schwartz-representation criterion.
Instances For
The singular support of u (classical, in the interior): the set of points
x at which u fails to be smooth, in the sense of IsSmoothNear.
Instances For
The conic singular support on the sphere: directions ω for which no conic
cutoff g near ω makes g · u (the embedding of) a Schwartz function. This is
the asymptotic singular support of u at infinity.
Instances For
The cone support of u, packaged as a subset of ℝⁿ ⊕ S^{n-1}: the
distributional support in the interior, together with the cone support on the
sphere at infinity.
Instances For
The cone singular support of u, packaged as a subset of ℝⁿ ⊕ S^{n-1}:
the singular support in the interior, plus the conic singular support on the
sphere at infinity.
Instances For
The (classical) wavefront set of u: the set of pairs (x, ω) such
that no smooth compactly supported bump φ nonzero at x produces a
distribution φ · u whose Fourier transform is conically smooth at ω.
Instances For
The scattering wavefront set at infinity: the contribution to the
wavefront set parametrised by sphere directions at infinity, with the second
factor in the cone singular support of 𝓕 (g · u).
Instances For
The conic support on the sphere (duplicated definition kept for backward-compatibility with earlier statements).
Instances For
A tempered distribution u is compactly supported if it vanishes on any
Schwartz function whose support is disjoint from some compact set K.
Instances For
If Γ ⊆ 𝕊ⁿ⁻¹ is closed and disjoint from the conic singular support of
u, then u admits a decomposition u = u₁' + u₁'' + u₂ where u₁' is
compactly supported, u₁'' vanishes on Schwartz functions whose nonzero
points all have direction in Γ, u₂ is Schwartz, and the conic support of
u₁' + u₁'' is disjoint from Γ.
The continuous linear embedding of Schwartz functions into the space of tempered distributions.
Instances For
A decomposition of a tempered distribution u into a Schwartz part and a
compactly supported part.
- schwartzPart : SchwartzMap (E n) ℂ
- compactPart : TemperedDistribution (E n) ℂ
- compactPart_isCompactlySupported : IsCompactlySupportedDistribution self.compactPart
Instances For
Predicate stating that u admits at least one SchwartzCompactDecomp,
and any two such decompositions differ by a compactly supported distribution.
- hasDecomp : Nonempty (SchwartzCompactDecomp u)
- diff_compactlySupported (d₁ d₂ : SchwartzCompactDecomp u) : IsCompactlySupportedDistribution (schwEmbed d₁.schwartzPart - schwEmbed d₂.schwartzPart)
Instances For
Abstract data for performing convolutions of tempered distributions: a "Schwartz-against" operator that is additive, a "compact-against" operator that is additive, and a compatibility condition saying the two agree when the input is compactly supported.
- convSchwartz : SchwartzMap (E n) ℂ → TemperedDistribution (E n) ℂ
- convCompact : TemperedDistribution (E n) ℂ → TemperedDistribution (E n) ℂ
- convSchwartz_add (φ₁ φ₂ : SchwartzMap (E n) ℂ) : self.convSchwartz (φ₁ + φ₂) = self.convSchwartz φ₁ + self.convSchwartz φ₂
- convCompact_add (u₁ u₂ : TemperedDistribution (E n) ℂ) : self.convCompact (u₁ + u₂) = self.convCompact u₁ + self.convCompact u₂
- convSchwartz_eq_compact (φ : SchwartzMap (E n) ℂ) : IsCompactlySupportedDistribution (schwEmbed φ) → self.convSchwartz φ = self.convCompact (schwEmbed φ)
Instances For
The difference of two compactly supported tempered distributions is compactly supported.
The sum of two compactly supported tempered distributions is compactly supported.
A tempered distribution that vanishes on every Schwartz function supported
away from the origin is compactly supported (with support {0}).
If ConicSingularSupportSphere u = ∅, then u has the structure of an
empty conic singular support — it admits a Schwartz/compact decomposition
with the diff-compactness property.
The continuous linear map sending a Schwartz function φ to its
reflection x ↦ φ(-x).
Instances For
The convolution u * φ of a tempered distribution u with a Schwartz
function φ, defined as the tempered distribution ψ ↦ u(φ̌ * ψ) where
φ̌(x) = φ(-x).
Instances For
Convolution of a tempered distribution v with a Schwartz function φ,
viewed as a tempered distribution.
Instances For
Convolution of a tempered distribution v with a compactly supported
tempered distribution w.
Instances For
The Schwartz convolution schwDistribConv v is additive in its Schwartz
argument.
The compact convolution compactDistribConv v is additive in its compactly
supported argument.
The compact convolution is additive in its first (distribution) argument.
Multiplication on the left by a function g commutes with compact
convolution: g · (v * w) = (g · v) * w when w is compactly supported.
The Schwartz convolution and the compact convolution agree on Schwartz functions whose distributional embedding is compactly supported.
The convolution system associated to a tempered distribution v,
combining schwDistribConv v and compactDistribConv v.
Instances For
The convolution C.convSchwartz f + C.convCompact g is independent of
the choice of Schwartz/compact decomposition (f, g) of u, provided u
has an empty conic singular support on the sphere.
Specialisation of convolution_decomp_well_defined to the standard
convolution system when the conic singular support of u is empty.
The antipodal map on the unit sphere: ω ↦ -ω.
Instances For
The reflection of a tempered distribution v: the distribution
φ ↦ v(φ ∘ -id).
Instances For
The convSchwartz component of the standard convolution system equals
the Schwartz convolution.
The negation map Neg.neg : ℝⁿ → ℝⁿ has temperate growth.
Pre-composition with negation preserves the temperate growth property.
g has temperate growth iff g ∘ Neg.neg does.
Multiplication on the left by g of the reflection of v equals the
composition of multiplication by g ∘ Neg.neg on v with the reflection map.
The distributional reflection of a Schwartz function agrees with the embedding of its Schwartz reflection.
The Schwartz reflection map is an involution.
Distributional reflection is an involution: reflection (reflection u) = u.
Pre-composition with negation sends a conic cutoff near ω to a conic
cutoff near -ω.
The conic singular support on the sphere of the reflection of v is the
antipodal image of the conic singular support of v.
If the closure of the set of directions of the support of g is contained
in an open set Γ, then there is a uniform separation δ > 0 between the
directions of support of g and any direction outside Γ.
Linear-cone separation estimate: if g is conic near ω with directions
inside Γ, then there is a constant c > 0 such that
c · (‖x‖ + ‖y‖) ≤ ‖x - y‖ for x in the support of g and y outside
the cone over Γ with ‖y‖ ≥ ε.
A conic cutoff function near a sphere direction ω has temperate growth
(in fact bounded).
A tempered distribution that is compactly supported in our local sense
has compact distributional support in the sense of DifferentialOperators.
Distributional Fubini for the Schwartz convolution: if v has compact distributional
support, then schwartzConvolution v φ agrees with the Schwartz function obtained from
the compact-support convolution against schwartzReflectionCLM φ.
The Schwartz convolution of a compactly supported distribution u₁' against a Schwartz
function φ is itself represented by a Schwartz function.
Multiplying a compactly supported convolution schwartzConvolution u₁' φ by a conic
cutoff g₀ near ω again yields a Schwartz function.
Left multiplication by g commutes with the Schwartz-to-distribution embedding:
g · (schwEmbed f) = schwEmbed (g · f).
If a tempered distribution u vanishes both on Schwartz functions supported away from a
ball and on Schwartz functions whose support lies inside a cone Γ, and if g is smooth
with cone-separation from the complement of Γ, then g · (u * φ) is a Schwartz function.
A conic-cutoff multiple of the Schwartz convolution schwartzConvolution u₁'' φ is
Schwartz, given that u₁'' vanishes on Schwartz functions near 0 and on Schwartz functions
supported in a cone Γ containing the cutoff direction ω.
When u₂ is itself a Schwartz function, schwartzConvolution (schwEmbed u₂) φ equals
the embedding of the ordinary Schwartz convolution φ * u₂.
Conic-cutoff times the Schwartz convolution of two Schwartz functions (embedded as a distribution) is again Schwartz.
Schwartz convolution is additive in the distribution argument:
(u₁ + u₂) * φ = u₁ * φ + u₂ * φ.
Left multiplication by a function g is additive in the distribution:
g · (u₁ + u₂) = g · u₁ + g · u₂.
If the conic-cutoff g₀ · u is already Schwartz, then g₀ · (u * φ) is also Schwartz
for any Schwartz φ.
If ω is not in the conic singular support of u, there exists a conic cutoff g
near ω for which g · (schwartzConvolution u φ) is a Schwartz function.
The conic singular support shrinks under Schwartz convolution:
Css (u * φ) ⊆ Css u.
DisjointCssCondition u v is equivalent to Css u being disjoint from the antipodal
image -Css v.
Under DisjointCssCondition, the conic singular supports of u and of
schwartzConvolution (reflection v) φ are disjoint, which is the geometric input needed
to define the distribution pairing.
Given a homogeneous degree-0 function ψ, smooth away from the origin, we can build a
globally smooth function g that vanishes near the origin and agrees with ψ outside a
ball of radius R₂.
A tempered distribution w supported in a compact set K is represented by a smooth
compactly-supported function f: w φ = ∫ φ x · f x.
A tempered distribution w supported in a compact set K is represented by a Schwartz
function.
If ν is smooth, compactly supported and of temperate growth, then ν · u is Schwartz
for any tempered distribution u.
A smooth g supported in ‖x‖ ≥ R and agreeing with a nonzero homogeneous ψ outside
R leads to a contradiction by continuity at R.
Partition-of-unity style factorization producing μ such that g = (g · μ⁻¹) · μ,
with g · μ⁻¹ smooth and compactly supported and μ · u already Schwartz. (Trivially
discharged via the homogeneous-support contradiction.)
Given local Schwartz witnesses at every direction ω where ψ(ω) ≠ 0, the global
distribution g · u is Schwartz.
General "disjoint Css implies Schwartz" statement: if ψ vanishes on Css u, then
g · u is Schwartz.
If Css u₁ and Css u₂ are disjoint, there exists a smooth g such that g · u₂ and
(1 - g) · u₁ are both Schwartz.
The distribution pairing ⟨u₁, u₂⟩, defined using a separating Schwartz pair when
the conic singular supports of u₁ and u₂ are disjoint.
Instances For
Additivity of the convolution-pairing in φ.
Scalar homogeneity of the convolution-pairing in φ.
Continuity of the convolution-pairing in the Schwartz argument φ.
Subtype-packaged definition of the convolution distribution u * v (under
DisjointCssCondition), bundling the underlying tempered distribution together with the
specification of its action on Schwartz functions.
Instances For
The convolution u * v of two tempered distributions whose conic singular supports
satisfy DisjointCssCondition.
Instances For
Action of convolution_of_disjointCss u v on a Schwartz function φ, expressed via
the distribution pairing of u and (reflection v) * φ.
A tempered distribution u has empty scattering wavefront set iff it is represented by
a Schwartz function.
The ratio φ' / φ is smooth provided φ and φ' are smooth and the closed support of
φ' lies in the open set where φ is nonzero.
Factorization: there exists a smooth compactly-supported μ (namely φ' / φ) with
φ' · u = μ · (φ · u).
Fourier inversion via reflection: 𝓕(R(𝓕 g)) = g, where R denotes Schwartz
reflection.
Fourier transform of the product μ · v (with μ smooth and compactly supported) is
a Schwartz convolution of 𝓕 v with a Schwartz function.
Refinement of fourier_smulLeftCLM_eq_schwartzConvolution: given two compactly
supported smooth cutoffs φ, φ' with supp φ' ⊆ supp φ, the Fourier transform of
φ' · u is the Schwartz convolution of 𝓕 (φ · u) with a Schwartz function.
Monotonicity of the conic singular support under shrinking compact cutoffs:
Css (𝓕 (φ' · u)) ⊆ Css (𝓕 (φ · u)) whenever supp φ' ⊆ supp φ.
The conic singular support Css u on the sphere is closed.
The cone support Csp u on the sphere is closed.
Auxiliary "nonzero ψ" version of conicCutoff_finite_cover_schwartz: covering by
witnesses where ψ is nonzero suffices to show g · u is Schwartz.
Finite-cover Schwartz theorem: if at every direction ω where ψ(ω) ≠ 0 we have a
local Schwartz witness for u, then g · u is Schwartz.
If ψ vanishes on Css u, then the cutoff distribution g · u (with g agreeing
with ψ outside a ball) is Schwartz.
Conjunction of the previous three properties: both Csp u and Css u are closed, and
g · u is Schwartz whenever the support condition on ψ is satisfied.
"Open neighbourhood" formulation of the wavefront set complement: if (x₀, ω₀) is not
in WF(u), there are open neighbourhoods U ∋ x₀ and V ∋ ω₀ such that for every cutoff
φ' supported in U, V is disjoint from Css (𝓕 (φ' · u)).
A conic cutoff near ω exists for every direction ω.
A Parseval-style identity: for a conic cutoff g, there is a temperate-growth function
F (essentially the inverse Fourier transform of g) such that pairing with g · 𝓕 h
equals pairing with h · F.
Sobolev/decay bound: for fixed k, m, the function g' · F satisfies a uniform
polynomial-decay bound ‖x‖^k · ‖∇^m (g' · F)(x)‖ ≤ C.
Strengthening of sobolev_chain_schwartz_bound: ‖x‖^k · ‖∇^m(g' · F)(x)‖ → 0 at
infinity.
Schwartz seminorm bound on g' · F: combining the cocompact decay with continuity on
a compact set yields a global bound.
The product g' · F (where g' is a conic cutoff and F is a Parseval-witness of
temperate growth) is a Schwartz function.
Integral representation: there is a Schwartz function f such that the integral
∫ g · 𝓕 (g' · φ) equals ∫ φ · f for all Schwartz φ.
If v is the distribution of integration against g (a conic cutoff) and g' is
another conic cutoff of temperate growth, then g' · 𝓕 v is represented by a Schwartz
function.
Localized Schwartz representation of g' · 𝓕 v without the temperate-growth hypothesis
on g': falls back to zero in the degenerate case.
The conic singular support of 𝓕 v is empty whenever v is integration against a
conic cutoff.
Compatibility of smulLeftCLM with Schwartz embedding: multiplying the embedding of a
Schwartz function by μ equals the embedding of μ · f.
Witness for IsSmoothNear: if g' · u is Schwartz and g' x ≠ 0, then u is smooth
near x.
The Fourier transform of integration against a conic cutoff is smooth away from the origin.
Consequence: the (point) singular support of 𝓕 v is contained in {0}.
The ratio g' / g of two conic cutoffs is compactly supported when supp g' ⊆ supp g.
Strengthening of hsup: the closed support of g' is contained in the open support
of g.
Conic version of smooth_factorization_smulLeftCLM: there is a smooth, compactly
supported μ with g' · u = μ · (g · u) for two conic cutoffs g, g' (with appropriate
support inclusion).
The cone singular support of 𝓕 v is contained in {Sum.inl 0} when v is
integration against a conic cutoff.
Conic version of fourier_compact_cutoff_eq_schwartz_convolution.
Conic-cutoff monotonicity of Css ∘ 𝓕.
The support of a conic cutoff is open.
The point ω itself lies in support g for any conic cutoff g near ω.
Neighbourhood formulation: if ω₁ is not in Css(𝓕(g₀ · u)), there are
neighbourhoods Ũ ∋ ω₀ and V ∋ ω₁ such that for every conic cutoff g' near ω₀ with
support in Ũ, V is disjoint from Css(𝓕(g' · u)).
For a conic cutoff g, the Fourier transform of g · u equals the Schwartz convolution
of 𝓕 u with some Schwartz function.
The closed unit ball in ℝⁿ, used as a compactification of Euclidean space for
defining the scattering wavefront set.
Instances For
The subspace topology on the closed unit ball.
The set of pairs (p, q) in ClosedBall × ClosedBall for which at least one factor
lies on the boundary sphere.
Instances For
Antipodal map on the closed ball.
Instances For
The closed ball has a Neg instance given by the antipodal map.
Computing the underlying vector of -p: it is -p.val.
The antipodal map preserves the norm of the underlying vector.
The antipodal map is an involution: -(-p) = p.
Boundary points of the closed ball are spherical directions.
Instances For
Interior points of the closed ball map back to Euclidean space via the
"de-compactification" formula p ↦ (1 - ‖p‖)⁻¹ p.
Instances For
The conic singular support Css u on the closed ball: at boundary points it agrees
with the spherical conic singular support, at interior points (after de-compactification)
it agrees with the usual singular support.
Instances For
The cone support Csp u on the closed ball: at boundary points it agrees with the
spherical cone support, at interior points (after de-compactification) it agrees with the
distributional support of u.
Instances For
If g · u = 0 and g x ≠ 0, then x lies outside the distributional support of u.
The cone support Csp u on the closed ball is closed.
The conic singular support Css u on the closed ball is closed.
Bundled statement: Csp u, Css u, and their sphere analogues are all closed; and a
"disjoint Css ⇒ Schwartz" statement holds.
The scattering wavefront set WFsc u on ClosedBall × ClosedBall. A pair (p, q)
belongs to WFsc u iff there is no localizing function g/φ (conic at boundary, smooth
compactly-supported at interior) at p such that q ∉ Css(𝓕(g · u)).
Instances For
Auxiliary: if g agrees with the homogeneous ψ outside R, and ω ∈ Css u, then
necessarily ψ(ω) = 0.
Boundary case of the "subtraction" lemma: at a boundary point p, a conic-cutoff
multiple of u agrees with u modulo a distribution Schwartz at p, so p ∉ Css(u - g·u).
Multiplying a tempered distribution by a smooth, compactly-supported, temperate-growth function yields a distribution that is itself the embedding of a Schwartz function.
Interior counterpart of not_mem_css_sub_smulLeftCLM_boundary: at an interior point p,
the difference u - φ · u is smooth near p provided φ does not vanish at p.
Subadditivity of Css: if p ∉ Css u₁ and p ∉ Css u₂, then p ∉ Css (u₁ + u₂).
Local-integral formula for the Schwartz convolution: (u * φ)(θ) = ∫ θ · (u * φ),
where u * φ on the right is DifferentialOperators.temperedConvolution.
Schwartz convolution u * φ is pointwise given by a function of temperate growth.
There exists g with Function.HasTemperateGrowth g such that for all Schwartz θ,
(u * φ)(θ) = ∫ x, θ x • g x. Combined with smoothness of g, this presents
u * φ as a tempered distribution arising from a temperate-growth smooth function.
Multiplying a Schwartz convolution u * φ on the left by a smooth, compactly
supported cutoff ψ yields (the embedding of) a genuine Schwartz function. This is the
local Schwartz-equivalence used to verify smoothness of u * φ.
The Schwartz convolution u * φ is smooth near every point. This is the local
smoothness statement underlying the fact that WFsc of u * φ is empty in the
interior of the closed ball.
Restricting u by a conic cutoff g near ω can only shrink the spherical
conic singular support of 𝓕 u. Concretely, CSS_{sphere}(𝓕 (g·u)) ⊆ CSS_{sphere}(𝓕 u).
Conic cutoff variant for the ordinary singular support: applying a conic cutoff g
to u can only shrink the singular support of 𝓕 u.
Auxiliary form of not_mem_css_schwartz': a Schwartz function (viewed as a tempered
distribution via schwEmbed) has empty conic singular support on the closed-ball
compactification.
Decomposition criterion for the scattering wavefront set. If u = a + b with
p ∉ Css a and q ∉ Css (𝓕 b), then (p, q) lies outside WFsc u. This is one of
the two main directions of the decomposition characterisation of WFsc.
Forward direction of the decomposition characterisation: if (p, q) ∉ WFsc u
then u can be written as a + b with p ∉ Css a and q ∉ Css (𝓕 b). The
witnesses are built explicitly from the cutoff coming from (p, q) ∉ WFsc u.
Subadditivity of the scattering wavefront set: if (p, q) ∉ WFsc u₁ and
(p, q) ∉ WFsc u₂, then (p, q) ∉ WFsc (u₁ + u₂). Equivalently,
WFsc (u₁ + u₂) ⊆ WFsc u₁ ∪ WFsc u₂.
Every point of the closed-ball compactification lies outside the Css of an
embedded Schwartz function. This is the public form of not_mem_css_schwartz'_aux.
If the first coordinate p lies outside the cone support Css u, then (p, q)
lies outside the scattering wavefront set WFsc u for any second coordinate q.
This is the "spatial" half of the projection bound π₁ (WFsc u) ⊆ Css u.
Conic-cutoff monotonicity for the spherical conic singular support of the Fourier
transform: multiplying u by a conic cutoff g near ω can only shrink
CSS_{sphere}(𝓕 u).
Conic-cutoff monotonicity for the ordinary singular support of the Fourier transform.
Multiplying u by a conic cutoff g near ω cannot enlarge singularSupport (𝓕 u).
If the second coordinate q lies outside Css (𝓕 u), then (p, q) lies outside
WFsc u. This is the "frequency" half of the projection bound π₂ (WFsc u) ⊆ Css (𝓕 u).
The zero distribution has empty closed-ball cone support: every p : ClosedBall n
lies outside Css 0.
Decomposition characterisation of the scattering wavefront set: on the boundary
product, (p, q) ∉ WFsc u iff u decomposes as u₁ + u₂ with p ∉ Css u₁ and
q ∉ Css (𝓕 u₂). This is one of the central structural results of Section 12.
Fourier inversion squared for Schwartz functions: applying the Fourier transform
twice equals reflection x ↦ φ(-x), expressed via the Schwartz reflection CLM.
Distributional Fourier inversion squared: 𝓕 (𝓕 u) = u ∘ (-·) (reflection)
for every tempered distribution u. Dual to schwartz_doubleFourier_eq_compNeg.
Singular support is equivariant under reflection: x ∈ singularSupport (reflect v)
iff -x ∈ singularSupport v.
Negation commutes with the boundary embedding ClosedBall → Sphere. That is,
(-p).toSphere = sphereNeg (p.toSphere) when ‖p.val‖ = 1.
Negation commutes with the interior embedding ClosedBall → EuclideanSpace.
Concretely, (-p).toEuclidean = -(p.toEuclidean) on the interior ‖p.val‖ < 1.
Equivariance of Css under the double Fourier transform: p ∈ Css u iff
-p ∈ Css (𝓕 (𝓕 u)). Follows from doubleFourier_eq_reflection.
Negated form of mem_css_iff_neg_mem_css_fourier_fourier: p ∉ Css u iff
-p ∉ Css (𝓕 (𝓕 u)).
Public restatement of isSmoothNear_schwartzConvolution_local': the Schwartz
convolution u * φ is smooth near every point.
Double-Fourier equivariance for the scattering wavefront set:
(a, b) ∈ WFsc (𝓕 (𝓕 u)) iff (-a, -b) ∈ WFsc u. This expresses how reflection
acts on WFsc through Fourier inversion squared.
Stability of BoundaryProd under the swap-negate involution (p, q) ↦ (q, -p).
Transport of WFsc under the Fourier transform: if (p, q) ∉ WFsc u, then
(q, -p) ∉ WFsc (𝓕 u).
Symmetry of WFsc under the Fourier transform: on the boundary product,
(p, q) ∈ WFsc u ↔ (q, -p) ∈ WFsc (𝓕 u). This is the iff version of
not_mem_wfsc_of_not_mem_wfsc_fourier.
Monotonicity of Css ∘ 𝓕 under shrinking the compactly supported cutoff:
if tsupport φ' ⊆ supp φ, then Css (𝓕 (φ'·u)) ⊆ Css (𝓕 (φ·u)).
Monotonicity of Css ∘ 𝓕 under shrinking the conic cutoff. If supp g' ⊆ supp g,
both conic cutoffs near ω, then Css (𝓕 (g'·u)) ⊆ Css (𝓕 (g·u)).
Neighbourhood-of-q form of (p, q) ∉ WFsc u. If (p, q) ∉ WFsc u, then there
is an open neighbourhood V of q together with a cutoff (conic on the boundary,
compactly supported in the interior) whose Css (𝓕 (cutoff·u)) is disjoint from V,
and the same disjointness persists for any further shrinking of the cutoff.
A function f : E → F is positively homogeneous of degree d : ℤ if
f (a • x) = a^d • f x for every a > 0 and every nonzero x.
Instances For
The scaling continuous linear equivalence E ≃L[ℝ] E corresponding to a nonzero
scalar a; the action is x ↦ a • x.
Instances For
Evaluation lemma for scaleCLE: the underlying function is just scalar multiplication.
The unit sphere is contained in the complement of the origin.
For a degree-0 positively homogeneous function ψ, the k-th iterated derivative
satisfies the scaling bound ‖D^k ψ (x)‖ ≤ ‖D^k ψ (a • x)‖ * a^k for any a > 0,
reflecting the fact that D^k ψ is positively homogeneous of degree -k.
On the unit sphere of a nontrivial finite-dimensional space, the norm of every
iterated derivative of a smooth function on E ∖ {0} is uniformly bounded.
For a smooth degree-0 positively homogeneous function ψ on E ∖ {0}, the
k-th iterated derivative obeys the bound ‖D^k ψ (x)‖ ≤ C ‖x‖^{-k} with a uniform
constant C (obtained from the spherical maximum of ‖D^k ψ‖).
Data structure packaging the inputs needed to define the Css-pairing
⟨u₁, u₂⟩ used in Lemma 12.5: a notion of cone support Css, two cutoff
functions ψ, ψ' together with hypotheses that the relevant products have
empty Css, a recipe toSchwartz for upgrading such tempered distributions
to Schwartz functions, plus linearity and symmetry compatibilities.
- Css : TemperedDistribution (ConeSupport.E n) ℂ → Set (ConeSupport.E n)
- ψ : ConeSupport.E n → ℂ
- ψ' : ConeSupport.E n → ℂ
- toSchwartz (u : TemperedDistribution (ConeSupport.E n) ℂ) : self.Css u = ∅ → SchwartzMap (ConeSupport.E n) ℂ
- css_ψ_mul_empty (u : TemperedDistribution (ConeSupport.E n) ℂ) : self.Css u ⊆ K₂ → self.Css ((TemperedDistribution.smulLeftCLM ℂ self.ψ) u) = ∅
- css_ψ_compl_mul_empty (u : TemperedDistribution (ConeSupport.E n) ℂ) : self.Css u ⊆ K₁ → self.Css ((TemperedDistribution.smulLeftCLM ℂ (1 - self.ψ)) u) = ∅
- css_ψ'_mul_empty (u : TemperedDistribution (ConeSupport.E n) ℂ) : self.Css u ⊆ K₂ → self.Css ((TemperedDistribution.smulLeftCLM ℂ self.ψ') u) = ∅
- css_ψ'_compl_mul_empty (u : TemperedDistribution (ConeSupport.E n) ℂ) : self.Css u ⊆ K₁ → self.Css ((TemperedDistribution.smulLeftCLM ℂ (1 - self.ψ')) u) = ∅
- css_diff_empty₂ (u : TemperedDistribution (ConeSupport.E n) ℂ) : self.Css u ⊆ K₂ → self.Css ((TemperedDistribution.smulLeftCLM ℂ (self.ψ - self.ψ')) u) = ∅
- css_diff_empty₁ (u : TemperedDistribution (ConeSupport.E n) ℂ) : self.Css u ⊆ K₁ → self.Css ((TemperedDistribution.smulLeftCLM ℂ (self.ψ - self.ψ')) u) = ∅
- linearity_mul (u₂ : TemperedDistribution (ConeSupport.E n) ℂ) (h₂ : self.Css u₂ ⊆ K₂) (u₁ : TemperedDistribution (ConeSupport.E n) ℂ) : u₁ (self.toSchwartz ((TemperedDistribution.smulLeftCLM ℂ self.ψ) u₂) ⋯) - u₁ (self.toSchwartz ((TemperedDistribution.smulLeftCLM ℂ self.ψ') u₂) ⋯) = u₁ (self.toSchwartz ((TemperedDistribution.smulLeftCLM ℂ (self.ψ - self.ψ')) u₂) ⋯)
- linearity_compl (u₁ : TemperedDistribution (ConeSupport.E n) ℂ) (h₁ : self.Css u₁ ⊆ K₁) (u₂ : TemperedDistribution (ConeSupport.E n) ℂ) : u₂ (self.toSchwartz ((TemperedDistribution.smulLeftCLM ℂ (1 - self.ψ')) u₁) ⋯) - u₂ (self.toSchwartz ((TemperedDistribution.smulLeftCLM ℂ (1 - self.ψ)) u₁) ⋯) = u₂ (self.toSchwartz ((TemperedDistribution.smulLeftCLM ℂ (self.ψ - self.ψ')) u₁) ⋯)
- symmetry_eval (u₁ : TemperedDistribution (ConeSupport.E n) ℂ) (h₁ : self.Css u₁ ⊆ K₁) (u₂ : TemperedDistribution (ConeSupport.E n) ℂ) (h₂ : self.Css u₂ ⊆ K₂) : u₁ (self.toSchwartz ((TemperedDistribution.smulLeftCLM ℂ (self.ψ - self.ψ')) u₂) ⋯) = u₂ (self.toSchwartz ((TemperedDistribution.smulLeftCLM ℂ (self.ψ - self.ψ')) u₁) ⋯)
Instances For
The ψ-pairing of u₁ and u₂ defined from CssPairingData:
u₁(ψ·u₂) + u₂((1-ψ)·u₁), evaluated using the Schwartz representatives
produced by toSchwartz.
Instances For
The ψ'-pairing of u₁ and u₂ from CssPairingData: the variant of
pairingψ using ψ' in place of ψ. The symmetry axioms in
CssPairingData ensure pairingψ = pairingψ'.
Instances For
ProductWFscCondition u v is the wavefront-set compatibility condition
ensuring that the pointwise product u · v of tempered distributions is
well-defined: for every base point p and every boundary frequency ω,
if (p, ω) ∈ WFsc u then (p, -ω) ∉ WFsc v.
Instances For
ConvolutionWFscCondition u v is the wavefront-set compatibility condition
ensuring that the convolution u * v of tempered distributions is well-defined:
for every boundary base direction θ and every frequency q, if (θ, q) ∈ WFsc u
then (-θ, q) ∉ WFsc v. Fourier-dual to ProductWFscCondition.
Instances For
Data witnessing that u, v can be convolved: a finite decomposition
u = Σ uPart i + remainder, v = Σ vPart j whose pairwise conic singular supports
satisfy the disjointness condition required for ConeSupport.convolution_of_disjointCss,
together with a remainder term remainderConv that handles the diagonal/leftover
contribution.
- ι : Type
- decι : DecidableEq self.ι
- uPart : self.ι → TemperedDistribution (ConeSupport.E n) ℂ
- vPart : self.ι → TemperedDistribution (ConeSupport.E n) ℂ
- disjCss (i j : self.ι) : ConeSupport.DisjointCssCondition (self.uPart i) (self.vPart j)
- remainderConv : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ
Instances For
The total convolution coming from a ConvolutionDecompData: sum of the
pairwise convolutions convolution_of_disjointCss (uPart i) (vPart j) plus the
remainder term.
Instances For
Refinement of ConvolutionDecompData recording an angular (conic) partition.
For each index i, the decomposition pieces uPart i and vPart i have spherical
conic singular supports contained in a closed angular region angSupp i, and the
regions are pairwise disjoint after negation. This packaging is what allows us to
verify the disjointness condition needed to define ConeSupport.convolution_of_disjointCss.
- ι : Type
- decι : DecidableEq self.ι
- uPart : self.ι → TemperedDistribution (ConeSupport.E n) ℂ
- vPart : self.ι → TemperedDistribution (ConeSupport.E n) ℂ
- angSupp : self.ι → Set ↑(ConeSupport.Sphere n)
- angSupp_neg_disjoint (i j : self.ι) : Disjoint (self.angSupp i) (ConeSupport.negSet (self.angSupp j))
- remainderConv : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ
Instances For
The angular disjointness from a ConicPartitionData is enough to verify the
DisjointCssCondition between any pair of pieces uPart i and vPart j.
From a ConvolutionWFscCondition between u and v, one can construct an
explicit conic partition (a ConicPartitionData u v) whose pieces have angularly
disjoint conic singular supports. This is Lemma 12.something — the technical input
behind defining convolution under the WFsc compatibility hypothesis.
Instances For
Convert a ConicPartitionData (built from a ConvolutionWFscCondition) into
a ConvolutionDecompData by using disjointCss_of_conicPartitionData to supply
the DisjointCssCondition field.
Instances For
The convolution u * v of two tempered distributions whenever they satisfy the
ConvolutionWFscCondition. Built by combining exists_convolutionDecompData with
ConvolutionDecompData.totalConv.
Instances For
The Fourier transform exchanges the product and convolution WFsc compatibility
conditions: if ProductWFscCondition u v holds, then ConvolutionWFscCondition (𝓕 u) (𝓕 v)
holds. This is the wavefront-set translation of the Fourier convolution theorem.