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

Instances For

## Fourier theory for functions on general vector spaces #

def VectorFourier.fourierIntegral {𝕜 : Type u_1} [] {V : Type u_2} [] [Module 𝕜 V] [] {W : Type u_3} [] [Module 𝕜 W] {E : Type u_4} [] (e : →* { x // }) (μ : ) (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : VE) (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} [] {V : Type u_2} [] [Module 𝕜 V] [] {W : Type u_3} [] [Module 𝕜 W] {E : Type u_4} [] (e : →* { x // }) (μ : ) (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : VE) (r : ) :
theorem VectorFourier.norm_fourierIntegral_le_integral_norm {𝕜 : Type u_1} [] {V : Type u_2} [] [Module 𝕜 V] [] {W : Type u_3} [] [Module 𝕜 W] {E : Type u_4} [] (e : →* { x // }) (μ : ) (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : VE) (w : 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} [] {V : Type u_2} [] [Module 𝕜 V] [] {W : Type u_3} [] [Module 𝕜 W] {E : Type u_4} [] [] (e : →* { x // }) (μ : ) (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : VE) (v₀ : V) :
VectorFourier.fourierIntegral e μ L (f fun v => v + v₀) = fun w => ↑(e (Multiplicative.ofAdd (↑(L v₀) w)))

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

theorem VectorFourier.fourier_integral_convergent_iff {𝕜 : Type u_1} [] {V : Type u_2} [] [Module 𝕜 V] [] {W : Type u_3} [] [Module 𝕜 W] {E : Type u_4} [] [] [] [] [] [] {e : →* { x // }} {μ : } {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜} (he : ) (hL : Continuous fun p => ↑(L p.fst) p.snd) {f : VE} (w : W) :
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} [] {V : Type u_2} [] [Module 𝕜 V] [] {W : Type u_3} [] [Module 𝕜 W] {E : Type u_4} [] [] [] [] [] [] {e : →* { x // }} {μ : } {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜} (he : ) (hL : Continuous fun p => ↑(L p.fst) p.snd) {f : VE} {g : VE} (hf : ) (hg : ) :
theorem VectorFourier.fourierIntegral_continuous {𝕜 : Type u_1} [] {V : Type u_2} [] [Module 𝕜 V] [] {W : Type u_3} [] [Module 𝕜 W] {E : Type u_4} [] [] [] [] [] [] {e : →* { x // }} {μ : } {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜} (he : ) (hL : Continuous fun p => ↑(L p.fst) p.snd) {f : VE} (hf : ) :

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

## Fourier theory for functions on 𝕜#

def Fourier.fourierIntegral {𝕜 : Type u_1} [] [] {E : Type u_2} [] (e : →* { x // }) (μ : ) (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} [] [] {E : Type u_2} [] (e : →* { x // }) (μ : ) (f : 𝕜E) (w : 𝕜) :
= ∫ (v : 𝕜), ↑(e (Multiplicative.ofAdd (-(v * w)))) f vμ
theorem Fourier.fourierIntegral_smul_const {𝕜 : Type u_1} [] [] {E : Type u_2} [] (e : →* { x // }) (μ : ) (f : 𝕜E) (r : ) :
theorem Fourier.norm_fourierIntegral_le_integral_norm {𝕜 : Type u_1} [] [] {E : Type u_2} [] (e : →* { x // }) (μ : ) (f : 𝕜E) (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} [] [] {E : Type u_2} [] [] (e : →* { x // }) (μ : ) (f : 𝕜E) (v₀ : 𝕜) :
Fourier.fourierIntegral e μ (f fun v => v + v₀) = fun w => ↑(e (Multiplicative.ofAdd (v₀ * w)))

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

def Real.fourierChar :
→* { x // }

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 (↑( * x) * Complex.I)
theorem Real.vector_fourierIntegral_eq_integral_exp_smul {E : Type u_1} [] {V : Type u_2} [] [] [] {W : Type u_3} [] [] (L : V →ₗ[] ) (μ : ) (f : VE) (w : W) :
= ∫ (v : V), Complex.exp (↑( * ↑(L v) w) * Complex.I) f vμ
def Real.fourierIntegral {E : Type u_1} [] (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} [] (f : E) (w : ) :
= ∫ (v : ), ↑(Real.fourierChar (Multiplicative.ofAdd (-(v * w)))) f v
Instances For
theorem Real.fourierIntegral_eq_integral_exp_smul {E : Type u_2} [] (f : E) (w : ) :
= ∫ (v : ), Complex.exp (↑( * v * w) * Complex.I) f v