theorem ConeSupport.convolution_decomp_well_defined_direct {n : ℕ} {u : TemperedDistribution (E n) ℂ} (hu : ConicSingularSupportSphere u = ∅) (convSchwartz : SchwartzMap (E n) ℂ → TemperedDistribution (E n) ℂ) (convCompact : TemperedDistribution (E n) ℂ → TemperedDistribution (E n) ℂ) (hSchwartz_add : ∀ (φ₁ φ₂ : SchwartzMap (E n) ℂ), convSchwartz (φ₁ + φ₂) = convSchwartz φ₁ + convSchwartz φ₂) (hCompact_add : ∀ (u₁ u₂ : TemperedDistribution (E n) ℂ), convCompact (u₁ + u₂) = convCompact u₁ + convCompact u₂) (hcompat : ∀ (φ : SchwartzMap (E n) ℂ), IsCompactlySupportedDistribution (schwEmbed φ) → convSchwartz φ = convCompact (schwEmbed φ)) (d₁ d₂ : SchwartzCompactDecomp u) : convSchwartz d₁.schwartzPart + convCompact d₁.compactPart = convSchwartz d₂.schwartzPart + convCompact d₂.compactPart

Direct, axiom-free version of Lemma 12.6 of Melrose: given a tempered distribution u with empty conic singular support on the sphere, and two linear-and-additive convolution operations convSchwartz (on Schwartz functions) and convCompact (on compactly-supported distributions) that agree on Schwartz functions whose embedding is compactly-supported, the sum convSchwartz d.schwartzPart + convCompact d.compactPart does not depend on the choice of decomposition d of u into a Schwartz and a compactly-supported part.