Documentation

Mathlib.Analysis.Fourier.FourierTransform

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. a homomorphism (Multiplicative 𝕜) →* 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 ∂μ,

where e [x] is notational sugar for (e (Multiplicative.ofAdd x) : ℂ) (available in locale fourier_transform). 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). The Fourier integral in this case is defined as Real.fourierIntegral.

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).

def FourierTransform.«term_[_]» :

Lean.TrailingParserDescr

Instances For

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 : Multiplicative 𝕜 →* { x // x ∈ 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.

Instances For

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 : Multiplicative 𝕜 →* { x // x ∈ 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 : Multiplicative 𝕜 →* { x // x ∈ 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 : Multiplicative 𝕜 →* { x // x ∈ circle }) (μ : MeasureTheory.Measure V) [MeasureTheory.Measure.IsAddRightInvariant μ] (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V → E) (v₀ : V) :

VectorFourier.fourierIntegral e μ L (f ∘ fun v => v + v₀) = fun w => ↑(↑e (↑Multiplicative.ofAdd (↑(↑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 : Multiplicative 𝕜 →* { x // x ∈ circle }} {μ : MeasureTheory.Measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜} (he : Continuous ↑e) (hL : Continuous fun p => ↑(↑L p.fst) p.snd) {f : V → E} (w : W) :

MeasureTheory.Integrable f ↔ MeasureTheory.Integrable fun v => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑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 : Multiplicative 𝕜 →* { x // x ∈ circle }} {μ : MeasureTheory.Measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜} (he : Continuous ↑e) (hL : Continuous fun p => ↑(↑L p.fst) p.snd) {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 : Multiplicative 𝕜 →* { x // x ∈ circle }} {μ : MeasureTheory.Measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜} [TopologicalSpace.FirstCountableTopology W] (he : Continuous ↑e) (hL : Continuous fun p => ↑(↑L p.fst) p.snd) {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.

Fourier theory for functions on `𝕜` #

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

E

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

Instances For

theorem Fourier.fourierIntegral_def {𝕜 : Type u_1} [CommRing 𝕜] [MeasurableSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] (e : Multiplicative 𝕜 →* { x // x ∈ circle }) (μ : MeasureTheory.Measure 𝕜) (f : 𝕜 → E) (w : 𝕜) :

Fourier.fourierIntegral e μ f w = ∫ (v : 𝕜), ↑(↑e (↑Multiplicative.ofAdd (-(v * w)))) • f v ∂μ

theorem Fourier.fourierIntegral_smul_const {𝕜 : Type u_1} [CommRing 𝕜] [MeasurableSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] (e : Multiplicative 𝕜 →* { x // x ∈ 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 : Multiplicative 𝕜 →* { x // x ∈ 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 : Multiplicative 𝕜 →* { x // x ∈ circle }) (μ : MeasureTheory.Measure 𝕜) [MeasureTheory.Measure.IsAddRightInvariant μ] (f : 𝕜 → E) (v₀ : 𝕜) :

Fourier.fourierIntegral e μ (f ∘ fun v => v + v₀) = fun w => ↑(↑e (↑Multiplicative.ofAdd (v₀ * w))) • Fourier.fourierIntegral e μ f w

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

def Real.fourierChar :

Multiplicative ℝ →* { x // x ∈ circle }

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

Instances For

theorem Real.fourierChar_apply (x : ℝ) :

↑(↑Real.fourierChar (↑Multiplicative.ofAdd 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_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℝ → E) (w : ℝ) :

E

The Fourier integral for f : ℝ → E, with respect to the standard additive character and measure on ℝ.

Instances For

theorem Real.fourierIntegral_def {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℝ → E) (w : ℝ) :

Real.fourierIntegral f w = ∫ (v : ℝ), ↑(↑Real.fourierChar (↑Multiplicative.ofAdd (-(v * w)))) • f v

def FourierTransform.term𝓕 :

Lean.ParserDescr

Instances For

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