theorem WavefrontSet.not_mem_css_zero {n : ℕ} (p : ClosedBall n) : p ∉ Css 0

The zero tempered distribution has empty conic singular support: any p lies outside Css 0.

theorem WavefrontSet.not_mem_css_fourier_zero {n : ℕ} (q : ClosedBall n) : q ∉ Css (FourierTransform.fourier 0)

The Fourier transform of zero is zero, so its conic singular support is empty.

theorem WavefrontSet.css_subadditive_not_mem {n : ℕ} {u₁ u₂ : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ} {p : ClosedBall n} (h₁ : p ∉ Css u₁) (h₂ : p ∉ Css u₂) : p ∉ Css (u₁ + u₂)

Subadditivity of the conic singular support: if p ∉ Css u₁ and p ∉ Css u₂, then p ∉ Css (u₁ + u₂).

theorem WavefrontSet.not_mem_css_implies_not_mem_wfsc_fst' {n : ℕ} (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (p q : ClosedBall n) (hp : p ∉ Css u) (hpq : (p, q) ∈ BoundaryProd n) : (p, q) ∉ WFsc u

If p lies outside Css u, then (p, q) lies outside WFsc u for any boundary pair (p, q).

theorem WavefrontSet.not_mem_css_fourier_implies_not_mem_wfsc_snd' {n : ℕ} (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (p q : ClosedBall n) (hq : q ∉ Css (FourierTransform.fourier u)) (hpq : (p, q) ∈ BoundaryProd n) : (p, q) ∉ WFsc u

If q lies outside Css (𝓕 u), then (p, q) lies outside WFsc u for any boundary pair (p, q).

theorem WavefrontSet.wfsc_subadditive' {n : ℕ} (u₁ u₂ : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (p q : ClosedBall n) (h₁ : (p, q) ∉ WFsc u₁) (h₂ : (p, q) ∉ WFsc u₂) : (p, q) ∉ WFsc (u₁ + u₂)

Subadditivity of the scattering wavefront set: if (p, q) ∉ WFsc u₁ and (p, q) ∉ WFsc u₂, then (p, q) ∉ WFsc (u₁ + u₂).

theorem WavefrontSet.exists_decomp_of_not_mem_wfsc' {n : ℕ} {u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ} {p q : ClosedBall n} (hpq : (p, q) ∈ BoundaryProd n) (h : (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₂)

If (p, q) ∉ WFsc u, then u decomposes as u₁ + u₂ with p ∉ Css u₁ and q ∉ Css (𝓕 u₂).

theorem WavefrontSet.not_mem_wfsc_iff_exists_css_decomp {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₂)

Equivalence (Melrose Thm 12.18-style): (p, q) ∉ WFsc u iff u decomposes into pieces avoiding p in physical and q in Fourier conic singular support.