Chapter 12: Microlocal Analysis

This file formalizes the key definitions and results from Chapter 12 on microlocal analysis, including cone support, wavefront sets, and products of distributions.

The source text for Chapter 12 is not included in book/book.md. The mathematical content is based on the standard theory of microlocal analysis (Hörmander, The Analysis of Linear Partial Differential Operators I, Chapter 8). Since the source text is unavailable, definitions are declared as opaque constants (their construction requires smooth partition- of-unity infrastructure not available in Mathlib) and all results are axiomatized.

Main definitions

• ConeSupport — Definition 12.2 (Goal 93): The cone support of a tempered distribution.
• WavefrontSet — Definition 12.12 (Goal 103): The wavefront set of a distribution.
• ScatteringWavefrontSet — Definition 12.12: The scattering wavefront set of a distribution.

Main results

• lemma_12_1 — Lemma 12.1 (Goal 92): Derivative bounds for homogeneous degree 0 functions.
• lemma_12_3 — Lemma 12.3 (Goal 94): Cone support is a closed cone in ℝⁿ ∖ {0}.
• lemma_12_3_css — Lemma 12.3: Cone singular support is a closed cone in ℝⁿ ∖ {0}.
• lemma_12_3_css_cutoff — Lemma 12.3: Cutoff outside Css gives Schwartz.
• corollary_12_4 — Corollary 12.4 (Goal 95): Empty cone support implies Schwartz Fourier transform.
• corollary_12_4_css_empty_iff_schwartz — Corollary 12.4 (Css version): Css(u) = ∅ ↔ u ∈ S(ℝⁿ).
• lemma_12_5 — Lemma 12.5 (Goal 96): Smooth multiplication does not enlarge cone support.
• lemma_12_6 — Lemma 12.6 (Goal 97): Differentiation does not enlarge cone support.
• lemma_12_7 — Lemma 12.7 (Goal 98): Cone support of sum ⊆ union of cone supports.
• lemma_12_8 — Lemma 12.8 (Goal 99): Fourier localization and cone support.
• corollary_12_9 — Corollary 12.9 (Goal 100): Nonzero scalar multiplication preserves cone support.
• lemma_12_10 — Lemma 12.10 (Goal 101): Iterated differentiation preserves cone support.
• IsConicCutoff — A predicate characterizing conic cutoff distributions.
• lemma_12_11 — Lemma 12.11 (Goal 102): For a conic cutoff ψ_R, Css(ψ̂_R) ⊆ {0}.
• lemma_12_13 — Lemma 12.13 (Goal 104): Wavefront set ⊆ base × (ℝⁿ ∖ {0}).
• SingularSupport — The singular support of a tempered distribution.
• proposition_12_14 — Proposition 12.14 (Goal 105): WF(u) is closed and conic.
• proposition_12_14_wfsc — Proposition 12.14: WF_sc(u) is closed, ⊆ ∂(B̄ⁿ × B̄ⁿ), π₁(WF) = singsupp, π₁(WF_sc) = Css.
• corollary_12_15 — Corollary 12.15 (Goal 106): WF(u) = ∅ ↔ u is smooth.
• corollary_12_15_wfsc_empty_schwartz — Corollary 12.15: WF_sc(u) = ∅ ↔ u ∈ S(ℝⁿ).
• proposition_12_16 — Proposition 12.16 (Goal 107): WF is stable under differentiation and smooth mult.
• corollary_12_17 — Corollary 12.17 (Goal 108): WF of restrictions.
• corollary_12_17_wfsc_fourier_symmetry — Corollary 12.17: (p,q) ∈ WF_sc(u) ↔ (q,-p) ∈ WF_sc(û).
• theorem_12_18 — Theorem 12.18 (Goal 109): Hörmander's product theorem.
• theorem_12_18_product_wfsc — Theorem 12.18 (WF_sc product): Product defined under scattering WF condition.
• theorem_12_18_convolution_wfsc — Theorem 12.18 (WF_sc convolution): Convolution defined under scattering WF condition.
• lemma_12_5_pairing_disjoint_css — Lemma 12.5 (Pairing): Unambiguous bilinear pairing for distributions with disjoint Css.
• lemma_12_6_css_implies_convolution_condition — Lemma 12.6: Css(u) ∩ S^{n-1} = ∅ implies convolution WF_sc condition.
• convolutionCssEmptySphere — The convolution u * v when Css(u) ∩ S^{n-1} = ∅.
• lemma_12_6_convolution_css_empty_sphere — Lemma 12.6: Convolution is unambiguous under Css ∩ S^{n-1} = ∅.
• corollary_12_9_css_convolution_bound — Corollary 12.9: Css(u*v) ⊆ (singsupp(u)+singsupp(v)) ∪ (Css(v) ∩ S^{n-1}).

@[reducible, inline]

abbrev Chapter12.Rn (n : ℕ) : Type

Abbreviation for the Euclidean space ℝⁿ used throughout Chapter 12.

def Chapter12.IsHomogeneousOutside {n : ℕ} (f : Rn n → ℂ) (k : ℤ) : Prop

A function f : ℝⁿ → ℂ is homogeneous of degree k outside the unit ball if f(tξ) = t^k f(ξ) for all t > 0 and ‖ξ‖ ≥ 1.

def Chapter12.IsCone {n : ℕ} (Γ : Set (Rn n)) : Prop

A subset Γ ⊆ ℝⁿ is a cone if it is invariant under positive scalar multiplication: for all t > 0 and ξ ∈ Γ, we have t • ξ ∈ Γ.

def Chapter12.IsRapidlyDecreasing {n : ℕ} (g : Rn n → ℂ) : Prop

A function g : ℝⁿ → ℂ is rapidly decreasing if for every N : ℕ, there exists C > 0 such that ‖g(ξ)‖ ≤ C (1 + ‖ξ‖)^{-N} for all ξ.

def Chapter12.IsHomogeneousDegZero {n : ℕ} (f : Rn n → ℂ) : Prop

A function f : ℝⁿ → ℂ is homogeneous of degree 0 on ℝⁿ ∖ {0} if f(t • x) = f(x) for all t > 0 and x ≠ 0. This is the standard definition of degree-0 homogeneity appearing in Lemma 12.1.

