def ConeSupport.HasExtendedConvolution {n : ℕ} (u v : TemperedDistribution (E n) ℂ) : Prop

Two tempered distributions u, v admit an extended convolution as soon as at least one of them has empty conic singular support on the sphere; this is the side condition under which the convolution u * v can be defined microlocally.

noncomputable def ConeSupport.extConv {n : ℕ} (u v : TemperedDistribution (E n) ℂ) (h : HasExtendedConvolution u v) : TemperedDistribution (E n) ℂ

The extended convolution u * v defined under HasExtendedConvolution u v by splitting the distribution with empty conic singular support into a Schwartz part and a compactly supported part.

theorem ConeSupport.extConv_eq_of_decomp {n : ℕ} (u v : TemperedDistribution (E n) ℂ) (h : HasExtendedConvolution u v) (hu : ConicSingularSupportSphere u = ∅) (d : SchwartzCompactDecomp u) : extConv u v h = (standardConvolutionSystem v).convSchwartz d.schwartzPart + (standardConvolutionSystem v).convCompact d.compactPart

Independence of the extended convolution on the Schwartz/compact decomposition: any choice of SchwartzCompactDecomp u (under ConicSingularSupportSphere u = ∅) yields the same value for extConv u v h.

theorem ConeSupport.IsConicCutoffNear.mul {n : ℕ} {ga gb : E n → ℂ} {ω : ↑(Sphere n)} (ha : IsConicCutoffNear ga ω) (hb : IsConicCutoffNear gb ω) : IsConicCutoffNear (ga * gb) ω

The product of two conic cutoff functions near a direction ω is again a conic cutoff near ω: the smoothness, support, and conic-extension properties are preserved by multiplication.

theorem ConeSupport.ConicSingularSupportSphere_add_subset {n : ℕ} (a b : TemperedDistribution (E n) ℂ) : ConicSingularSupportSphere (a + b) ⊆ ConicSingularSupportSphere a ∪ ConicSingularSupportSphere b

Subadditivity of the conic singular support on the sphere under addition of distributions: ConicSingularSupportSphere (a + b) ⊆ ConicSingularSupportSphere a ∪ ConicSingularSupportSphere b.

theorem ConeSupport.singularSupport_add_subset {n : ℕ} (a b : TemperedDistribution (E n) ℂ) : singularSupport (a + b) ⊆ singularSupport a ∪ singularSupport b

Subadditivity of the singular support under addition of tempered distributions: sing supp (a + b) ⊆ sing supp a ∪ sing supp b.

theorem ConeSupport.singularSupport_extConv_decomp {n : ℕ} (u v : TemperedDistribution (E n) ℂ) (h : HasExtendedConvolution u v) (hu : ConicSingularSupportSphere u = ∅) (d : SchwartzCompactDecomp u) : singularSupport (extConv u v h) ⊆ singularSupport ((standardConvolutionSystem v).convSchwartz d.schwartzPart) ∪ singularSupport ((standardConvolutionSystem v).convCompact d.compactPart)

The singular support of extConv u v h is contained in the union of the singular supports of the convolutions of v with the Schwartz and compact parts of u.

theorem ConeSupport.smulLeft_schwartzConvolution_of_compactBump {n : ℕ} (v : TemperedDistribution (E n) ℂ) (φ : SchwartzMap (E n) ℂ) (ψ : E n → ℂ) (hψ_smooth : ContDiff ℝ (↑⊤) ψ) (hψ_compact : HasCompactSupport ψ) : ∃ (f : SchwartzMap (E n) ℂ), (TemperedDistribution.smulLeftCLM ℂ ψ) (schwartzConvolution v φ) = schwEmbed f

Multiplying the Schwartz convolution v * φ on the left by a smooth compactly supported function ψ produces a tempered distribution which is again represented by a Schwartz function.

theorem ConeSupport.schwartzConvolution_isSmoothNear {n : ℕ} (v : TemperedDistribution (E n) ℂ) (φ : SchwartzMap (E n) ℂ) (x : E n) : IsSmoothNear (schwartzConvolution v φ) x

