Fourier multipliers on tempered distributions

Mathlib's Fourier multiplier TemperedDistribution.fourierMultiplierCLM F g on tempered distributions conjugates multiplication by a temperate-growth symbol g with the Fourier transform. This file records that it is additive in the symbol, the tempered analogue of SchwartzMap.fourierMultiplierCLM_add.

It also records how multipliers interact with frequency localization. A tempered distribution u is localized in frequency to the complement of a set s when its Fourier transform vanishes on s (Distribution.IsVanishingOn (𝓕 u) s). A multiplier whose symbol equals one away from a closed subset of s then fixes u, and directional derivatives, which are the multipliers with symbols 2πi ⟪ξ, m⟫, preserve the localization. This is how band-limited functions are reproduced by a multiplier with a smooth compactly supported symbol, the starting point of Bernstein's inequalities.

Main results

• TemperedDistribution.fourierMultiplierCLM_add: Fourier multipliers are additive in the symbol.
• TemperedDistribution.fourierMultiplierCLM_eq_zero_of_not_hasTemperateGrowth: the multiplier of a symbol without temperate growth is the junk value 0.
• TemperedDistribution.fourierMultiplierCLM_eq_self_of_isVanishingOn: a multiplier whose symbol is one outside the set where 𝓕 u vanishes fixes u.
• TemperedDistribution.isVanishingOn_fourier_lineDerivOp, TemperedDistribution.isVanishingOn_fourier_iteratedLineDerivOp: derivatives preserve the vanishing of the Fourier transform.

@[simp]

theorem TemperedDistribution.fourierMultiplierCLM_eq_zero_of_not_hasTemperateGrowth {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] {g : E → ℂ} (hg : ¬Function.HasTemperateGrowth g) : fourierMultiplierCLM F g = 0

The Fourier multiplier of a symbol without temperate growth is the junk value 0, because TemperedDistribution.smulLeftCLM is 0 for such a symbol.

theorem TemperedDistribution.fourierMultiplierCLM_add {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] {g₁ g₂ : E → ℂ} (hg₁ : Function.HasTemperateGrowth g₁) (hg₂ : Function.HasTemperateGrowth g₂) : fourierMultiplierCLM F (g₁ + g₂) = fourierMultiplierCLM F g₁ + fourierMultiplierCLM F g₂

Fourier multipliers on tempered distributions are additive in the symbol.

theorem TemperedDistribution.isVanishingOn_fourier_lineDerivOp {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] {u : TemperedDistribution E F} {s : Set E} (hu : Distribution.IsVanishingOn (⇑(FourierTransform.fourier u)) s) (m : E) : Distribution.IsVanishingOn (⇑(FourierTransform.fourier (LineDeriv.lineDerivOp m u))) s

Differentiation does not enlarge the spectrum. If the Fourier transform of u vanishes on s, so does that of ∂_m u.

theorem TemperedDistribution.isVanishingOn_fourier_iteratedLineDerivOp {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] {u : TemperedDistribution E F} {s : Set E} (hu : Distribution.IsVanishingOn (⇑(FourierTransform.fourier u)) s) {k : ℕ} (m : Fin k → E) : Distribution.IsVanishingOn (⇑(FourierTransform.fourier (LineDeriv.iteratedLineDerivOp m u))) s

Differentiation does not enlarge the spectrum. If the Fourier transform of u vanishes on s, so does that of every iterated derivative ∂_{m₁} ⋯ ∂_{mₖ} u.

theorem TemperedDistribution.fourierMultiplierCLM_eq_self_of_isVanishingOn {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] {u : TemperedDistribution E F} {s : Set E} (hu : Distribution.IsVanishingOn (⇑(FourierTransform.fourier u)) s) {g : E → ℂ} (hg : Function.HasTemperateGrowth g) (hgs : tsupport (g - 1) ⊆ s) : (fourierMultiplierCLM F g) u = u

A multiplier equal to one near the spectrum is the identity. If the Fourier transform of a tempered distribution u vanishes on s, and the symbol g of temperate growth equals one outside a closed subset of s (that is, tsupport (g - 1) ⊆ s), then the Fourier multiplier with symbol g fixes u.