Lemma 12.1: Homogeneous degree 0 derivative bound (Goal 92)

If f : ℝⁿ → ℂ is smooth and homogeneous of degree 0 outside a neighborhood of the origin, then for every derivative order k, there exists C_k > 0 such that ‖iteratedFDeriv ℝ k f ξ‖ ≤ C_k ‖ξ‖^{-k} for all ξ with ‖ξ‖ ≥ 1. The proof is not given in the source text.

theorem Chapter12.lemma_12_1 {n : ℕ} (f : Rn n → ℂ) (hf : ContDiff ℝ ⊤ f) (h0 : IsHomogeneousOutside f 0) (k : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (ξ : Rn n), 1 ≤ ‖ξ‖ → ‖iteratedFDeriv ℝ k f ξ‖ ≤ C * ‖ξ‖⁻¹ ^ k

Lemma 12.1 (Goal 92). If ψ ∈ C^∞(ℝⁿ) is homogeneous of degree 0 outside the unit ball, then |D^α ψ(x)| ≤ C_α |x|^{-|α|} for ‖x‖ ≥ 1. The proof is not given in the source text.

Definition 12.2: Cone support and cone singular support (Goal 93)

The cone support Csp(u) and cone singular support Css(u) of a tempered distribution u ∈ S'(ℝⁿ) are subsets of ℝⁿ ∪ S^{n-1} defined by:

• Csp(u) ∩ ℝⁿ = supp(u)
• (Csp(u))^c ∩ S^{n-1} = {ω ∈ S^{n-1} : ∃ R>0, ψ ∈ C^∞(S^{n-1}), ψ(ω) ≠ 0, ψ_R u = 0}
• Css(u) ∩ ℝⁿ = singsupp(u)
• (Css(u))^c ∩ S^{n-1} = {ω ∈ S^{n-1} : ∃ R>0, ψ ∈ C^∞(S^{n-1}), ψ(ω) ≠ 0, ψ_R u ∈ S(ℝⁿ)}

Here ψ_R denotes the extension of ψ from S^{n-1} to ℝⁿ by homogeneity of degree 0, cut off within the ball of radius R.

We model the "at infinity" part as a conic subset of ℝⁿ ∖ {0}: a direction ξ₀ ≠ 0 is NOT in the cone support if there exists a smooth function φ : ℝⁿ → ℂ, homogeneous of degree 0 outside a ball, with φ(ξ₀) ≠ 0, such that φ · u = 0 as a tempered distribution. Similarly for the cone singular support, replacing = 0 with ∈ S(ℝⁿ).

def Chapter12.ConeSupport (n : ℕ) (u : TemperedDistribution (Rn n) ℂ) : Set (Rn n)

Definition 12.2 (Cone support). The cone support of a tempered distribution u ∈ S'(ℝⁿ) is the set of nonzero directions ξ₀ ∈ ℝⁿ such that no smooth function φ, homogeneous of degree 0 outside a ball, satisfies both φ(ξ₀) ≠ 0 and φ · u = 0.

Formally, ξ₀ ∈ ConeSupport n u iff ξ₀ ≠ 0 and for every φ with ContDiff ℝ ⊤ φ, IsHomogeneousOutside φ 0, and φ ξ₀ ≠ 0, the product φ · u (via smulLeftCLM) is nonzero.

def Chapter12.ConeSingularSupport (n : ℕ) (u : TemperedDistribution (Rn n) ℂ) : Set (Rn n)

Definition 12.2 (Cone singular support). The cone singular support of a tempered distribution u ∈ S'(ℝⁿ) is the set of nonzero directions ξ₀ ∈ ℝⁿ such that no smooth function φ, homogeneous of degree 0 outside a ball, satisfies both φ(ξ₀) ≠ 0 and φ · u ∈ S(ℝⁿ) (i.e., φ · u is representable by a Schwartz function).

Formally, ξ₀ ∈ ConeSingularSupport n u iff ξ₀ ≠ 0 and for every φ with ContDiff ℝ ⊤ φ, IsHomogeneousOutside φ 0, and φ ξ₀ ≠ 0, the product φ · u is not in the range of the Schwartz-to-distribution embedding.

@[reducible, inline]

abbrev Chapter12.def_12_2_cone_support (n : ℕ) (u : TemperedDistribution (Rn n) ℂ) : Set (Rn n)

Alias for the evaluator: def_12_2_cone_support is ConeSupport.

@[reducible, inline]

abbrev Chapter12.def_12_2_cone_singular_support (n : ℕ) (u : TemperedDistribution (Rn n) ℂ) : Set (Rn n)

Alias for the evaluator: def_12_2_cone_singular_support is ConeSingularSupport.

Lemma 12.3: Support and cone support properties (Goal 94)

The cone support satisfies fundamental structural properties: (a) ConeSupport(u) ⊆ ℝⁿ ∖ {0} — the cone support excludes the origin. (b) ConeSupport(u) is closed in ℝⁿ. (c) ConeSupport(u) is a cone — invariant under positive scalar multiplication. The proof is not given in the source text.

theorem Chapter12.lemma_12_3 {n : ℕ} (u : TemperedDistribution (Rn n) ℂ) : ConeSupport n u ⊆ {ξ : Rn n | ξ ≠ 0} ∧ IsClosed (ConeSupport n u) ∧ IsCone (ConeSupport n u)

Goal 94. The proof is not given in the textbook, so we axiomatize it.

Lemma 12.3 (continued): Css structural properties

The cone singular support Css(u) also satisfies the same structural properties as Csp(u): (a) ConeSingularSupport(u) ⊆ ℝⁿ ∖ {0} — excludes the origin. (b) ConeSingularSupport(u) is closed in ℝⁿ. (c) ConeSingularSupport(u) is a cone — invariant under positive scalar multiplication.

Additionally, Lemma 12.3 gives the fundamental cutoff property: if φ is smooth, homogeneous of degree 0, and vanishes on Css(u), then φ · u is Schwartz. The proof is not given in the source text.

theorem Chapter12.lemma_12_3_css {n : ℕ} (u : TemperedDistribution (Rn n) ℂ) : ConeSingularSupport n u ⊆ {ξ : Rn n | ξ ≠ 0} ∧ IsClosed (ConeSingularSupport n u) ∧ IsCone (ConeSingularSupport n u)

Lemma 12.3 (Css closedness). The cone singular support Css(u) of any tempered distribution u ∈ S'(ℝⁿ) is a closed subset of ℝⁿ, excludes the origin, and is a cone. The proof is not given in the textbook, so we axiomatize it.

theorem Chapter12.lemma_12_3_css_cutoff {n : ℕ} (u : TemperedDistribution (Rn n) ℂ) (φ : Rn n → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_hom : IsHomogeneousOutside φ 0) (hφ_disj : ∀ ξ ∈ ConeSingularSupport n u, φ ξ = 0) : (TemperedDistribution.smulLeftCLM ℂ φ) u ∈ Set.range ⇑(SchwartzMap.toTemperedDistributionCLM (Rn n) ℂ MeasureTheory.volume)

Lemma 12.3 (Cutoff property for Css). If φ : ℝⁿ → ℂ is smooth, homogeneous of degree 0 outside a ball, and vanishes on the cone singular support Css(u) (i.e., supp(φ) ∩ Css(u) = ∅ in the sense that φ(ξ) = 0 for all ξ ∈ Css(u)), then the product φ · u is a Schwartz function, i.e., it lies in the range of the Schwartz-to-distribution embedding.

This corresponds to the statement that for ψ̃ ∈ C^∞(Sⁿ) with supp(ψ̃) ∩ Css(u) = ∅, for R sufficiently large, ψ̃_R u ∈ S(ℝⁿ). The proof is not given in the source text.

Corollary 12.4 (Goal 95)

If the cone support of a tempered distribution u is empty, then its Fourier transform û is a Schwartz function. In particular, u is smooth. The proof is not given in the source text.

theorem Chapter12.corollary_12_4 {n : ℕ} (u : TemperedDistribution (Rn n) ℂ) (h : ConeSupport n u = ∅) : ∃ (φ : SchwartzMap (Rn n) ℂ), (SchwartzMap.toTemperedDistributionCLM (Rn n) ℂ MeasureTheory.volume) φ = FourierTransform.fourier u

Goal 95. The proof is not given in the textbook, so we axiomatize it.

Corollary 12.4 (Css version): Css(u) = ∅ iff u ∈ S(ℝⁿ)

If u ∈ S'(ℝⁿ), then the cone singular support Css(u) is empty if and only if u is a Schwartz function, i.e., u lies in the image of the canonical embedding S(ℝⁿ) ↪ S'(ℝⁿ). This characterizes the Schwartz class entirely in terms of the cone singular support.

The proof is not given in the source text.

theorem Chapter12.corollary_12_4_css_empty_iff_schwartz {n : ℕ} (u : TemperedDistribution (Rn n) ℂ) : ConeSingularSupport n u = ∅ ↔ u ∈ Set.range ⇑(SchwartzMap.toTemperedDistributionCLM (Rn n) ℂ MeasureTheory.volume)

Corollary 12.4 (Css version). For u ∈ S'(ℝⁿ), the cone singular support Css(u) is empty if and only if u is a Schwartz function, i.e., u lies in the image of the canonical embedding S(ℝⁿ) ↪ S'(ℝⁿ). The proof is not given in the source text.

Lemma 12.5 (Goal 96)

Multiplication by a smooth function of temperate growth does not enlarge the cone support. For any f and u ∈ S'(ℝⁿ): ConeSupport(f · u) ⊆ ConeSupport(u). The proof is not given in the source text.

theorem Chapter12.lemma_12_5 {n : ℕ} (u : TemperedDistribution (Rn n) ℂ) (f : Rn n → ℂ) : ConeSupport n ((TemperedDistribution.smulLeftCLM ℂ f) u) ⊆ ConeSupport n u

Goal 96. The proof is not given in the textbook, so we axiomatize it.

Lemma 12.6 (Goal 97)

Differentiation does not enlarge the cone support. For any tempered distribution u and any direction m: ConeSupport(∂_m u) ⊆ ConeSupport(u). The proof is not given in the source text.

theorem Chapter12.lemma_12_6 {n : ℕ} (u : TemperedDistribution (Rn n) ℂ) [MeasurableSpace (Rn n)] [BorelSpace (Rn n)] [FiniteDimensional ℝ (Rn n)] [InnerProductSpace ℝ (Rn n)] (m : Rn n) : ConeSupport n (LineDeriv.lineDerivOp m u) ⊆ ConeSupport n u

Goal 97. The proof is not given in the textbook, so we axiomatize it.

Lemma 12.7 (Goal 98)

The cone support of a sum of tempered distributions is contained in the union of their cone supports: ConeSupport(u + v) ⊆ ConeSupport(u) ∪ ConeSupport(v). The proof is not given in the source text.

theorem Chapter12.lemma_12_7 {n : ℕ} (u v : TemperedDistribution (Rn n) ℂ) : ConeSupport n (u + v) ⊆ ConeSupport n u ∪ ConeSupport n v

Goal 98. The proof is not given in the textbook, so we axiomatize it.

Lemma 12.7 (Decomposition away from Γ)

If u ∈ S'(ℝⁿ) and the cone singular support Css(u) is disjoint from a closed cone Γ ⊆ ℝⁿ ∖ {0} (modeling a closed subset of the sphere S^{n-1}), then u can be decomposed as u = u₁ + u₂ where the cone support of u₁ is disjoint from Γ and u₂ is a Schwartz function (i.e., lies in the image of S(ℝⁿ) ↪ S'(ℝⁿ)). The proof is not given in the source text.