The convolution of a tempered distribution with a Schwartz function is smooth at every point: locally one can multiply by a compactly supported bump to obtain a Schwartz representative.

theorem ConeSupport.singularSupport_convSchwartz_empty {n : ℕ} (v : TemperedDistribution (E n) ℂ) (φ : SchwartzMap (E n) ℂ) : singularSupport ((standardConvolutionSystem v).convSchwartz φ) = ∅

Convolution of any tempered distribution with a Schwartz function has empty singular support: it is smooth everywhere.

theorem ConeSupport.isCompactlySupportedDistribution_iff_hasCompactSupport {n : ℕ} (w : TemperedDistribution (E n) ℂ) : IsCompactlySupportedDistribution w ↔ DifferentialOperators.HasCompactSupport w

The two notions of "compactly supported distribution" used in the cone-support and differential-operators namespaces coincide definitionally.

theorem ConeSupport.convCompact_eq_distribConvolution {n : ℕ} (v w : TemperedDistribution (E n) ℂ) (hw : DifferentialOperators.HasCompactSupport w) : (standardConvolutionSystem v).convCompact w = DifferentialOperators.distribConvolution w v hw

The convolution-system specialisation convCompact v w for a compactly supported w coincides with the DifferentialOperators.distribConvolution w v hw construction.

theorem ConeSupport.singularSupport_eq_of_namespaces {n : ℕ} (u : TemperedDistribution (E n) ℂ) : singularSupport u = DifferentialOperators.singularSupport u

The ConeSupport.singularSupport and DifferentialOperators.singularSupport definitions of the singular support of a tempered distribution agree.

theorem ConeSupport.singularSupport_convCompact_subset {n : ℕ} (v w : TemperedDistribution (E n) ℂ) (hw : IsCompactlySupportedDistribution w) : singularSupport ((standardConvolutionSystem v).convCompact w) ⊆ singularSupport w + singularSupport v

Singular support of a convolution with a compactly supported distribution: the standard microlocal inclusion sing supp (v * w) ⊆ sing supp w + sing supp v.

theorem ConeSupport.singularSupport_compactPart_subset {n : ℕ} (u : TemperedDistribution (E n) ℂ) (d : SchwartzCompactDecomp u) : singularSupport d.compactPart ⊆ singularSupport u

Singular support of the compact part of a Schwartz/compact decomposition is contained in the singular support of the original distribution.

theorem ConeSupport.singularSupport_extConv_subset {n : ℕ} (u v : TemperedDistribution (E n) ℂ) (h : HasExtendedConvolution u v) (hu : ConicSingularSupportSphere u = ∅) : singularSupport (extConv u v h) ⊆ singularSupport u + singularSupport v

Singular support of the extended convolution: sing supp (extConv u v h) ⊆ sing supp u + sing supp v, the microlocal inclusion for the extended convolution.

theorem ConeSupport.cssSphere_extConv_decomp {n : ℕ} (u v : TemperedDistribution (E n) ℂ) (h : HasExtendedConvolution u v) (hu : ConicSingularSupportSphere u = ∅) (d : SchwartzCompactDecomp u) : ConicSingularSupportSphere (extConv u v h) ⊆ ConicSingularSupportSphere ((standardConvolutionSystem v).convSchwartz d.schwartzPart) ∪ ConicSingularSupportSphere ((standardConvolutionSystem v).convCompact d.compactPart)

The conic singular support of extConv u v h is contained in the union of the conic singular supports of the Schwartz and compact convolution components.

theorem ConeSupport.cssSphere_convSchwartz_subset {n : ℕ} (v : TemperedDistribution (E n) ℂ) (φ : SchwartzMap (E n) ℂ) : ConicSingularSupportSphere ((standardConvolutionSystem v).convSchwartz φ) ⊆ ConicSingularSupportSphere v

Conic singular support is monotone under convolution with a Schwartz function: CSS_sphere (v * φ) ⊆ CSS_sphere v.

