Atlas.DifferentialAnalysis.code.WavefrontDiffOps

source

theorem WavefrontDiffOps.not_mem_wavefrontSet_of_isSmoothNear {n : ℕ} (u : TemperedDistribution (ConeSupport.E n) ℂ) (x : ConeSupport.E n) (ω : ↑(ConeSupport.Sphere n)) (hsmooth : ConeSupport.IsSmoothNear u x) :

(x, ω) ∉ ConeSupport.wavefrontSet u

If a tempered distribution u is smooth near a point x, then the pair (x, ω) is not in the wavefront set of u for any direction ω.

source

theorem WavefrontDiffOps.singularSupport_fourier_compactCutoff_empty {n : ℕ} (u : TemperedDistribution (ConeSupport.E n) ℂ) (φ : ConeSupport.E n → ℂ) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) :

ConeSupport.singularSupport (FourierTransform.fourier ((TemperedDistribution.smulLeftCLM ℂ φ) u)) = ∅

The singular support of the Fourier transform of a compactly cut-off tempered distribution φ · u is empty: the result is smooth everywhere.

source

theorem WavefrontDiffOps.cssSphere_empty_compactCutoff_isSchwartz {n : ℕ} (u : TemperedDistribution (ConeSupport.E n) ℂ) (φ : ConeSupport.E n → ℂ) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (hcss : ConeSupport.ConicSingularSupportSphere (FourierTransform.fourier ((TemperedDistribution.smulLeftCLM ℂ φ) u)) = ∅) :

∃ (f : SchwartzMap (ConeSupport.E n) ℂ), (TemperedDistribution.smulLeftCLM ℂ φ) u = (SchwartzMap.toTemperedDistributionCLM (ConeSupport.E n) ℂ MeasureTheory.volume) f

If the conic singular support sphere of 𝓕(φ · u) is empty and φ is a smooth compactly supported cutoff, then φ · u is itself a Schwartz function.

source

theorem WavefrontDiffOps.exists_smooth_compactly_supported_in_open {n : ℕ} (U : Set (ConeSupport.E n)) (hU : IsOpen U) (x : ConeSupport.E n) (hx : x ∈ U) :

∃ (φ : ConeSupport.E n → ℂ), ContDiff ℝ (↑⊤) φ ∧ HasCompactSupport φ ∧ φ x ≠ 0 ∧ tsupport φ ⊆ U

For any open set U and point x ∈ U, there exists a smooth compactly supported complex bump function φ with φ x ≠ 0 and tsupport φ ⊆ U.

source

theorem WavefrontDiffOps.isSmoothNear_of_forall_not_mem_wavefrontSet {n : ℕ} (u : TemperedDistribution (ConeSupport.E n) ℂ) (x : ConeSupport.E n) (h : ∀ (ω : ↑(ConeSupport.Sphere n)), (x, ω) ∉ ConeSupport.wavefrontSet u) :

ConeSupport.IsSmoothNear u x

Converse to not_mem_wavefrontSet_of_isSmoothNear: if no direction (x, ω) belongs to the wavefront set of u, then u is smooth near x. Uses compactness of the sphere of directions.

source

theorem WavefrontDiffOps.wavefrontSet_proj_fst_subset_singularSupport {n : ℕ} (u : TemperedDistribution (ConeSupport.E n) ℂ) :

Prod.fst '' ConeSupport.wavefrontSet u ⊆ ConeSupport.singularSupport u

The projection to the base of the wavefront set is contained in the singular support.

source

theorem WavefrontDiffOps.singularSupport_subset_wavefrontSet_proj_fst {n : ℕ} (u : TemperedDistribution (ConeSupport.E n) ℂ) :

ConeSupport.singularSupport u ⊆ Prod.fst '' ConeSupport.wavefrontSet u

The singular support is contained in the projection to the base of the wavefront set.

source

theorem WavefrontDiffOps.wavefrontSet_proj_fst_eq_singularSupport {n : ℕ} (u : TemperedDistribution (ConeSupport.E n) ℂ) :

Prod.fst '' ConeSupport.wavefrontSet u = ConeSupport.singularSupport u