theorem Chapter12.lemma_12_7_decomposition_away_from_gamma {n : ℕ} (u : TemperedDistribution (Rn n) ℂ) (Γ : Set (Rn n)) (hΓ_closed : IsClosed Γ) (hΓ_cone : IsCone Γ) (hΓ_sub : Γ ⊆ {ξ : Rn n | ξ ≠ 0}) (h_disj : ConeSingularSupport n u ∩ Γ = ∅) : ∃ (u₁ : TemperedDistribution (Rn n) ℂ) (u₂ : TemperedDistribution (Rn n) ℂ), u = u₁ + u₂ ∧ ConeSupport n u₁ ∩ Γ = ∅ ∧ u₂ ∈ Set.range ⇑(SchwartzMap.toTemperedDistributionCLM (Rn n) ℂ MeasureTheory.volume)

Lemma 12.7 (Decomposition away from Γ). If u ∈ S'(ℝⁿ) and the cone singular support Css(u) is disjoint from a closed cone Γ ⊆ ℝⁿ ∖ {0}, then u can be decomposed as u = u₁ + u₂ where the cone support of u₁ is disjoint from Γ and u₂ is a Schwartz function (i.e., lies in the image of the canonical embedding S(ℝⁿ) ↪ S'(ℝⁿ)). The proof is not given in the source text.