theorem ConeSupport.standardConvolutionSystem_convCompact_add_right {n : ℕ} (v₁ v₂ w : TemperedDistribution (E n) ℂ) : (standardConvolutionSystem (v₁ + v₂)).convCompact w = (standardConvolutionSystem v₁).convCompact w + (standardConvolutionSystem v₂).convCompact w

Additivity of convCompact in the right argument of standardConvolutionSystem: (v₁ + v₂) * w = v₁ * w + v₂ * w for compactly supported w.

theorem ConeSupport.distribConvolution_assoc {n : ℕ} (w : TemperedDistribution (E n) ℂ) (hw : DifferentialOperators.HasCompactSupport w) (φ ψ : SchwartzMap (E n) ℂ) : (schwEmbed φ) ((DifferentialOperators.convolutionSchwartzCLM w hw) ψ) = w (((SchwartzMap.convolution (ContinuousLinearMap.lsmul ℂ ℂ)) φ) ψ)

Associativity of distributional convolution with Schwartz functions: pairing the Schwartz function φ against the convolution w * ψ equals pairing w against the Schwartz convolution φ * ψ.

theorem ConeSupport.distribFubini_conv {n : ℕ} (w : TemperedDistribution (E n) ℂ) (hw : DifferentialOperators.HasCompactSupport w) (φ ψ F : SchwartzMap (E n) ℂ) (hF : ∀ (y : E n), F y = ∫ (x : E n), φ x • ψ (y - x)) : ∫ (x : E n), ((DifferentialOperators.convolutionSchwartzCLM w hw) ψ) x • φ x = w F

A distributional Fubini formula: the integral of (w * ψ) · φ equals the pairing of w with the Schwartz function F(y) = ∫ φ(x) ψ(y - x) dx.

theorem ConeSupport.convolutionSchwartzCLM_L2_symmetric {n : ℕ} (w : TemperedDistribution (E n) ℂ) (hw : DifferentialOperators.HasCompactSupport w) (φ ψ : SchwartzMap (E n) ℂ) : ∫ (x : E n), ((DifferentialOperators.convolutionSchwartzCLM w hw) ψ) x • φ x = ∫ (x : E n), ψ x • ((DifferentialOperators.convolutionSchwartzCLM w hw) φ) x

L² symmetry of the convolution operator with a compactly supported distribution w: ⟨w * ψ, φ⟩_{L²} = ⟨ψ, w * φ⟩_{L²}, an instance of the Fubini-type identity.

theorem ConeSupport.distribConvolution_schwEmbed_isSchwartz {n : ℕ} (φ : SchwartzMap (E n) ℂ) (w : TemperedDistribution (E n) ℂ) (hw : DifferentialOperators.HasCompactSupport w) : ∃ (f : SchwartzMap (E n) ℂ), DifferentialOperators.distribConvolution w (schwEmbed φ) hw = schwEmbed f

Convolution of a compactly supported distribution w with the embedded Schwartz function φ yields a tempered distribution represented by a Schwartz function.

theorem ConeSupport.convCompact_schwEmbed_isSchwartz {n : ℕ} (φ : SchwartzMap (E n) ℂ) (w : TemperedDistribution (E n) ℂ) (hw : IsCompactlySupportedDistribution w) : ∃ (f : SchwartzMap (E n) ℂ), (standardConvolutionSystem (schwEmbed φ)).convCompact w = schwEmbed f

convCompact of a compactly supported distribution with the embedded Schwartz function φ is itself represented by a Schwartz function.

theorem ConeSupport.cssSphere_convCompact_schwartz_param_empty {n : ℕ} (φ : SchwartzMap (E n) ℂ) (w : TemperedDistribution (E n) ℂ) (hw : IsCompactlySupportedDistribution w) : ConicSingularSupportSphere ((standardConvolutionSystem (schwEmbed φ)).convCompact w) = ∅

When the parameter of standardConvolutionSystem is a Schwartz function (embedded as a distribution), convCompact always has empty conic singular support on the sphere.

theorem ConeSupport.compactDistribConv_zero_right {n : ℕ} (w : TemperedDistribution (E n) ℂ) : compactDistribConv 0 w = 0

