The Fourier transform of the convolution

In this file we calculate the Fourier transform of a convolution.

Main definitions

• SchwartzMap.convolution: The convolution on Schwartz functions is defined via the Fourier transform.

Main statements

• Real.fourier_bilin_convolution_eq: The Fourier transform of a convolution is the bilinear map applied to the Fourier transform of the functions.
• Real.fourier_smul_convolution_eq: Variant for scalar multiplication.
• Real.fourier_mul_convolution_eq: Variant for multiplication.
• SchwartzMap.fourier_convolution: The Fourier transform of the Schwartz convolution is given by the pairing of the Fourier transformed Schwartz functions.
• SchwartzMap.convolution_apply: The Schwartz function convolution coincides with the convolution for functions.

theorem Real.integrable_prod_sub {𝕜 : Type u_1} {E : Type u_3} {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F₁] [NormedAddCommGroup F₂] [NormedAddCommGroup F₃] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedSpace 𝕜 F₁] [NormedSpace 𝕜 F₂] [NormedSpace 𝕜 F₃] (B : F₁ →L[𝕜] F₂ →L[𝕜] F₃) {f₁ : E → F₁} {f₂ : E → F₂} (hf₁ : MeasureTheory.Integrable f₁ MeasureTheory.volume) (hf₂ : MeasureTheory.Integrable f₂ MeasureTheory.volume) (hf₁' : Continuous f₁) (hf₂' : Continuous f₂) : MeasureTheory.Integrable (fun (p : E × E) => ‖B‖ * (‖f₁ (p.1 - p.2)‖ * ‖f₂ p.2‖)) (MeasureTheory.volume.prod MeasureTheory.volume)

theorem Real.fourier_bilin_convolution_eq_integral {𝕜 : Type u_1} {E : Type u_3} {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F₁] [NormedAddCommGroup F₂] [NormedAddCommGroup F₃] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedSpace 𝕜 F₁] [NormedSpace 𝕜 F₂] [NormedSpace 𝕜 F₃] [NormedSpace ℂ F₃] (B : F₁ →L[𝕜] F₂ →L[𝕜] F₃) {f₁ : E → F₁} {f₂ : E → F₂} (hf₁ : MeasureTheory.Integrable f₁ MeasureTheory.volume) (hf₂ : MeasureTheory.Integrable f₂ MeasureTheory.volume) (hf₁' : Continuous f₁) (hf₂' : Continuous f₂) (ξ : E) : FourierTransform.fourier (MeasureTheory.convolution f₁ f₂ B MeasureTheory.volume) ξ = ∫ (y : E) (x : E), fourierChar (-inner ℝ (y + x) ξ) • (B (f₁ x)) (f₂ y)

Calculate the Fourier transform of the convolution as a symmetric integral.

theorem Real.fourier_bilin_convolution_eq {E : Type u_3} {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup F₁] [NormedAddCommGroup F₂] [NormedAddCommGroup F₃] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedSpace ℂ F₃] [CompleteSpace F₁] [CompleteSpace F₂] [CompleteSpace F₃] [NormedSpace ℂ F₁] [NormedSpace ℂ F₂] (B : F₁ →L[ℂ] F₂ →L[ℂ] F₃) {f₁ : E → F₁} {f₂ : E → F₂} (hf₁ : MeasureTheory.Integrable f₁ MeasureTheory.volume) (hf₂ : MeasureTheory.Integrable f₂ MeasureTheory.volume) (hf₁' : Continuous f₁) (hf₂' : Continuous f₂) (ξ : E) : FourierTransform.fourier (MeasureTheory.convolution f₁ f₂ B MeasureTheory.volume) ξ = (B (FourierTransform.fourier f₁ ξ)) (FourierTransform.fourier f₂ ξ)

The Fourier transform of the convolution is given by the bilinear map applied to the Fourier transform of the individual functions.

theorem Real.fourier_smul_convolution_eq {E : Type u_3} {F₁ : Type u_5} [NormedAddCommGroup E] [NormedAddCommGroup F₁] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F₁] [NormedSpace ℂ F₁] {f₁ : E → ℂ} {f₂ : E → F₁} (hf₁ : MeasureTheory.Integrable f₁ MeasureTheory.volume) (hf₂ : MeasureTheory.Integrable f₂ MeasureTheory.volume) (hf₁' : Continuous f₁) (hf₂' : Continuous f₂) (ξ : E) : FourierTransform.fourier (MeasureTheory.convolution f₁ f₂ (ContinuousLinearMap.lsmul ℂ ℂ) MeasureTheory.volume) ξ = FourierTransform.fourier f₁ ξ • FourierTransform.fourier f₂ ξ

The Fourier transform of the convolution is given by the multiplication of the Fourier transform of the individual functions.

Version for scalar multiplication.