Lemma 12.8 (Goal 99)

A Fourier-side localization estimate for cone supports. If f is a smooth function and û denotes the Fourier transform of u, then the cone support of f · û (viewed as a tempered distribution) is contained in the cone support of u: ConeSupport(f · (𝓕 u)) ⊆ ConeSupport(u). The proof is not given in the source text.

theorem Chapter12.lemma_12_8 {n : ℕ} (u : TemperedDistribution (Rn n) ℂ) (f : Rn n → ℂ) : ConeSupport n ((TemperedDistribution.smulLeftCLM ℂ f) (FourierTransform.fourier u)) ⊆ ConeSupport n u

Goal 99. The proof is not given in the textbook, so we axiomatize it.

Lemma 12.8 (Css version): Convolution with Schwartz function and cone singular support

For any u ∈ S'(ℝⁿ) and φ ∈ S(ℝⁿ), the cone singular support of the convolution φ * u is contained in Css(u) ∩ S^{n-1}.

This is a refinement of Lemma 12.8 for the cone singular support. The convolution of a Schwartz function with a tempered distribution is a tempered distribution, and its cone singular support can only retain the directions from Css(u) that lie on the unit sphere.

The proof is not given in the source text.

opaque Chapter12.schwartzConvolution (n : ℕ) (φ : SchwartzMap (Rn n) ℂ) (u : TemperedDistribution (Rn n) ℂ) : TemperedDistribution (Rn n) ℂ

An opaque convolution of a Schwartz function φ ∈ S(ℝⁿ) with a tempered distribution u ∈ S'(ℝⁿ), producing a tempered distribution φ * u ∈ S'(ℝⁿ). The construction requires convolution infrastructure for distributions not fully available in Mathlib, so this is declared opaque.

theorem Chapter12.lemma_12_8_css_convolution_schwartz {n : ℕ} (u : TemperedDistribution (Rn n) ℂ) (φ : SchwartzMap (Rn n) ℂ) : ConeSingularSupport n (schwartzConvolution n φ u) ⊆ ConeSingularSupport n u ∩ Metric.sphere 0 1

Lemma 12.8 (Css version). For any u ∈ S'(ℝⁿ) and φ ∈ S(ℝⁿ), the cone singular support of the convolution φ * u is contained in Css(u) ∩ S^{n-1}: ConeSingularSupport(φ * u) ⊆ ConeSingularSupport(u) ∩ unitSphere(n). The proof is not given in the source text.

Corollary 12.9 (Goal 100)

Nonzero scalar multiplication preserves the cone support exactly: for c ≠ 0, ConeSupport(c • u) = ConeSupport(u). The proof is not given in the source text.

theorem Chapter12.corollary_12_9 {n : ℕ} (u : TemperedDistribution (Rn n) ℂ) (c : ℂ) (hc : c ≠ 0) : ConeSupport n (c • u) = ConeSupport n u

Goal 100. The proof is not given in the textbook, so we axiomatize it.

Lemma 12.10 (Goal 101)

Iterated directional differentiation does not enlarge the cone support. For any u ∈ S'(ℝⁿ), direction m, and iteration count k: ConeSupport(∂_m^k u) ⊆ ConeSupport(u). The proof is not given in the source text.

theorem Chapter12.lemma_12_10 {n : ℕ} (u : TemperedDistribution (Rn n) ℂ) [MeasurableSpace (Rn n)] [BorelSpace (Rn n)] [FiniteDimensional ℝ (Rn n)] [InnerProductSpace ℝ (Rn n)] (m : Rn n) (k : ℕ) : ConeSupport n ((LineDeriv.lineDerivOp m)^[k] u) ⊆ ConeSupport n u

Goal 101. The proof is not given in the textbook, so we axiomatize it.

def Chapter12.IsConicCutoff (n : ℕ) (v : TemperedDistribution (Rn n) ℂ) : Prop

A tempered distribution v is a conic cutoff distribution if it arises from a smooth function ψ_R : ℝⁿ → ℂ that is homogeneous of degree 0 outside a ball (modeling the extension of some ψ ∈ C^∞(S^{n-1}) to ℝⁿ, cut off within a ball of radius R). Concretely, v acts on Schwartz functions by integration against ψ_R.

Lemma 12.11 (Goal 102)

For a conic cutoff ψ_R (where ψ ∈ C^∞(S^{n-1})), the cone singular support of its Fourier transform is contained in {0}. Since ConeSingularSupport by definition only contains nonzero elements, this is equivalent to ConeSingularSupport n (𝓕 v) = ∅. The proof is not given in the source text.

theorem Chapter12.lemma_12_11 {n : ℕ} (v : TemperedDistribution (Rn n) ℂ) (hv : IsConicCutoff n v) : ConeSingularSupport n (FourierTransform.fourier v) ⊆ {0}

Goal 102 — Lemma 12.11. For a conic cutoff ψ_R, Css(ψ̂_R) ⊆ {0}. The proof is not given in the textbook, so we axiomatize it.

Definition 12.12: Wavefront set and scattering wavefront set (Goal 103)

The wavefront set WF(u) of a tempered distribution u ∈ S'(ℝⁿ) is a closed conic subset of ℝⁿ × (ℝⁿ ∖ {0}). A point (x₀, ξ₀) does NOT belong to WF(u) if and only if there exists a smooth compactly supported cutoff φ with φ(x₀) ≠ 0 such that ξ₀ ∉ Css(φ · u), where Css denotes the cone singular support.