The projection to the base of the wavefront set equals the singular support.

source

def WavefrontDiffOps.boundaryOfProd {n : ℕ} :

Set ((ConeSupport.E n ⊕ ↑(ConeSupport.Sphere n)) × (ConeSupport.E n ⊕ ↑(ConeSupport.Sphere n)))

The "boundary" subset of pairs (p, q) where at least one of the components corresponds to a direction at infinity (an Sum.inr of Sphere n).

Instances For

source

theorem WavefrontDiffOps.scatteringWavefrontSet_subset_boundary {n : ℕ} (u : TemperedDistribution (ConeSupport.E n) ℂ) :

ConeSupport.scatteringWavefrontSet u ⊆ boundaryOfProd

The scattering wavefront set is always contained in the boundary subset boundaryOfProd.

source

theorem WavefrontDiffOps.wavefrontSet_isClosed {n : ℕ} (u : TemperedDistribution (ConeSupport.E n) ℂ) :

IsClosed (ConeSupport.wavefrontSet u)

The wavefront set of a tempered distribution is a closed subset of E n × Sphere n.

source

theorem WavefrontDiffOps.singularSupport_isClosed {n : ℕ} (u : TemperedDistribution (ConeSupport.E n) ℂ) :

IsClosed (ConeSupport.singularSupport u)

The singular support of a tempered distribution is closed in E n.

source

theorem WavefrontDiffOps.coneSingularSupport_isClosed {n : ℕ} (u : TemperedDistribution (ConeSupport.E n) ℂ) :

IsClosed (ConeSupport.coneSingularSupport u)

The cone singular support of a tempered distribution is closed in E n ⊕ Sphere n.

source

theorem WavefrontDiffOps.isConicCutoffNear_isOpen {n : ℕ} (g : ConeSupport.E n → ℂ) :

IsOpen {ω : ↑(ConeSupport.Sphere n) | ConeSupport.IsConicCutoffNear g ω}

The set of sphere directions ω for which g is a conic cutoff near ω is open.

source

theorem WavefrontDiffOps.scatteringWavefrontSetAtInfinity_isClosed {n : ℕ} (u : TemperedDistribution (ConeSupport.E n) ℂ) :

IsClosed (ConeSupport.scatteringWavefrontSetAtInfinity u)

The scattering wavefront set at infinity is a closed subset of Sphere n × (E n ⊕ Sphere n).

source

theorem WavefrontDiffOps.scatteringWavefrontSet_isClosed {n : ℕ} (u : TemperedDistribution (ConeSupport.E n) ℂ) :

IsClosed (ConeSupport.scatteringWavefrontSet u)

The full scattering wavefront set (union of finite-part and at-infinity components) is closed.

source

theorem WavefrontDiffOps.not_mem_scatteringWavefrontSet_of_not_mem_coneSingularSupport {n : ℕ} (u : TemperedDistribution (ConeSupport.E n) ℂ) (p q : ConeSupport.E n ⊕ ↑(ConeSupport.Sphere n)) (hp : p ∉ ConeSupport.coneSingularSupport u) :

(p, q) ∉ ConeSupport.scatteringWavefrontSet u

If the first projection p is outside the cone singular support, then no pair (p, q) belongs to the scattering wavefront set.

source

theorem WavefrontDiffOps.singularSupport_fourier_conicCutoff_smul_empty {n : ℕ} (u : TemperedDistribution (ConeSupport.E n) ℂ) (g : ConeSupport.E n → ℂ) (ω : ↑(ConeSupport.Sphere n)) (hg : ConeSupport.IsConicCutoffNear g ω) :

ConeSupport.singularSupport (FourierTransform.fourier ((TemperedDistribution.smulLeftCLM ℂ g) u)) = ∅

If g is a conic cutoff near ω, then the singular support of 𝓕(g · u) is empty: it is smooth everywhere as the Fourier transform of a conically localized distribution.

source

