theorem ConeSupport.exists_decomposition_disjoint_conicSingularSupport' {n : ℕ} (u : TemperedDistribution (E n) ℂ) (Γ : Set ↑(Sphere n)) (hΓ_closed : IsClosed Γ) (hΓ_disjoint : Disjoint (ConicSingularSupportSphere u) Γ) : ∃ (u₁' : TemperedDistribution (E n) ℂ) (u₁'' : TemperedDistribution (E n) ℂ) (u₂ : SchwartzMap (E n) ℂ), u = u₁' + u₁'' + (SchwartzMap.toTemperedDistributionCLM (E n) ℂ MeasureTheory.volume) u₂ ∧ IsCompactlySupportedDistribution u₁' ∧ (∃ (ε : ℝ), 0 < ε ∧ ∀ (f : SchwartzMap (E n) ℂ), (∀ (x : E n), ε ≤ ‖x‖ → f x = 0) → u₁'' f = 0) ∧ (∀ (f : SchwartzMap (E n) ℂ), (∀ (x : E n), f x ≠ 0 → x ≠ 0 ∧ ∀ (hx : x ≠ 0), directionOf x hx ∈ Γ) → u₁'' f = 0) ∧ Disjoint (ConicSupportSphere (u₁' + u₁'')) Γ

Decomposition of a tempered distribution u away from a closed conic set Γ disjoint from the conic singular support: u can be written as u₁' + u₁'' + u₂ where u₁' is compactly supported, u₁'' vanishes on test functions supported far from the origin and supported in directions in Γ, u₂ is Schwartz, and the conic support of u₁' + u₁'' is disjoint from Γ.