The Fourier transform

We set up the Fourier transform for complex-valued functions on finite-dimensional spaces.

Design choices

In namespace VectorFourier, we define the Fourier integral in the following context:

• 𝕜 is a commutative ring.
• V and W are 𝕜-modules.
• e is a unitary additive character of 𝕜, i.e. an AddChar 𝕜 circle.
• μ is a measure on V.
• L is a 𝕜-bilinear form V × W → 𝕜.
• E is a complete normed ℂ-vector space.

With these definitions, we define fourierIntegral to be the map from functions V → E to functions W → E that sends f to

fun w ↦ ∫ v in V, e (-L v w) • f v ∂μ,

This includes the cases W is the dual of V and L is the canonical pairing, or W = V and L is a bilinear form (e.g. an inner product).

In namespace Fourier, we consider the more familiar special case when V = W = 𝕜 and L is the multiplication map (but still allowing 𝕜 to be an arbitrary ring equipped with a measure).

The most familiar case of all is when V = W = 𝕜 = ℝ, L is multiplication, μ is volume, and e is Real.fourierChar, i.e. the character fun x ↦ exp ((2 * π * x) * I) (for which we introduce the notation 𝐞 in the locale FourierTransform).

Another familiar case (which generalizes the previous one) is when V = W is an inner product space over ℝ and L is the scalar product. We introduce two notations 𝓕 for the Fourier transform in this case and 𝓕⁻ f (v) = 𝓕 f (-v) for the inverse Fourier transform. These notations make in particular sense for V = W = ℝ.

Main results

At present the only nontrivial lemma we prove is fourierIntegral_continuous, stating that the Fourier transform of an integrable function is continuous (under mild assumptions).

Fourier theory for functions on general vector spaces

def VectorFourier.fourierIntegral {𝕜 : Type u_1} [CommRing 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] [MeasurableSpace V] {W : Type u_3} [AddCommGroup W] [Module 𝕜 W] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℂ E] (e : AddChar 𝕜 ↥circle) (μ : MeasureTheory.Measure V) (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V → E) (w : W) : E

The Fourier transform integral for f : V → E, with respect to a bilinear form L : V × W → 𝕜 and an additive character e.

Equations

• VectorFourier.fourierIntegral e μ L f w = ∫ (v : V), e (-(L v) w) • f v ∂μ

theorem VectorFourier.fourierIntegral_smul_const {𝕜 : Type u_1} [CommRing 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] [MeasurableSpace V] {W : Type u_3} [AddCommGroup W] [Module 𝕜 W] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℂ E] (e : AddChar 𝕜 ↥circle) (μ : MeasureTheory.Measure V) (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V → E) (r : ℂ) : VectorFourier.fourierIntegral e μ L (r • f) = r • VectorFourier.fourierIntegral e μ L f

theorem VectorFourier.norm_fourierIntegral_le_integral_norm {𝕜 : Type u_1} [CommRing 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] [MeasurableSpace V] {W : Type u_3} [AddCommGroup W] [Module 𝕜 W] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℂ E] (e : AddChar 𝕜 ↥circle) (μ : MeasureTheory.Measure V) (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V → E) (w : W) : ‖VectorFourier.fourierIntegral e μ L f w‖ ≤ ∫ (v : V), ‖f v‖ ∂μ

The uniform norm of the Fourier integral of f is bounded by the L¹ norm of f.

theorem VectorFourier.fourierIntegral_comp_add_right {𝕜 : Type u_1} [CommRing 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] [MeasurableSpace V] {W : Type u_3} [AddCommGroup W] [Module 𝕜 W] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℂ E] [MeasurableAdd V] (e : AddChar 𝕜 ↥circle) (μ : MeasureTheory.Measure V) [MeasureTheory.Measure.IsAddRightInvariant μ] (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V → E) (v₀ : V) : VectorFourier.fourierIntegral e μ L (f ∘ fun (v : V) => v + v₀) = fun (w : W) => e ((L v₀) w) • VectorFourier.fourierIntegral e μ L f w

The Fourier integral converts right-translation into scalar multiplication by a phase factor.