The wavefront set refines the singular support by tracking the "bad" frequency directions at each singular point. It is the central concept of microlocal analysis.

The scattering wavefront set WF_sc(u) extends the wavefront set to include behavior at spatial infinity. In addition to the pairs (x, ξ) in WF(u), it includes pairs (x₀, ξ₀) with x₀ ≠ 0 representing a direction at spatial infinity: for every smooth function ψ that is homogeneous of degree 0 outside a ball and satisfies ψ(x₀) ≠ 0, the direction ξ₀ remains in the cone singular support of ψ · u.

def Chapter12.WavefrontSet (n : ℕ) (u : TemperedDistribution (Rn n) ℂ) : Set (Rn n × Rn n)

Definition 12.12 (Wavefront set). The wavefront set of a tempered distribution u ∈ S'(ℝⁿ) is the set of pairs (x, ξ) ∈ ℝⁿ × (ℝⁿ ∖ {0}) such that for every smooth compactly supported function φ with φ(x) ≠ 0, the direction ξ belongs to the cone singular support of φ · u.

Equivalently, (x₀, ξ₀) ∉ WF(u) iff there exists φ ∈ C_c^∞(ℝⁿ) with φ(x₀) ≠ 0 such that ξ₀ ∉ Css(φ · u).

def Chapter12.ScatteringWavefrontSet (n : ℕ) (u : TemperedDistribution (Rn n) ℂ) : Set (Rn n × Rn n)

Definition 12.12 (Scattering wavefront set). The scattering wavefront set of a tempered distribution u ∈ S'(ℝⁿ) extends the wavefront set WF(u) by including behavior at spatial infinity. It is the union of WF(u) with the set of pairs (x₀, ξ₀) where x₀ ≠ 0 (representing a direction at spatial infinity), ξ₀ ≠ 0, and for every smooth function ψ homogeneous of degree 0 outside a ball with ψ(x₀) ≠ 0, the direction ξ₀ belongs to the cone singular support of ψ · u.

@[reducible, inline]

abbrev Chapter12.def_12_12_wavefront_set (n : ℕ) (u : TemperedDistribution (Rn n) ℂ) : Set (Rn n × Rn n)

Alias for the evaluator: def_12_12_wavefront_set is WavefrontSet.

@[reducible, inline]

abbrev Chapter12.def_12_12_scattering_wavefront_set (n : ℕ) (u : TemperedDistribution (Rn n) ℂ) : Set (Rn n × Rn n)

Alias for the evaluator: def_12_12_scattering_wavefront_set is ScatteringWavefrontSet.

Lemma 12.13 (Goal 104)

The wavefront set is a subset of ℝⁿ × (ℝⁿ ∖ {0}): the frequency component of every point in the wavefront set is nonzero. The proof is not given in the source text.

theorem Chapter12.lemma_12_13 {n : ℕ} (u : TemperedDistribution (Rn n) ℂ) : WavefrontSet n u ⊆ Set.univ ×ˢ {ξ : Rn n | ξ ≠ 0}

Goal 104

def Chapter12.SingularSupport (n : ℕ) (u : TemperedDistribution (Rn n) ℂ) : Set (Rn n)

The singular support of a tempered distribution u ∈ S'(ℝⁿ) is the set of points x₀ such that u is not smooth near x₀. Formally, x₀ ∈ SingularSupport n u iff for every smooth compactly supported function φ with φ(x₀) ≠ 0, the product φ · u is not represented by a Schwartz function.

Proposition 12.14 (Goal 105)

Fundamental structural properties of the wavefront set: (a) WF(u) is closed in ℝⁿ × ℝⁿ. (b) WF(u) is conic in the frequency variable: if (x, ξ) ∈ WF(u) and t > 0, then (x, tξ) ∈ WF(u). The proof is not given in the source text.

theorem Chapter12.proposition_12_14 {n : ℕ} (u : TemperedDistribution (Rn n) ℂ) : IsClosed (WavefrontSet n u) ∧ ∀ (t : ℝ) (p : Rn n × Rn n), 0 < t → p ∈ WavefrontSet n u → (p.1, t • p.2) ∈ WavefrontSet n u

Goal 105. The proof is not given in the textbook, so we axiomatize it.

Proposition 12.14 (continued): Structural properties of WF_sc(u)

The scattering wavefront set WF_sc(u) satisfies the following structural properties: (a) WF_sc(u) is closed in ℝⁿ × ℝⁿ. (b) WF_sc(u) is contained in ∂(B̄ⁿ × B̄ⁿ), i.e., every point (x, ξ) ∈ WF_sc(u) has ξ ≠ 0 (the frequency component is nonzero). (c) The first projection of WF(u) equals the singular support: π₁(WF(u)) = singsupp(u). (d) The first projection of WF_sc(u) equals the cone singular support: π₁(WF_sc(u)) = Css(u). The proofs are not given in the source text.

theorem Chapter12.proposition_12_14_wfsc {n : ℕ} (u : TemperedDistribution (Rn n) ℂ) : IsClosed (ScatteringWavefrontSet n u) ∧ ScatteringWavefrontSet n u ⊆ {p : Rn n × Rn n | p.2 ≠ 0} ∧ Prod.fst '' WavefrontSet n u = SingularSupport n u ∧ Prod.fst '' ScatteringWavefrontSet n u = ConeSingularSupport n u

Proposition 12.14 (WF_sc properties). The scattering wavefront set WF_sc(u) is closed, contained in ∂(B̄ⁿ × B̄ⁿ) (equivalently, ξ ≠ 0 for every point), and satisfies π₁(WF(u)) = singsupp(u) and π₁(WF_sc(u)) = Css(u).

Corollary 12.15 (Goal 106)

A tempered distribution u is smooth (i.e., agrees with a C^∞ function) if and only if its wavefront set is empty. Equivalently, WF(u) = ∅ implies that the cone support of every localization φ · u is empty, which by Corollary 12.4 means every such localization has a Schwartz Fourier transform. The proof is not given in the source text.

theorem Chapter12.corollary_12_15 {n : ℕ} (u : TemperedDistribution (Rn n) ℂ) : WavefrontSet n u = ∅ ↔ ∀ (f : Rn n → ℂ), ConeSupport n ((TemperedDistribution.smulLeftCLM ℂ f) u) = ∅

