theorem WavefrontSet.isSmoothNear_fourier_smulLeftCLM_compactlySupported {n : ℕ} (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (φ : ConeSupport.E n → ℂ) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (x : EuclideanSpace ℝ (Fin n)) : ConeSupport.IsSmoothNear (FourierTransform.fourier ((TemperedDistribution.smulLeftCLM ℂ φ) u)) x

The Fourier transform of a compactly supported (smooth) multiplication of any tempered distribution u is smooth near every point.

theorem WavefrontSet.not_mem_css_fourier_compactlySupported_interior {n : ℕ} (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (φ : ConeSupport.E n → ℂ) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (q : ClosedBall n) (hq : ‖↑q‖ < 1) : q ∉ Css (FourierTransform.fourier ((TemperedDistribution.smulLeftCLM ℂ φ) u))

Interior points of the closed ball never appear in Css of the Fourier transform of a compactly supported smooth multiplication: the singular support is empty there.

theorem WavefrontSet.wfsc_subset_boundaryProd {n : ℕ} (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : WFsc u ⊆ BoundaryProd n

The wavefront set WFsc u (in the sphere-compactified sense) is contained in the boundary product BoundaryProd n.

theorem WavefrontSet.not_mem_css_iff_neg_not_mem_css_fourier_fourier' {n : ℕ} (u₁ : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (p : ClosedBall n) : p ∉ Css u₁ ↔ -p ∉ Css (FourierTransform.fourier (FourierTransform.fourier u₁))

A renamed wrapper around not_mem_css_iff_neg_not_mem_css_fourier_fourier: non-membership in Css u₁ at p is equivalent to non-membership in Css (𝓕(𝓕 u₁)) at -p.

theorem WavefrontSet.mem_wfsc_fourier_fourier_iff_neg_mem_wfsc' {n : ℕ} (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (a b : ClosedBall n) : (a, b) ∈ WFsc (FourierTransform.fourier (FourierTransform.fourier u)) ↔ (-a, -b) ∈ WFsc u

Symmetry under double Fourier transform on the wavefront set: (a, b) ∈ WFsc(𝓕 𝓕 u) iff (-a, -b) ∈ WFsc u.

theorem WavefrontSet.boundaryProd_swap_neg' {n : ℕ} {p q : ClosedBall n} (hpq : (p, q) ∈ BoundaryProd n) : (q, -p) ∈ BoundaryProd n

The boundary-product set is preserved under the swap-and-negate map (p, q) ↦ (q, -p).

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

One direction of the Fourier symmetry on wavefront sets: if (p, q) ∉ WFsc u on the boundary product, then (q, -p) ∉ WFsc(𝓕 u).

theorem WavefrontSet.mem_wfsc_iff_swap_neg_mem_wfsc_fourier' {n : ℕ} (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (p q : ClosedBall n) : (p, q) ∈ WFsc u ↔ (q, -p) ∈ WFsc (FourierTransform.fourier u)

Melrose Corollary 12.17: the wavefront set transforms under the Fourier transform via (p, q) ∈ WFsc u ↔ (q, -p) ∈ WFsc(𝓕 u).