theorem VectorFourier.fourier_integral_convergent_iff {𝕜 : Type u_1} [CommRing 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] [MeasurableSpace V] {W : Type u_3} [AddCommGroup W] [Module 𝕜 W] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℂ E] [TopologicalSpace 𝕜] [TopologicalRing 𝕜] [TopologicalSpace V] [BorelSpace V] [TopologicalSpace W] {e : AddChar 𝕜 ↥circle} {μ : MeasureTheory.Measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜} (he : Continuous ⇑e) (hL : Continuous fun (p : V × W) => (L p.1) p.2) {f : V → E} (w : W) : MeasureTheory.Integrable f μ ↔ MeasureTheory.Integrable (fun (v : V) => e (-(L v) w) • f v) μ

For any w, the Fourier integral is convergent iff f is integrable.

theorem VectorFourier.fourierIntegral_add {𝕜 : Type u_1} [CommRing 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] [MeasurableSpace V] {W : Type u_3} [AddCommGroup W] [Module 𝕜 W] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℂ E] [TopologicalSpace 𝕜] [TopologicalRing 𝕜] [TopologicalSpace V] [BorelSpace V] [TopologicalSpace W] {e : AddChar 𝕜 ↥circle} {μ : MeasureTheory.Measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜} (he : Continuous ⇑e) (hL : Continuous fun (p : V × W) => (L p.1) p.2) {f : V → E} {g : V → E} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) : VectorFourier.fourierIntegral e μ L f + VectorFourier.fourierIntegral e μ L g = VectorFourier.fourierIntegral e μ L (f + g)

theorem VectorFourier.fourierIntegral_continuous {𝕜 : Type u_1} [CommRing 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] [MeasurableSpace V] {W : Type u_3} [AddCommGroup W] [Module 𝕜 W] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℂ E] [TopologicalSpace 𝕜] [TopologicalRing 𝕜] [TopologicalSpace V] [BorelSpace V] [TopologicalSpace W] {e : AddChar 𝕜 ↥circle} {μ : MeasureTheory.Measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜} [FirstCountableTopology W] (he : Continuous ⇑e) (hL : Continuous fun (p : V × W) => (L p.1) p.2) {f : V → E} (hf : MeasureTheory.Integrable f μ) : Continuous (VectorFourier.fourierIntegral e μ L f)

The Fourier integral of an L^1 function is a continuous function.

theorem VectorFourier.integral_bilin_fourierIntegral_eq_flip {𝕜 : Type u_1} [CommRing 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] [MeasurableSpace V] {W : Type u_3} [AddCommGroup W] [Module 𝕜 W] {E : Type u_4} {F : Type u_5} {G : Type u_6} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [NormedAddCommGroup G] [NormedSpace ℂ G] [TopologicalSpace 𝕜] [TopologicalRing 𝕜] [TopologicalSpace V] [BorelSpace V] [TopologicalSpace W] [MeasurableSpace W] [BorelSpace W] {e : AddChar 𝕜 ↥circle} {μ : MeasureTheory.Measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜} {ν : MeasureTheory.Measure W} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] [SecondCountableTopology V] [CompleteSpace E] [CompleteSpace F] {f : V → E} {g : W → F} (M : E →L[ℂ] F →L[ℂ] G) (he : Continuous ⇑e) (hL : Continuous fun (p : V × W) => (L p.1) p.2) (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g ν) : ∫ (ξ : W), (M (VectorFourier.fourierIntegral e μ L f ξ)) (g ξ) ∂ν = ∫ (x : V), (M (f x)) (VectorFourier.fourierIntegral e ν (LinearMap.flip L) g x) ∂μ

The Fourier transform satisfies ∫ 𝓕 f * g = ∫ f * 𝓕 g, i.e., it is self-adjoint. Version where the multiplication is replaced by a general bilinear form M.

theorem VectorFourier.integral_fourierIntegral_smul_eq_flip {𝕜 : Type u_1} [CommRing 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] [MeasurableSpace V] {W : Type u_3} [AddCommGroup W] [Module 𝕜 W] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace ℂ F] [TopologicalSpace 𝕜] [TopologicalRing 𝕜] [TopologicalSpace V] [BorelSpace V] [TopologicalSpace W] [MeasurableSpace W] [BorelSpace W] {e : AddChar 𝕜 ↥circle} {μ : MeasureTheory.Measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜} {ν : MeasureTheory.Measure W} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] [SecondCountableTopology V] [CompleteSpace F] {f : V → ℂ} {g : W → F} (he : Continuous ⇑e) (hL : Continuous fun (p : V × W) => (L p.1) p.2) (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g ν) : ∫ (ξ : W), VectorFourier.fourierIntegral e μ L f ξ • g ξ ∂ν = ∫ (x : V), f x • VectorFourier.fourierIntegral e ν (LinearMap.flip L) g x ∂μ