Vanishing of compactDistribConv in the left argument when this is zero: (0) * w = 0.

theorem ConeSupport.smulLeftCLM_compactDistribConv_vanishing {n : ℕ} (v w : TemperedDistribution (E n) ℂ) (hw : IsCompactlySupportedDistribution w) (g₀ : E n → ℂ) (hg₀_vanish : (TemperedDistribution.smulLeftCLM ℂ g₀) v = 0) : (TemperedDistribution.smulLeftCLM ℂ g₀) (compactDistribConv v w) = 0

If multiplication of v by g₀ annihilates v, then the same multiplication annihilates compactDistribConv v w for any compactly supported w.

theorem ConeSupport.conicCutoff_smul_compactConvolution_schwartz_of_vanishing {n : ℕ} (v w : TemperedDistribution (E n) ℂ) (hw : IsCompactlySupportedDistribution w) (g₀ : E n → ℂ) (ω : ↑(Sphere n)) (hg₀ : IsConicCutoffNear g₀ ω) (hg₀_vanish : (TemperedDistribution.smulLeftCLM ℂ g₀) v = 0) : ∃ (f : SchwartzMap (E n) ℂ), (TemperedDistribution.smulLeftCLM ℂ g₀) ((standardConvolutionSystem v).convCompact w) = (SchwartzMap.toTemperedDistributionCLM (E n) ℂ MeasureTheory.volume) f

If a conic cutoff g₀ near ω annihilates v, then g₀ · (v * w) is a Schwartz function for any compactly supported w; here this is exhibited by the zero Schwartz function.

theorem ConeSupport.cssSphere_convCompact_coneSupportDisjoint {n : ℕ} (v w : TemperedDistribution (E n) ℂ) (hw : IsCompactlySupportedDistribution w) (Γ : Set ↑(Sphere n)) (hdisjoint : Disjoint (ConicSupportSphere v) Γ) : Disjoint (ConicSingularSupportSphere ((standardConvolutionSystem v).convCompact w)) Γ

Microlocal control: if a direction set Γ is disjoint from the conic support of v, then it is also disjoint from the conic singular support of v * w for compactly supported w.

theorem ConeSupport.cssSphere_add_subset {n : ℕ} (u₁ u₂ : TemperedDistribution (E n) ℂ) : ConicSingularSupportSphere (u₁ + u₂) ⊆ ConicSingularSupportSphere u₁ ∪ ConicSingularSupportSphere u₂

Short-name alias for the subadditivity of ConicSingularSupportSphere under addition.

theorem ConeSupport.cssSphere_convCompact_subset {n : ℕ} (v w : TemperedDistribution (E n) ℂ) (hw : IsCompactlySupportedDistribution w) : ConicSingularSupportSphere ((standardConvolutionSystem v).convCompact w) ⊆ ConicSingularSupportSphere v

Convolution with a compactly supported distribution does not enlarge the conic singular support on the sphere: CSS_sphere (v * w) ⊆ CSS_sphere v.

theorem ConeSupport.cssSphere_extConv_subset {n : ℕ} (u v : TemperedDistribution (E n) ℂ) (h : HasExtendedConvolution u v) (hu : ConicSingularSupportSphere u = ∅) : ConicSingularSupportSphere (extConv u v h) ⊆ ConicSingularSupportSphere v

Conic singular support of the extended convolution: CSS_sphere (extConv u v h) ⊆ CSS_sphere v, recovering the microlocal direction control.

theorem ConeSupport.css_convolution_subset {n : ℕ} (u v : TemperedDistribution (E n) ℂ) (h : HasExtendedConvolution u v) (hu : ConicSingularSupportSphere u = ∅) : coneSingularSupport (extConv u v h) ⊆ Sum.inl '' (singularSupport u + singularSupport v) ∪ Sum.inr '' ConicSingularSupportSphere v

Microlocal inclusion for the cone singular support of the extended convolution: the cone singular support of extConv u v h is contained in the union of the Minkowski sum of singular supports (in the Sum.inl block) and the conic singular support of v (in the Sum.inr block). This is Cor 12.17 in Melrose.