theorem Real.fourier_mul_convolution_eq {R : Type u_2} {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedRing R] [NormedSpace ℂ R] [IsScalarTower ℂ R R] [SMulCommClass ℂ R R] [CompleteSpace R] {f₁ f₂ : E → R} (hf₁ : MeasureTheory.Integrable f₁ MeasureTheory.volume) (hf₂ : MeasureTheory.Integrable f₂ MeasureTheory.volume) (hf₁' : Continuous f₁) (hf₂' : Continuous f₂) (ξ : E) : FourierTransform.fourier (MeasureTheory.convolution f₁ f₂ (ContinuousLinearMap.mul ℂ R) MeasureTheory.volume) ξ = FourierTransform.fourier f₁ ξ * FourierTransform.fourier f₂ ξ

The Fourier transform of the convolution is given by the multiplication of the Fourier transform of the individual functions.

Version for multiplication.

noncomputable def SchwartzMap.convolution {𝕜 : Type u_1} {E : Type u_3} {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F₁] [NormedSpace ℂ F₁] [NormedSpace 𝕜 F₁] [SMulCommClass ℂ 𝕜 F₁] [NormedAddCommGroup F₂] [NormedSpace ℂ F₂] [NormedSpace 𝕜 F₂] [SMulCommClass ℂ 𝕜 F₂] [NormedAddCommGroup F₃] [NormedSpace ℂ F₃] [NormedSpace 𝕜 F₃] [SMulCommClass ℂ 𝕜 F₃] (B : F₁ →L[𝕜] F₂ →L[𝕜] F₃) : SchwartzMap E F₁ →ₗ[𝕜] SchwartzMap E F₂ →L[𝕜] SchwartzMap E F₃

The bilinear convolution of Schwartz functions.

The continuity in the left argument is provided in SchwartzMap.convolution_continuous_left.

Equations

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

@[simp]

theorem SchwartzMap.convolution_flip {𝕜 : Type u_1} {E : Type u_3} {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F₁] [NormedSpace ℂ F₁] [NormedSpace 𝕜 F₁] [SMulCommClass ℂ 𝕜 F₁] [NormedAddCommGroup F₂] [NormedSpace ℂ F₂] [NormedSpace 𝕜 F₂] [SMulCommClass ℂ 𝕜 F₂] [NormedAddCommGroup F₃] [NormedSpace ℂ F₃] [NormedSpace 𝕜 F₃] [SMulCommClass ℂ 𝕜 F₃] (B : F₁ →L[𝕜] F₂ →L[𝕜] F₃) (f : SchwartzMap E F₁) (g : SchwartzMap E F₂) : ((convolution B.flip) g) f = ((convolution B) f) g

theorem SchwartzMap.convolution_continuous_left {𝕜 : Type u_1} {E : Type u_3} {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F₁] [NormedSpace ℂ F₁] [NormedSpace 𝕜 F₁] [SMulCommClass ℂ 𝕜 F₁] [NormedAddCommGroup F₂] [NormedSpace ℂ F₂] [NormedSpace 𝕜 F₂] [SMulCommClass ℂ 𝕜 F₂] [NormedAddCommGroup F₃] [NormedSpace ℂ F₃] [NormedSpace 𝕜 F₃] [SMulCommClass ℂ 𝕜 F₃] (B : F₁ →L[𝕜] F₂ →L[𝕜] F₃) (g : SchwartzMap E F₂) : Continuous fun (x : SchwartzMap E F₁) => ((convolution B) x) g

The convolution is continuous in the left argument.

Note that since 𝓢(E, F) is not a normed space, uncurried and curried continuity do not coincide.

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

theorem SchwartzMap.fourier_convolution_apply {E : Type u_3} {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F₁] [NormedSpace ℂ F₁] [NormedAddCommGroup F₂] [NormedSpace ℂ F₂] [NormedAddCommGroup F₃] [NormedSpace ℂ F₃] [CompleteSpace F₃] [CompleteSpace F₁] [CompleteSpace F₂] (B : F₁ →L[ℂ] F₂ →L[ℂ] F₃) (f : SchwartzMap E F₁) (g : SchwartzMap E F₂) (x : E) : (FourierTransform.fourier (((convolution B) f) g)) x = FourierTransform.fourier (MeasureTheory.convolution (⇑f) (⇑g) B MeasureTheory.volume) x

theorem SchwartzMap.convolution_apply {E : Type u_3} {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F₁] [NormedSpace ℂ F₁] [NormedAddCommGroup F₂] [NormedSpace ℂ F₂] [NormedAddCommGroup F₃] [NormedSpace ℂ F₃] [CompleteSpace F₃] [CompleteSpace F₁] [CompleteSpace F₂] (B : F₁ →L[ℂ] F₂ →L[ℂ] F₃) (f : SchwartzMap E F₁) (g : SchwartzMap E F₂) (x : E) : (((convolution B) f) g) x = MeasureTheory.convolution (⇑f) (⇑g) B MeasureTheory.volume x

The convolution on Schwartz functions is equal to the convolution on functions.