The Fourier transform satisfies ∫ 𝓕 f * g = ∫ f * 𝓕 g, i.e., it is self-adjoint.

Fourier theory for functions on 𝕜

def Fourier.fourierIntegral {𝕜 : Type u_1} [CommRing 𝕜] [MeasurableSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] (e : AddChar 𝕜 ↥circle) (μ : MeasureTheory.Measure 𝕜) (f : 𝕜 → E) (w : 𝕜) : E

The Fourier transform integral for f : 𝕜 → E, with respect to the measure μ and additive character e.

Equations

• Fourier.fourierIntegral e μ f w = VectorFourier.fourierIntegral e μ (LinearMap.mul 𝕜 𝕜) f w

theorem Fourier.fourierIntegral_def {𝕜 : Type u_1} [CommRing 𝕜] [MeasurableSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] (e : AddChar 𝕜 ↥circle) (μ : MeasureTheory.Measure 𝕜) (f : 𝕜 → E) (w : 𝕜) : Fourier.fourierIntegral e μ f w = ∫ (v : 𝕜), e (-(v * w)) • f v ∂μ

theorem Fourier.fourierIntegral_smul_const {𝕜 : Type u_1} [CommRing 𝕜] [MeasurableSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] (e : AddChar 𝕜 ↥circle) (μ : MeasureTheory.Measure 𝕜) (f : 𝕜 → E) (r : ℂ) : Fourier.fourierIntegral e μ (r • f) = r • Fourier.fourierIntegral e μ f

theorem Fourier.norm_fourierIntegral_le_integral_norm {𝕜 : Type u_1} [CommRing 𝕜] [MeasurableSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] (e : AddChar 𝕜 ↥circle) (μ : MeasureTheory.Measure 𝕜) (f : 𝕜 → E) (w : 𝕜) : ‖Fourier.fourierIntegral e μ f w‖ ≤ ∫ (x : 𝕜), ‖f x‖ ∂μ

The uniform norm of the Fourier transform of f is bounded by the L¹ norm of f.

