Fourier multiplier on Schwartz functions and tempered distributions

We define a Fourier multiplier as continuous linear maps on Schwartz functions and tempered distributions. The multiplier function is throughout assumed to have temperate growth.

Main definitions

• SchwartzMap.fourierMultiplierCLM: Fourier multiplier on Schwartz functions
• TemperedDistribution.fourierMultiplierCLM: Fourier multiplier on tempered distribution

Main statements

• SchwartzMap.lineDeriv_eq_fourierMultiplierCLM: the directional derivative is equal to the Fourier multiplier with inner ℝ . m.
• SchwartzMap.laplacian_eq_fourierMultiplierCLM: the Laplacian is equal to the Fourier multiplier with ‖·‖.
• TemperedDistribution.lineDeriv_eq_fourierMultiplierCLM: the distributional directional derivative is equal to the Fourier multiplier with inner ℝ . m.
• TemperedDistribution.laplacian_eq_fourierMultiplierCLM: the distributional Laplacian is equal to the Fourier multiplier with ‖·‖.

Schwartz functions

noncomputable def SchwartzMap.fourierMultiplierCLM {𝕜 : Type u_2} {E : Type u_3} (F : Type u_4) [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [NormedSpace 𝕜 F] [SMulCommClass ℂ 𝕜 F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (g : E → 𝕜) : SchwartzMap E F →L[𝕜] SchwartzMap E F

Fourier multiplier on Schwartz functions.

Equations

• SchwartzMap.fourierMultiplierCLM F g = FourierTransform.fourierInvCLM 𝕜 (SchwartzMap E F) ∘SL SchwartzMap.smulLeftCLM F g ∘SL FourierTransform.fourierCLM 𝕜 (SchwartzMap E F)

theorem SchwartzMap.fourierMultiplierCLM_apply {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [NormedSpace 𝕜 F] [SMulCommClass ℂ 𝕜 F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (g : E → 𝕜) (f : SchwartzMap E F) : (fourierMultiplierCLM F g) f = FourierTransformInv.fourierInv ((smulLeftCLM F g) (FourierTransform.fourier f))

theorem SchwartzMap.fourierMultiplierCLM_ofReal (𝕜 : Type u_2) {E : Type u_3} {F : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [NormedSpace 𝕜 F] [SMulCommClass ℂ 𝕜 F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {g : E → ℝ} (hg : Function.HasTemperateGrowth g) (f : SchwartzMap E F) : (fourierMultiplierCLM F fun (x : E) => ↑(g x)) f = (fourierMultiplierCLM F g) f

theorem SchwartzMap.fourierMultiplierCLM_smul {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [NormedSpace 𝕜 F] [SMulCommClass ℂ 𝕜 F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {g : E → 𝕜} (hg : Function.HasTemperateGrowth g) (c : 𝕜) : fourierMultiplierCLM F (c • g) = c • fourierMultiplierCLM F g

theorem SchwartzMap.fourierMultiplierCLM_sum {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} (F : Type u_4) [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [NormedSpace 𝕜 F] [SMulCommClass ℂ 𝕜 F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {g : ι → E → 𝕜} {s : Finset ι} (hg : ∀ i ∈ s, Function.HasTemperateGrowth (g i)) : (fourierMultiplierCLM F fun (x : E) => ∑ i ∈ s, g i x) = ∑ i ∈ s, fourierMultiplierCLM F (g i)

@[simp]

theorem SchwartzMap.fourierMultiplierCLM_const {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [NormedSpace 𝕜 F] [SMulCommClass ℂ 𝕜 F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] (c : 𝕜) : (fourierMultiplierCLM F fun (x : E) => c) = c • ContinuousLinearMap.id 𝕜 (SchwartzMap E F)

theorem SchwartzMap.fourierMultiplierCLM_fourierMultiplierCLM_apply {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [NormedSpace 𝕜 F] [SMulCommClass ℂ 𝕜 F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] {g₁ g₂ : E → 𝕜} (hg₁ : Function.HasTemperateGrowth g₁) (hg₂ : Function.HasTemperateGrowth g₂) (f : SchwartzMap E F) : (fourierMultiplierCLM F g₁) ((fourierMultiplierCLM F g₂) f) = (fourierMultiplierCLM F (g₁ * g₂)) f

theorem SchwartzMap.fourierMultiplierCLM_compL_fourierMultiplierCLM {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [NormedSpace 𝕜 F] [SMulCommClass ℂ 𝕜 F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] {g₁ g₂ : E → 𝕜} (hg₁ : Function.HasTemperateGrowth g₁) (hg₂ : Function.HasTemperateGrowth g₂) : fourierMultiplierCLM F g₁ ∘SL fourierMultiplierCLM F g₂ = fourierMultiplierCLM F (g₁ * g₂)

theorem SchwartzMap.lineDeriv_eq_fourierMultiplierCLM {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] (m : E) (f : SchwartzMap E F) : LineDeriv.lineDerivOp m f = (2 * ↑Real.pi * Complex.I) • (fourierMultiplierCLM F fun (x : E) => inner ℝ x m) f

theorem SchwartzMap.laplacian_eq_fourierMultiplierCLM {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] (f : SchwartzMap E F) : Laplacian.laplacian f = -(2 * Real.pi) ^ 2 • (fourierMultiplierCLM F fun (x : E) => ‖x‖ ^ 2) f

Tempered distributions

noncomputable def TemperedDistribution.fourierMultiplierCLM {E : Type u_3} (F : Type u_4) [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (g : E → ℂ) : TemperedDistribution E F →L[ℂ] TemperedDistribution E F

Fourier multiplier on tempered distributions.

Equations

• One or more equations did not get rendered due to their size.

theorem TemperedDistribution.fourierMultiplierCLM_apply {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (g : E → ℂ) (f : TemperedDistribution E F) : (fourierMultiplierCLM F g) f = FourierTransformInv.fourierInv ((smulLeftCLM F g) (FourierTransform.fourier f))

@[simp]

theorem TemperedDistribution.fourierMultiplierCLM_apply_apply {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (g : E → ℂ) (f : TemperedDistribution E F) (u : SchwartzMap E ℂ) : ((fourierMultiplierCLM F g) f) u = f (FourierTransform.fourier ((SchwartzMap.smulLeftCLM ℂ g) (FourierTransformInv.fourierInv u)))

@[simp]

theorem TemperedDistribution.fourierMultiplierCLM_const {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (c : ℂ) : (fourierMultiplierCLM F fun (x : E) => c) = c • ContinuousLinearMap.id ℂ (TemperedDistribution E F)

theorem TemperedDistribution.fourierMultiplierCLM_fourierMultiplierCLM_apply {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {g₁ g₂ : E → ℂ} (hg₁ : Function.HasTemperateGrowth g₁) (hg₂ : Function.HasTemperateGrowth g₂) (f : TemperedDistribution E F) : (fourierMultiplierCLM F g₂) ((fourierMultiplierCLM F g₁) f) = (fourierMultiplierCLM F (g₁ * g₂)) f

theorem TemperedDistribution.fourierMultiplierCLM_compL_fourierMultiplierCLM {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {g₁ g₂ : E → ℂ} (hg₁ : Function.HasTemperateGrowth g₁) (hg₂ : Function.HasTemperateGrowth g₂) : fourierMultiplierCLM F g₂ ∘SL fourierMultiplierCLM F g₁ = fourierMultiplierCLM F (g₁ * g₂)

theorem TemperedDistribution.fourierMultiplierCLM_smul {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {g : E → ℂ} (hg : Function.HasTemperateGrowth g) (c : ℂ) : fourierMultiplierCLM F (c • g) = c • fourierMultiplierCLM F g

theorem TemperedDistribution.fourierMultiplierCLM_sum {ι : Type u_1} {E : Type u_3} (F : Type u_4) [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {g : ι → E → ℂ} {s : Finset ι} (hg : ∀ i ∈ s, Function.HasTemperateGrowth (g i)) : (fourierMultiplierCLM F fun (x : E) => ∑ i ∈ s, g i x) = ∑ i ∈ s, fourierMultiplierCLM F (g i)

theorem TemperedDistribution.fourierMultiplierCLM_toTemperedDistributionCLM_eq {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] {g : E → ℂ} (hg : Function.HasTemperateGrowth g) (f : SchwartzMap E F) : (fourierMultiplierCLM F g) ((SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume) f) = (SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume) ((SchwartzMap.fourierMultiplierCLM F g) f)

theorem TemperedDistribution.lineDeriv_eq_fourierMultiplierCLM {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (m : E) (f : TemperedDistribution E F) : LineDeriv.lineDerivOp m f = (2 * ↑Real.pi * Complex.I) • (fourierMultiplierCLM F fun (x : E) => ↑(inner ℝ x m)) f

theorem TemperedDistribution.laplacian_eq_fourierMultiplierCLM {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [NormedSpace ℂ F] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (f : TemperedDistribution E F) : Laplacian.laplacian f = -(2 * Real.pi) ^ 2 • (fourierMultiplierCLM F fun (x : E) => ↑(‖x‖ ^ 2)) f