theorem
ConeSupport.convolution_well_defined_lemma_12_6
{n : ℕ}
{u : TemperedDistribution (E n) ℂ}
(hu : ConicSingularSupportSphere u = ∅)
(C : ConvolutionSystem n)
(d₁ d₂ : SchwartzCompactDecomp u)
:
C.convSchwartz d₁.schwartzPart + C.convCompact d₁.compactPart = C.convSchwartz d₂.schwartzPart + C.convCompact d₂.compactPart
Melrose's Lemma 12.6: the convolution u * v extending the classical product to
distributions with empty conic singular support sphere is independent of the choice of
Schwartz/compactly supported decomposition of u.
noncomputable def
ConeSupport.extendedConvolution
{n : ℕ}
(u v : TemperedDistribution (E n) ℂ)
(hu : ConicSingularSupportSphere u = ∅)
:
TemperedDistribution (E n) ℂ
The extended convolution u ⋆ v of tempered distributions, defined when the left
factor u has empty conic singular support sphere by decomposing u into a Schwartz part
and a compactly supported part and convolving each with v (Melrose, Section 12).
Instances For
noncomputable def
ConeSupport.extendedConvolutionRight
{n : ℕ}
(u v : TemperedDistribution (E n) ℂ)
(hv : ConicSingularSupportSphere v = ∅)
:
TemperedDistribution (E n) ℂ
The extended convolution u ⋆ v of tempered distributions, defined when the right
factor v has empty conic singular support sphere by decomposing v into a Schwartz part
and a compactly supported part and convolving each with u.