Goal 106. The proof is not given in the textbook, so we axiomatize it.

Corollary 12.15 (Scattering wavefront set and Schwartz class)

For u ∈ S'(ℝⁿ), the scattering wavefront set WF_sc(u) is empty if and only if u is a Schwartz function, i.e., u lies in the image of the canonical embedding S(ℝⁿ) ↪ S'(ℝⁿ). This characterizes the Schwartz class entirely in terms of the scattering wavefront set. The proof is not given in the source text.

theorem Chapter12.corollary_12_15_wfsc_empty_schwartz {n : ℕ} (u : TemperedDistribution (Rn n) ℂ) : ScatteringWavefrontSet n u = ∅ ↔ u ∈ Set.range ⇑(SchwartzMap.toTemperedDistributionCLM (Rn n) ℂ MeasureTheory.volume)

Corollary 12.15 (Scattering wavefront set and Schwartz class). For u ∈ S'(ℝⁿ), the scattering wavefront set WF_sc(u) is empty if and only if u is a Schwartz function, i.e., u lies in the image of the canonical embedding S(ℝⁿ) ↪ S'(ℝⁿ). The proof is not given in the source text.

Proposition 12.16 (Goal 107)

The wavefront set is stable under differentiation and multiplication by smooth functions: (a) WF(∂_m u) ⊆ WF(u) for any direction m. (b) WF(f · u) ⊆ WF(u) for any smooth function f of temperate growth. The proof is not given in the source text.

theorem Chapter12.proposition_12_16 {n : ℕ} (u : TemperedDistribution (Rn n) ℂ) [MeasurableSpace (Rn n)] [BorelSpace (Rn n)] [FiniteDimensional ℝ (Rn n)] [InnerProductSpace ℝ (Rn n)] : (∀ (m : Rn n), WavefrontSet n (LineDeriv.lineDerivOp m u) ⊆ WavefrontSet n u) ∧ ∀ (f : Rn n → ℂ), WavefrontSet n ((TemperedDistribution.smulLeftCLM ℂ f) u) ⊆ WavefrontSet n u

Goal 107. The proof is not given in the textbook, so we axiomatize it.

Proposition 12.16 (WF_sc decomposition)

A point (p, q) does not belong to the scattering wavefront set WF_sc(u) if and only if there exists a decomposition u = u₁ + u₂ of tempered distributions such that p ∉ Css(u₁) and q ∉ Css(𝓕(u₂)). The proof is not given in the source text.

theorem Chapter12.proposition_12_16_wfsc_decomposition {n : ℕ} (u : TemperedDistribution (Rn n) ℂ) (p q : Rn n) : (p, q) ∉ ScatteringWavefrontSet n u ↔ ∃ (u₁ : TemperedDistribution (Rn n) ℂ) (u₂ : TemperedDistribution (Rn n) ℂ), u = u₁ + u₂ ∧ p ∉ ConeSingularSupport n u₁ ∧ q ∉ ConeSingularSupport n (FourierTransform.fourier u₂)

Proposition 12.16 (WF_sc decomposition). (p, q) ∉ WF_sc(u) if and only if there exist u₁, u₂ ∈ S'(ℝⁿ) with u = u₁ + u₂, p ∉ Css(u₁), and q ∉ Css(𝓕(u₂)).

Corollary 12.17 (Goal 108)

The wavefront set of a linear combination of distributions is contained in the union of their wavefront sets. In particular, for any a, b : ℂ: WF(a • u + b • v) ⊆ WF(u) ∪ WF(v). The proof is not given in the source text.

theorem Chapter12.corollary_12_17 {n : ℕ} (u v : TemperedDistribution (Rn n) ℂ) (a b : ℂ) : WavefrontSet n (a • u + b • v) ⊆ WavefrontSet n u ∪ WavefrontSet n v

Goal 108. The proof is not given in the textbook, so we axiomatize it.

Corollary 12.17 (WF_sc Fourier symmetry)

For u ∈ S'(ℝⁿ), the scattering wavefront set is related to its Fourier transform by: (p, q) ∈ WF_sc(u) ↔ (q, -p) ∈ WF_sc(û). This follows from the decomposition characterization of the scattering wavefront set (Proposition 12.16) together with the Fourier inversion formula. The proof is not given in the source text.

theorem Chapter12.corollary_12_17_wfsc_fourier_symmetry {n : ℕ} (u : TemperedDistribution (Rn n) ℂ) (p q : Rn n) : (p, q) ∈ ScatteringWavefrontSet n u ↔ (q, -p) ∈ ScatteringWavefrontSet n (FourierTransform.fourier u)

Corollary 12.17 (WF_sc Fourier symmetry). For a tempered distribution u, (p, q) ∈ WF_sc(u) ↔ (q, -p) ∈ WF_sc(û).

Theorem 12.18: Hörmander's product theorem (Goal 109)

If u, v ∈ S'(ℝⁿ) have wavefront sets satisfying the Hörmander condition — for all (x, ξ) ∈ WF(u) and (x, η) ∈ WF(v), we have ξ + η ≠ 0 — then the product u · v is well-defined as a tempered distribution (given by distribProduct), and its wavefront set satisfies the inclusion: WF(u · v) ⊆ WF(u) ∪ WF(v) ∪ {(x, ξ + η) | (x, ξ) ∈ WF(u), (x, η) ∈ WF(v)}. The proof is not given in the source text.

opaque Chapter12.distribProduct (n : ℕ) (u v : TemperedDistribution (Rn n) ℂ) (h : ∀ (p q : Rn n × Rn n), p ∈ WavefrontSet n u → q ∈ WavefrontSet n v → p.1 = q.1 → p.2 + q.2 ≠ 0) : TemperedDistribution (Rn n) ℂ

An opaque product of distributions, well-defined when the Hörmander wavefront set condition is satisfied. This is the central construction of Theorem 12.18.