theorem Fourier.fourierIntegral_comp_add_right {𝕜 : Type u_1} [CommRing 𝕜] [MeasurableSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [MeasurableAdd 𝕜] (e : AddChar 𝕜 ↥circle) (μ : MeasureTheory.Measure 𝕜) [MeasureTheory.Measure.IsAddRightInvariant μ] (f : 𝕜 → E) (v₀ : 𝕜) : Fourier.fourierIntegral e μ (f ∘ fun (v : 𝕜) => v + v₀) = fun (w : 𝕜) => e (v₀ * w) • Fourier.fourierIntegral e μ f w

The Fourier transform converts right-translation into scalar multiplication by a phase factor.

def Real.fourierChar : AddChar ℝ ↥circle

The standard additive character of ℝ, given by fun x ↦ exp (2 * π * x * I).

Equations

• Real.fourierChar = { toFun := fun (z : ℝ) => expMapCircle (2 * Real.pi * z), map_zero_one' := Real.fourierChar.proof_2, map_add_mul' := Real.fourierChar.proof_3 }

def FourierTransform.«term𝐞» : Lean.ParserDescr

The standard additive character of ℝ, given by fun x ↦ exp (2 * π * x * I).

Equations

• FourierTransform.«term𝐞» = Lean.ParserDescr.node `FourierTransform.term𝐞 1024 (Lean.ParserDescr.symbol "𝐞")

theorem Real.fourierChar_apply (x : ℝ) : ↑(Real.fourierChar x) = Complex.exp (↑(2 * Real.pi * x) * Complex.I)

theorem Real.continuous_fourierChar : Continuous ⇑Real.fourierChar

theorem Real.vector_fourierIntegral_eq_integral_exp_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_2} [AddCommGroup V] [Module ℝ V] [MeasurableSpace V] {W : Type u_3} [AddCommGroup W] [Module ℝ W] (L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ) (μ : MeasureTheory.Measure V) (f : V → E) (w : W) : VectorFourier.fourierIntegral Real.fourierChar μ L f w = ∫ (v : V), Complex.exp (↑(-2 * Real.pi * (L v) w) * Complex.I) • f v ∂μ

def Real.fourierIntegral {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] (f : V → E) (w : V) : E

The Fourier transform of a function on an inner product space, with respect to the standard additive character ω ↦ exp (2 i π ω).

Equations

• Real.fourierIntegral f w = VectorFourier.fourierIntegral Real.fourierChar MeasureTheory.volume (innerₗ V) f w

def Real.fourierIntegralInv {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] (f : V → E) (w : V) : E

The inverse Fourier transform of a function on an inner product space, defined as the Fourier transform but with opposite sign in the exponential.

Equations

• Real.fourierIntegralInv f w = VectorFourier.fourierIntegral Real.fourierChar MeasureTheory.volume (-innerₗ V) f w

def FourierTransform.term𝓕 : Lean.ParserDescr

The Fourier transform of a function on an inner product space, with respect to the standard additive character ω ↦ exp (2 i π ω).

Equations

• FourierTransform.term𝓕 = Lean.ParserDescr.node `FourierTransform.term𝓕 1024 (Lean.ParserDescr.symbol "𝓕")

def FourierTransform.«term𝓕⁻» : Lean.ParserDescr

The inverse Fourier transform of a function on an inner product space, defined as the Fourier transform but with opposite sign in the exponential.

Equations

• FourierTransform.«term𝓕⁻» = Lean.ParserDescr.node `FourierTransform.term𝓕⁻ 1024 (Lean.ParserDescr.symbol "𝓕⁻")

theorem Real.fourierIntegral_eq {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] (f : V → E) (w : V) : Real.fourierIntegral f w = ∫ (v : V), Real.fourierChar (-⟪v, w⟫_ℝ) • f v

theorem Real.fourierIntegral_eq' {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] (f : V → E) (w : V) : Real.fourierIntegral f w = ∫ (v : V), Complex.exp (↑(-2 * Real.pi * ⟪v, w⟫_ℝ) * Complex.I) • f v

theorem Real.fourierIntegralInv_eq {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] (f : V → E) (w : V) : Real.fourierIntegralInv f w = ∫ (v : V), Real.fourierChar ⟪v, w⟫_ℝ • f v

theorem Real.fourierIntegralInv_eq' {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] (f : V → E) (w : V) : Real.fourierIntegralInv f w = ∫ (v : V), Complex.exp (↑(2 * Real.pi * ⟪v, w⟫_ℝ) * Complex.I) • f v

theorem Real.fourierIntegralInv_eq_fourierIntegral_neg {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] (f : V → E) (w : V) : Real.fourierIntegralInv f w = Real.fourierIntegral f (-w)

theorem Real.fourierIntegral_comp_linearIsometry {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] {W : Type u_4} [NormedAddCommGroup W] [InnerProductSpace ℝ W] [MeasurableSpace W] [BorelSpace W] [FiniteDimensional ℝ W] (A : W ≃ₗᵢ[ℝ] V) (f : V → E) (w : W) : Real.fourierIntegral (f ∘ ⇑A) w = Real.fourierIntegral f (A w)

theorem Real.fourierIntegralInv_comp_linearIsometry {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] {W : Type u_4} [NormedAddCommGroup W] [InnerProductSpace ℝ W] [MeasurableSpace W] [BorelSpace W] [FiniteDimensional ℝ W] (A : W ≃ₗᵢ[ℝ] V) (f : V → E) (w : W) : Real.fourierIntegralInv (f ∘ ⇑A) w = Real.fourierIntegralInv f (A w)

theorem Real.fourierIntegral_real_eq {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℝ → E) (w : ℝ) : Real.fourierIntegral f w = ∫ (v : ℝ), Real.fourierChar (-(v * w)) • f v

@[deprecated Real.fourierIntegral_real_eq]

theorem Real.fourierIntegral_def {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℝ → E) (w : ℝ) : Real.fourierIntegral f w = ∫ (v : ℝ), Real.fourierChar (-(v * w)) • f v

Alias of Real.fourierIntegral_real_eq.

theorem Real.fourierIntegral_real_eq_integral_exp_smul {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℝ → E) (w : ℝ) : Real.fourierIntegral f w = ∫ (v : ℝ), Complex.exp (↑(-2 * Real.pi * v * w) * Complex.I) • f v

@[deprecated Real.fourierIntegral_real_eq_integral_exp_smul]

theorem Real.fourierIntegral_eq_integral_exp_smul {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℝ → E) (w : ℝ) : Real.fourierIntegral f w = ∫ (v : ℝ), Complex.exp (↑(-2 * Real.pi * v * w) * Complex.I) • f v

Alias of Real.fourierIntegral_real_eq_integral_exp_smul.