theorem WavefrontDiffOps.isSchwartz_of_fourier_isSchwartz {n : ℕ} (v : TemperedDistribution (ConeSupport.E n) ℂ) (hv : ∃ (f : SchwartzMap (ConeSupport.E n) ℂ), FourierTransform.fourier v = (SchwartzMap.toTemperedDistributionCLM (ConeSupport.E n) ℂ MeasureTheory.volume) f) :

∃ (f : SchwartzMap (ConeSupport.E n) ℂ), v = (SchwartzMap.toTemperedDistributionCLM (ConeSupport.E n) ℂ MeasureTheory.volume) f

A tempered distribution is itself given by a Schwartz function whenever its Fourier transform is.

source

theorem WavefrontDiffOps.cssSphere_empty_conicCutoff_isSchwartz {n : ℕ} (u : TemperedDistribution (ConeSupport.E n) ℂ) (g : ConeSupport.E n → ℂ) (ω : ↑(ConeSupport.Sphere n)) (hg : ConeSupport.IsConicCutoffNear g ω) (hcss : ConeSupport.ConicSingularSupportSphere (FourierTransform.fourier ((TemperedDistribution.smulLeftCLM ℂ g) u)) = ∅) :

∃ (f : SchwartzMap (ConeSupport.E n) ℂ), (TemperedDistribution.smulLeftCLM ℂ g) u = (SchwartzMap.toTemperedDistributionCLM (ConeSupport.E n) ℂ MeasureTheory.volume) f

If g is a conic cutoff near ω and the conic singular support sphere of 𝓕(g · u) is empty, then g · u is given by a Schwartz function.

source

theorem WavefrontDiffOps.exists_conic_cutoff_near_in_open {n : ℕ} (ω : ↑(ConeSupport.Sphere n)) (U : Set (ConeSupport.E n)) (hU : IsOpen U) (hω : ↑ω ∈ U) :

∃ (g : ConeSupport.E n → ℂ), ConeSupport.IsConicCutoffNear g ω ∧ Function.support g ⊆ U

For any direction ω and open neighbourhood U of ω, there exists a function g that is a conic cutoff near ω whose support is contained in U.

source

theorem WavefrontDiffOps.not_mem_coneSingularSupport_of_forall_not_mem_scatteringWavefrontSet {n : ℕ} (u : TemperedDistribution (ConeSupport.E n) ℂ) (p : ConeSupport.E n ⊕ ↑(ConeSupport.Sphere n)) (h : ∀ (q : ConeSupport.E n ⊕ ↑(ConeSupport.Sphere n)), (p, q) ∉ ConeSupport.scatteringWavefrontSet u) :

p ∉ ConeSupport.coneSingularSupport u

Converse direction for the cone singular support: if no second component q makes (p, q) land in the scattering wavefront set, then p is outside the cone singular support.

source

theorem WavefrontDiffOps.scatteringWavefrontSet_proj_fst_subset_coneSingularSupport {n : ℕ} (u : TemperedDistribution (ConeSupport.E n) ℂ) :

Prod.fst '' ConeSupport.scatteringWavefrontSet u ⊆ ConeSupport.coneSingularSupport u

The projection to the first factor of the scattering wavefront set is contained in the cone singular support.

source

theorem WavefrontDiffOps.coneSingularSupport_subset_scatteringWavefrontSet_proj_fst {n : ℕ} (u : TemperedDistribution (ConeSupport.E n) ℂ) :

ConeSupport.coneSingularSupport u ⊆ Prod.fst '' ConeSupport.scatteringWavefrontSet u

The cone singular support is contained in the projection to the first factor of the scattering wavefront set.

source

theorem WavefrontDiffOps.scatteringWavefrontSet_proj_fst_eq_coneSingularSupport {n : ℕ} (u : TemperedDistribution (ConeSupport.E n) ℂ) :

Prod.fst '' ConeSupport.scatteringWavefrontSet u = ConeSupport.coneSingularSupport u

The projection to the first factor of the scattering wavefront set equals the cone singular support.

source

Melrose Proposition 12.14: the scattering wavefront set lies in the boundary, both wavefront sets are closed, and the projections to the first factor recover the singular support and the cone singular support respectively.