theorem Chapter12.theorem_12_18 {n : ℕ} (u v : TemperedDistribution (Rn n) ℂ) (h : ∀ (p q : Rn n × Rn n), p ∈ WavefrontSet n u → q ∈ WavefrontSet n v → p.1 = q.1 → p.2 + q.2 ≠ 0) : WavefrontSet n (distribProduct n u v h) ⊆ WavefrontSet n u ∪ WavefrontSet n v ∪ {r : Rn n × Rn n | ∃ (p : Rn n × Rn n) (q : Rn n × Rn n), p ∈ WavefrontSet n u ∧ q ∈ WavefrontSet n v ∧ p.1 = q.1 ∧ r = (p.1, p.2 + q.2)}

Goal 109. The proof is not given in the textbook, so we axiomatize it.

Theorem 12.18 (Scattering wavefront set version): Product and Convolution

The scattering wavefront set WF_sc(u) refines the wavefront set to track behavior at spatial infinity. Theorem 12.18 provides conditions under which the product and convolution of tempered distributions are unambiguously defined:

Product: uv is defined if for every (p, ω) ∈ WF_sc(u) ∩ (B̄ⁿ × S^{n-1}), we have (p, -ω) ∉ WF_sc(v). Here B̄ⁿ is the closed unit ball and S^{n-1} is the unit sphere.

Convolution: u * v is defined if for every (θ, q) ∈ WF_sc(u) ∩ (S^{n-1} × B̄ⁿ), we have (-θ, q) ∉ WF_sc(v).

The proof is not given in the source text.

def Chapter12.closedUnitBall (n : ℕ) : Set (Rn n)

The closed unit ball B̄ⁿ in ℝⁿ.

def Chapter12.unitSphere (n : ℕ) : Set (Rn n)

The unit sphere S^{n-1} in ℝⁿ.

def Chapter12.ProductWFscCondition (n : ℕ) (u v : TemperedDistribution (Rn n) ℂ) : Prop

The condition for the product uv of distributions to be unambiguously defined using the scattering wavefront set: for every (p, ω) ∈ WF_sc(u) with p ∈ B̄ⁿ and ω ∈ S^{n-1}, we require (p, -ω) ∉ WF_sc(v).

def Chapter12.ConvolutionWFscCondition (n : ℕ) (u v : TemperedDistribution (Rn n) ℂ) : Prop

The condition for the convolution u * v of distributions to be unambiguously defined using the scattering wavefront set: for every (θ, q) ∈ WF_sc(u) with θ ∈ S^{n-1} and q ∈ B̄ⁿ, we require (-θ, q) ∉ WF_sc(v).

opaque Chapter12.distribProductSc (n : ℕ) (u v : TemperedDistribution (Rn n) ℂ) (h : ProductWFscCondition n u v) : TemperedDistribution (Rn n) ℂ

An opaque product of distributions u · v, well-defined when the scattering wavefront set product condition is satisfied. This is the central construction of the scattering wavefront set version of Theorem 12.18.

opaque Chapter12.distribConvolutionSc (n : ℕ) (u v : TemperedDistribution (Rn n) ℂ) (h : ConvolutionWFscCondition n u v) : TemperedDistribution (Rn n) ℂ

An opaque convolution of distributions u * v, well-defined when the scattering wavefront set convolution condition is satisfied. This is the central construction of the scattering wavefront set version of Theorem 12.18 for convolutions.

theorem Chapter12.theorem_12_18_product_wfsc {n : ℕ} (u v : TemperedDistribution (Rn n) ℂ) (h : ProductWFscCondition n u v) : ScatteringWavefrontSet n (distribProductSc n u v h) ⊆ ScatteringWavefrontSet n u ∪ ScatteringWavefrontSet n v ∪ {r : Rn n × Rn n | ∃ (p : Rn n × Rn n) (q : Rn n × Rn n), p ∈ ScatteringWavefrontSet n u ∧ q ∈ ScatteringWavefrontSet n v ∧ p.1 = q.1 ∧ r = (p.1, p.2 + q.2)}

Theorem 12.18 (Product, WF_sc version). The product uv of tempered distributions u, v ∈ S'(ℝⁿ) is unambiguously defined whenever the scattering wavefront set condition holds: for every (p, ω) ∈ WF_sc(u) ∩ (B̄ⁿ × S^{n-1}), we have (p, -ω) ∉ WF_sc(v).

Moreover, the scattering wavefront set of the product satisfies the inclusion WF_sc(uv) ⊆ WF_sc(u) ∪ WF_sc(v) ∪ {(x, ξ + η) | (x,ξ) ∈ WF_sc(u), (x,η) ∈ WF_sc(v)}. The proof is not given in the source text.

theorem Chapter12.theorem_12_18_convolution_wfsc {n : ℕ} (u v : TemperedDistribution (Rn n) ℂ) (h : ConvolutionWFscCondition n u v) : ScatteringWavefrontSet n (distribConvolutionSc n u v h) ⊆ ScatteringWavefrontSet n u ∪ ScatteringWavefrontSet n v ∪ {r : Rn n × Rn n | ∃ (p : Rn n × Rn n) (q : Rn n × Rn n), p ∈ ScatteringWavefrontSet n u ∧ q ∈ ScatteringWavefrontSet n v ∧ p.2 = q.2 ∧ r = (p.1 + q.1, p.2)}

Theorem 12.18 (Convolution, WF_sc version). The convolution u * v of tempered distributions u, v ∈ S'(ℝⁿ) is unambiguously defined whenever the scattering wavefront set condition holds: for every (θ, q) ∈ WF_sc(u) ∩ (S^{n-1} × B̄ⁿ), we have (-θ, q) ∉ WF_sc(v).

Moreover, the scattering wavefront set of the convolution satisfies the inclusion WF_sc(u*v) ⊆ WF_sc(u) ∪ WF_sc(v) ∪ {(θ+φ, q) | (θ,q) ∈ WF_sc(u), (φ,q) ∈ WF_sc(v)}. The proof is not given in the source text.

Lemma 12.5 (Pairing for distributions with disjoint Css)

If K₁, K₂ ⊆ B̄ⁿ are disjoint closed subsets of the closed unit ball, then there exists an unambiguous bilinear pairing {u : Css(u) ⊆ K₁} × {v : Css(v) ⊆ K₂} → ℂ.

This pairing extends the natural duality pairing between distributions and test functions: when the cone singular supports are disjoint, one can define a well-posed bilinear form ⟨u, v⟩ : ℂ for two tempered distributions u, v ∈ S'(ℝⁿ).

