theorem WavefrontSet.wfsc_decomposition_iff {n : ℕ} {u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ} {p q : ClosedBall n} (hpq : (p, q) ∈ BoundaryProd n) : (p, q) ∉ WFsc u ↔ ∃ (u₁ : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (u₂ : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ), u = u₁ + u₂ ∧ p ∉ Css u₁ ∧ q ∉ Css (FourierTransform.fourier u₂)

Decomposition characterization of the scattering wavefront set on boundary pairs: for (p, q) ∈ BoundaryProd n, the pair lies outside WFsc u iff u decomposes as u = u₁ + u₂ with p outside the scattering singular support of u₁ and q outside the scattering singular support of 𝓕 u₂.