If the conic singular support set Css u of a tempered distribution u is empty, then its
sphere component ConicSingularSupportSphere u is also empty.
If the conic singular support set Css u of a tempered distribution u is empty, then its
ordinary singular support is also empty.
If the conic singular support set Css u of a tempered distribution u is empty, then its
cone singular support (the union of singular support and conic sphere part) is also empty.
When the conic singular support Css u of a tempered distribution is empty, produce a Schwartz
function whose Schwartz embedding equals u.
Instances For
Predicate that ψ₁ acts as a conic cutoff separating conic singular supports K₁ and K₂:
multiplying by ψ₁ (resp. 1 - ψ₁) kills the conic singular support of any distribution whose
Css lies in K₂ (resp. K₁).
- schwartz_of_mul (u₂ : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : Css u₂ ⊆ K₂ → Css ((TemperedDistribution.smulLeftCLM ℂ ψ₁) u₂) = ∅
- schwartz_of_compl_mul (u₁ : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : Css u₁ ⊆ K₁ → Css ((TemperedDistribution.smulLeftCLM ℂ (1 - ψ₁)) u₁) = ∅
Instances For
Pairing of distributions u₁, u₂ with disjoint conic singular supports, defined via a
specified conic cutoff ψ₁: applies u₁ to the Schwartz representative of ψ₁ · u₂ and u₂ to
the Schwartz representative of (1 - ψ₁) · u₁, then sums.
Instances For
The Schwartz embedding of toSchwartzOfEmptyCss u h recovers the original tempered
distribution u.
Partition of unity identity: for any temperate-growth φ and tempered distribution u, we have
φ · u + (1 - φ) · u = u.
The Schwartz embedding schwEmbed : 𝓢(ℝⁿ, ℂ) → 𝓢'(ℝⁿ, ℂ) is injective.
If a temperate-growth function χ agrees outside a ball with smooth homogeneous functions
vanishing at every direction of the conic singular support of u, then the conic singular support
of χ · u is empty.
Multiplication by χ fixes the Schwartz-valued differences (ψ₁ - ψ₁') · u₂ and
((1 - ψ₁') - (1 - ψ₁)) · u₁ arising from a pair of conic cutoffs for disjoint conic singular
supports.
If two distributions u₁, u₂ have conic singular supports contained in disjoint sets
K₁, K₂, then their conic singular support spheres are also disjoint.
Existence of a temperate-growth cutoff χ such that χ · u₁ and χ · u₂ both have empty
conic singular support and χ fixes the relevant Schwartz-valued differences.
Existence of a temperate-growth cutoff χ making the conic singular supports of χ · u₁ and
χ · u₂ empty while fixing the Schwartz differences associated to the cutoffs ψ₁ and ψ₁'.
Given Schwartz representatives for χ · u₁, χ · u₂ and Schwartz functions f, g with
prescribed embeddings (and fixed by χ-multiplication), the pairings u₁ f and u₂ g agree.
Cross-pairing identity: under the empty-Css and fixing hypotheses on χ, the pairings of
the Schwartz representatives c₁, c₂ with the Schwartz functions f, g corresponding to the two
cutoffs coincide.
Bundled existence statement combining exists_chi_css_empty with the cross-pairing identity:
there is a temperate-growth χ whose multiplication empties the conic singular supports, fixes the
Schwartz differences, and makes the cross-pairings of the Schwartz representatives agree.
If multiplication by a temperate-growth χ fixes a tempered distribution v, then
multiplication by 1 - χ annihilates v.
Existence of auxiliary Schwartz representatives c₁, c₂ such that pairings of u₁ and u₂
with the Schwartz preimages of the cutoff differences factor through the embeddings of c₁ and
c₂, and the cross-pairings agree.
Independence-of-cutoff key identity: the pairing of u₁ with the Schwartz preimage of
(ψ₁ - ψ₁') · u₂ equals the pairing of u₂ with the Schwartz preimage of
((1 - ψ₁') - (1 - ψ₁)) · u₁.
The value of cssPairingWith ψ₁ hψ u₁ h₁ u₂ h₂ is independent of the choice of conic cutoff
ψ₁: any two valid cutoffs give equal pairings.
Existence of a canonical pairing P u₁ u₂ for distributions with disjoint conic singular
supports K₁, K₂, which agrees with cssPairingWith for every choice of conic cutoff.