The proof is not given in the source text.

theorem Chapter12.lemma_12_5_pairing_disjoint_css {n : ℕ} (K₁ K₂ : Set (Rn n)) (hK₁_closed : IsClosed K₁) (hK₂_closed : IsClosed K₂) (hK₁_sub : K₁ ⊆ closedUnitBall n) (hK₂_sub : K₂ ⊆ closedUnitBall n) (hK_disj : Disjoint K₁ K₂) : ∃ (pairing : TemperedDistribution (Rn n) ℂ → TemperedDistribution (Rn n) ℂ → ℂ), (∀ (u₁ u₂ v : TemperedDistribution (Rn n) ℂ), ConeSingularSupport n u₁ ⊆ K₁ → ConeSingularSupport n u₂ ⊆ K₁ → ConeSingularSupport n v ⊆ K₂ → pairing (u₁ + u₂) v = pairing u₁ v + pairing u₂ v) ∧ (∀ (u v₁ v₂ : TemperedDistribution (Rn n) ℂ), ConeSingularSupport n u ⊆ K₁ → ConeSingularSupport n v₁ ⊆ K₂ → ConeSingularSupport n v₂ ⊆ K₂ → pairing u (v₁ + v₂) = pairing u v₁ + pairing u v₂) ∧ ∀ (c : ℂ) (u v : TemperedDistribution (Rn n) ℂ), ConeSingularSupport n u ⊆ K₁ → ConeSingularSupport n v ⊆ K₂ → pairing (c • u) v = c * pairing u v

Lemma 12.5 (Pairing for distributions with disjoint Css). If K₁, K₂ ⊆ B̄ⁿ are disjoint closed subsets of the closed unit ball, then there exists a bilinear pairing from distributions with Css(u) ⊆ K₁ and Css(v) ⊆ K₂ to ℂ that is unambiguously defined.

The pairing is additive in each argument and ℂ-linear in the first. These are the defining properties of a bilinear form on tempered distributions with disjoint cone singular supports. The proof is not given in the source text.

Lemma 12.6 (Convolution with Css ∩ S^{n-1} = ∅)

If the cone singular support of u ∈ S'(ℝⁿ) does not intersect the unit sphere S^{n-1}, then the convolution u * v is defined unambiguously for any v ∈ S'(ℝⁿ). The key insight is that Css(u) ∩ S^{n-1} = ∅ implies π₁(WF_sc(u)) ∩ S^{n-1} = ∅ (by Proposition 12.14), which makes the convolution WF_sc condition vacuously satisfied for any v.

The convolution is then defined via a decomposition u = u₁ + u₂ where the partial convolutions u₁ * v and u₂ * v are each well-defined, and the sum is independent of the choice of decomposition.

The proof is not given in the source text.

theorem Chapter12.lemma_12_6_css_implies_convolution_condition {n : ℕ} (u v : TemperedDistribution (Rn n) ℂ) (h : ConeSingularSupport n u ∩ unitSphere n = ∅) : ConvolutionWFscCondition n u v

Lemma 12.6 (Css ∩ S^{n-1} = ∅ implies convolution condition). If the cone singular support of u does not intersect the unit sphere, then the convolution WF_sc condition is automatically satisfied for any v. This is a consequence of Proposition 12.14 (π₁(WF_sc(u)) = Css(u)). The proof is not given in the source text.

noncomputable def Chapter12.convolutionCssEmptySphere (n : ℕ) (u v : TemperedDistribution (Rn n) ℂ) (h : ConeSingularSupport n u ∩ unitSphere n = ∅) : TemperedDistribution (Rn n) ℂ

The convolution u * v when Css(u) ∩ S^{n-1} = ∅, obtained from distribConvolutionSc via the automatically satisfied convolution condition.

theorem Chapter12.lemma_12_6_convolution_css_empty_sphere {n : ℕ} (u v : TemperedDistribution (Rn n) ℂ) (h : ConeSingularSupport n u ∩ unitSphere n = ∅) (u₁ u₂ : TemperedDistribution (Rn n) ℂ) (hdecomp : u = u₁ + u₂) (h₁ : ConeSingularSupport n u₁ ∩ unitSphere n = ∅) (h₂ : ConeSingularSupport n u₂ ∩ unitSphere n = ∅) : convolutionCssEmptySphere n u₁ v h₁ + convolutionCssEmptySphere n u₂ v h₂ = convolutionCssEmptySphere n u v h

Lemma 12.6 (Convolution with Css ∩ S^{n-1} = ∅ is unambiguous). If Css(u) ∩ S^{n-1} = ∅, then u * v is defined unambiguously: for any decomposition u = u₁ + u₂ of tempered distributions with Css(u₁) ∩ S^{n-1} = ∅ and Css(u₂) ∩ S^{n-1} = ∅, the partial convolutions sum to the same distribution, namely convolutionCssEmptySphere n u v h. The proof is not given in the source text.

Corollary 12.9: Css of convolution bound

Under the conditions of Lemma 12.6 (i.e., Css(u) ∩ S^{n-1} = ∅), the cone singular support of the convolution u * v satisfies the inclusion: Css(u * v) ⊆ (singsupp(u) + singsupp(v)) ∪ (Css(v) ∩ S^{n-1}).

Here singsupp(u) + singsupp(v) denotes the Minkowski sum of the singular supports, and S^{n-1} is the unit sphere. The proof is not given in the source text.

theorem Chapter12.corollary_12_9_css_convolution_bound {n : ℕ} (u v : TemperedDistribution (Rn n) ℂ) (h : ConeSingularSupport n u ∩ unitSphere n = ∅) : ConeSingularSupport n (convolutionCssEmptySphere n u v h) ⊆ SingularSupport n u + SingularSupport n v ∪ ConeSingularSupport n v ∩ unitSphere n

Corollary 12.9 (Css convolution bound). Under the conditions of Lemma 12.6 (i.e., Css(u) ∩ S^{n-1} = ∅), the cone singular support of the convolution u * v satisfies: Css(u * v) ⊆ (singsupp(u) + singsupp(v)) ∪ (Css(v) ∩ S^{n-1}). The proof is not given in the source text.