def WavefrontSet.IsOnSphere {n : ℕ} (p : ClosedBall n) : Prop

A point p of the closed unit ball is "on the sphere" if its underlying norm equals 1.

def WavefrontSet.DisjointWFscProductCondition {n : ℕ} (u v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : Prop

The disjoint scattering wavefront set condition that ensures the product u · v of two tempered distributions is well-defined: for every point p of the closed unit ball and every direction ω on the sphere, if (p, ω) lies in the scattering wavefront set of u, then the antipodal direction (p, -ω) must not lie in the scattering wavefront set of v.

def WavefrontSet.DisjointWFscConvolutionCondition {n : ℕ} (u v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : Prop

The disjoint scattering wavefront set condition that ensures the convolution u ∗ v of two tempered distributions is well-defined: for every direction θ on the sphere and every point q of the closed unit ball, if (θ, q) lies in the scattering wavefront set of u, then (-θ, q) must not lie in the scattering wavefront set of v. This is the Fourier-dual of DisjointWFscProductCondition.

noncomputable def WavefrontSet.convolution_welldefined_of_disjointWFsc {n : ℕ} (u v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hcond : DisjointWFscConvolutionCondition u v) : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ

Construction of the convolution u ∗ v of two tempered distributions under the disjoint scattering wavefront set condition for convolution.

theorem WavefrontSet.convolution_independent_of_decomposition {n : ℕ} (u v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (data₁ data₂ : ConvolutionDecompData u v) : data₁.totalConv = data₂.totalConv

The convolution constructed via a Schwartz / compactly-supported decomposition of the pair (u, v) does not depend on the choice of decomposition. This is the well-definedness statement underlying Lemma 12.6 of Melrose.

theorem WavefrontSet.disjointWFscProduct_implies_disjointWFscConvolution_fourier {n : ℕ} (u v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hcond : DisjointWFscProductCondition u v) : DisjointWFscConvolutionCondition (FourierTransform.fourier u) (FourierTransform.fourier v)

The disjoint scattering wavefront set condition for products of u and v translates, via the Fourier transform, into the disjoint scattering wavefront set condition for convolutions of 𝓕 u and 𝓕 v. This is the Fourier exchange between products and convolutions of distributions (Theorem 12.18 of Melrose).

noncomputable def WavefrontSet.product_welldefined_of_disjointWFsc {n : ℕ} (u v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hcond : DisjointWFscProductCondition u v) : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ

Construction of the product u · v of two tempered distributions under the disjoint scattering wavefront set condition for products. The product is defined by reducing to the convolution of 𝓕 u and 𝓕 v via the Fourier transform.

noncomputable def WavefrontSet.welldefined_of_disjointWFsc {n : ℕ} (u v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : (DisjointWFscProductCondition u v → TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) × (DisjointWFscConvolutionCondition u v → TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ)

Packaged form of the well-definedness statement of Theorem 12.18 of Melrose: under the appropriate disjoint scattering wavefront set conditions, the product and convolution of two tempered distributions are simultaneously well-defined.