Convolution and the Fourier transform on Schwartz space

For a Schwartz symbol σ : 𝓢(E, ℂ), the Fourier multiplier φ ↦ 𝓕⁻ (σ • 𝓕 φ) on Schwartz functions (Mathlib's SchwartzMap.fourierMultiplierCLM) is convolution with the Schwartz function 𝓕⁻ σ:

𝓕⁻ (σ • 𝓕 φ) x = ∫ 𝓕⁻ σ (x - y) • φ y.

This is the convolution theorem SchwartzMap.fourier_convolution read backwards. It identifies the kernel of a multiplier whose symbol is smooth and rapidly decreasing, which is the form taken by the truncated symbols in the Littlewood–Paley proof of the Mihlin–Hörmander multiplier theorem. By Young's inequality (MeasureTheory.eLpNorm_convolution_le), such a multiplier is bounded in every Lᵖ norm, 1 ≤ p ≤ ∞, by the L¹ norm of its kernel: ‖T_σ φ‖_p ≤ ‖𝓕⁻ σ‖₁ ‖φ‖_p.

Dually, the Fourier transform turns pointwise products into convolutions: for Schwartz functions f, g and a continuous bilinear map B,

𝓕 (B (f ·) (g ·)) ξ = ∫ B (𝓕 f t) (𝓕 g (ξ - t)) dt.

This follows from the inverse convolution theorem 𝓕⁻ (f ⋆ g) = 𝓕⁻ f · 𝓕⁻ g, which in turn is Mathlib's Real.fourier_bilin_convolution_eq composed with the reflection ξ ↦ -ξ. It is the starting point of the estimates for multiplication operators on Sobolev spaces.

Main declarations

• SchwartzMap.fourierMultiplierCLM_eq_convolution: the multiplier with symbol σ is SchwartzMap.convolution with 𝓕⁻ σ.
• SchwartzMap.fourierMultiplierCLM_apply_eq_integral: the same, pointwise, as an integral.
• SchwartzMap.eLpNorm_fourierMultiplierCLM_le: the Lᵖ bound ‖T_σ φ‖_p ≤ ‖𝓕⁻ σ‖₁ ‖φ‖_p.
• SchwartzMap.integrable_fourierInv_sub_smul: for u ∈ L², the convolution integral ∫ 𝓕⁻ σ (x - y) • u y converges absolutely at every x.
• SchwartzMap.fourierInv_convolution: the inverse Fourier transform of a convolution is the pairing of the inverse Fourier transforms.
• SchwartzMap.fourier_pairing, SchwartzMap.fourier_pairing_apply: the Fourier transform of a pointwise product is the convolution of the Fourier transforms.
• SchwartzMap.fourier_smulLeftCLM_apply: the same for the product with a scalar Schwartz function, 𝓕 (φ • f) ξ = ∫ 𝓕 φ t • 𝓕 f (ξ - t) dt.

References

• L. Grafakos, Classical Fourier Analysis, 3rd ed., Sections 2.2 and 2.5.

theorem SchwartzMap.fourierMultiplierCLM_eq_convolution {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (σ : SchwartzMap E ℂ) : fourierMultiplierCLM F ⇑σ = (convolution (ContinuousLinearMap.lsmul ℂ ℂ)) (FourierTransformInv.fourierInv σ)

On Schwartz functions, the multiplier with a Schwartz symbol σ is convolution with the Schwartz function 𝓕⁻ σ.

theorem SchwartzMap.fourierMultiplierCLM_apply_eq_integral {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (σ : SchwartzMap E ℂ) (φ : SchwartzMap E F) (x : E) : ((fourierMultiplierCLM F ⇑σ) φ) x = ∫ (y : E), (FourierTransformInv.fourierInv σ) (x - y) • φ y

The multiplier with a Schwartz symbol σ on Schwartz functions, as an integral against the kernel 𝓕⁻ σ: T_σ φ x = ∫ 𝓕⁻ σ (x - y) • φ y.

theorem SchwartzMap.eLpNorm_fourierMultiplierCLM_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (σ : SchwartzMap E ℂ) (φ : SchwartzMap E F) {p : ENNReal} (hp : 1 ≤ p) : MeasureTheory.eLpNorm (⇑((fourierMultiplierCLM F ⇑σ) φ)) p MeasureTheory.volume ≤ MeasureTheory.eLpNorm (FourierTransformInv.fourierInv ⇑σ) 1 MeasureTheory.volume * MeasureTheory.eLpNorm (⇑φ) p MeasureTheory.volume

Lᵖ bound for a multiplier with Schwartz symbol. For 1 ≤ p ≤ ∞ the multiplier with a Schwartz symbol σ satisfies ‖T_σ φ‖_p ≤ ‖𝓕⁻ σ‖₁ ‖φ‖_p on Schwartz functions.

theorem SchwartzMap.integrable_fourierInv_sub_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℂ G] (σ : SchwartzMap E ℂ) (u : ↥(MeasureTheory.Lp G 2 MeasureTheory.volume)) (x : E) : MeasureTheory.Integrable (fun (y : E) => (FourierTransformInv.fourierInv σ) (x - y) • ↑↑u y) MeasureTheory.volume

The convolution integral of an L² function against the inverse Fourier transform of a Schwartz function converges absolutely at every point.

theorem SchwartzMap.fourierInv_convolution_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {F₁ : Type u_3} {F₂ : Type u_4} {F₃ : Type u_5} [NormedAddCommGroup F₁] [NormedSpace ℂ F₁] [CompleteSpace F₁] [NormedAddCommGroup F₂] [NormedSpace ℂ F₂] [CompleteSpace F₂] [NormedAddCommGroup F₃] [NormedSpace ℂ F₃] [CompleteSpace F₃] (B : F₁ →L[ℂ] F₂ →L[ℂ] F₃) (f : SchwartzMap E F₁) (g : SchwartzMap E F₂) (ξ : E) : (FourierTransformInv.fourierInv (((convolution B) f) g)) ξ = (B ((FourierTransformInv.fourierInv f) ξ)) ((FourierTransformInv.fourierInv g) ξ)

The inverse Fourier transform turns the convolution of Schwartz functions into the pointwise product of their inverse Fourier transforms.

theorem SchwartzMap.fourierInv_convolution {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {F₁ : Type u_3} {F₂ : Type u_4} {F₃ : Type u_5} [NormedAddCommGroup F₁] [NormedSpace ℂ F₁] [CompleteSpace F₁] [NormedAddCommGroup F₂] [NormedSpace ℂ F₂] [CompleteSpace F₂] [NormedAddCommGroup F₃] [NormedSpace ℂ F₃] [CompleteSpace F₃] (B : F₁ →L[ℂ] F₂ →L[ℂ] F₃) (f : SchwartzMap E F₁) (g : SchwartzMap E F₂) : FourierTransformInv.fourierInv (((convolution B) f) g) = ((pairing B) (FourierTransformInv.fourierInv f)) (FourierTransformInv.fourierInv g)

The inverse Fourier transform of a convolution of Schwartz functions is the pairing of their inverse Fourier transforms.

theorem SchwartzMap.fourier_pairing {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {F₁ : Type u_3} {F₂ : Type u_4} {F₃ : Type u_5} [NormedAddCommGroup F₁] [NormedSpace ℂ F₁] [CompleteSpace F₁] [NormedAddCommGroup F₂] [NormedSpace ℂ F₂] [CompleteSpace F₂] [NormedAddCommGroup F₃] [NormedSpace ℂ F₃] [CompleteSpace F₃] (B : F₁ →L[ℂ] F₂ →L[ℂ] F₃) (f : SchwartzMap E F₁) (g : SchwartzMap E F₂) : FourierTransform.fourier (((pairing B) f) g) = ((convolution B) (FourierTransform.fourier f)) (FourierTransform.fourier g)

The Fourier transform of a product is the convolution of the Fourier transforms. For Schwartz functions f, g and a continuous bilinear map B, the Fourier transform of the pointwise product x ↦ B (f x) (g x) is the convolution of 𝓕 f and 𝓕 g.

theorem SchwartzMap.fourier_pairing_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {F₁ : Type u_3} {F₂ : Type u_4} {F₃ : Type u_5} [NormedAddCommGroup F₁] [NormedSpace ℂ F₁] [CompleteSpace F₁] [NormedAddCommGroup F₂] [NormedSpace ℂ F₂] [CompleteSpace F₂] [NormedAddCommGroup F₃] [NormedSpace ℂ F₃] [CompleteSpace F₃] (B : F₁ →L[ℂ] F₂ →L[ℂ] F₃) (f : SchwartzMap E F₁) (g : SchwartzMap E F₂) (ξ : E) : (FourierTransform.fourier (((pairing B) f) g)) ξ = ∫ (t : E), (B ((FourierTransform.fourier f) t)) ((FourierTransform.fourier g) (ξ - t))

The Fourier transform of a pointwise product of Schwartz functions, as an integral: 𝓕 (B (f ·) (g ·)) ξ = ∫ t, B (𝓕 f t) (𝓕 g (ξ - t)).

theorem SchwartzMap.fourier_smulLeftCLM_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (φ : SchwartzMap E ℂ) (f : SchwartzMap E F) (ξ : E) : (FourierTransform.fourier ((smulLeftCLM F ⇑φ) f)) ξ = ∫ (t : E), (FourierTransform.fourier φ) t • (FourierTransform.fourier f) (ξ - t)

The Fourier transform of the product of a Schwartz function f by a scalar Schwartz function φ is the convolution 𝓕 (φ • f) ξ = ∫ t, 𝓕 φ t • 𝓕 f (ξ - t).