# 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} [] [Module π V] [] {W : Type u_3} [] [Module π W] {E : Type u_4} [] (e : AddChar π β₯circle) (ΞΌ : ) (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
• = β« (v : V), e (-(L v) w) β’ f v βΞΌ
Instances For
theorem VectorFourier.fourierIntegral_smul_const {π : Type u_1} [CommRing π] {V : Type u_2} [] [Module π V] [] {W : Type u_3} [] [Module π W] {E : Type u_4} [] (e : AddChar π β₯circle) (ΞΌ : ) (L : V ββ[π] W ββ[π] π) (f : V β E) (r : β) :
theorem VectorFourier.norm_fourierIntegral_le_integral_norm {π : Type u_1} [CommRing π] {V : Type u_2} [] [Module π V] [] {W : Type u_3} [] [Module π W] {E : Type u_4} [] (e : AddChar π β₯circle) (ΞΌ : ) (L : V ββ[π] W ββ[π] π) (f : V β E) (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} [CommRing π] {V : Type u_2} [] [Module π V] [] {W : Type u_3} [] [Module π W] {E : Type u_4} [] [] (e : AddChar π β₯circle) (ΞΌ : ) [ΞΌ.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) β’

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

In this section we assume π, V, W have topologies, and L, e are continuous (but f needn't be). This is used to ensure that e (-L v w) is (a.e. strongly) measurable. We could get away with imposing only a measurable-space structure on π (it doesn't have to be the Borel sigma-algebra of a topology); but it seems hard to imagine cases where this extra generality would be useful, and allowing it would complicate matters in the most important use cases.

theorem VectorFourier.fourierIntegral_convergent_iff {π : Type u_1} [CommRing π] {V : Type u_2} [] [Module π V] [] {W : Type u_3} [] [Module π W] {E : Type u_4} [] [TopologicalSpace π] [TopologicalRing π] [] [] [] {e : AddChar π β₯circle} {ΞΌ : } {L : V ββ[π] W ββ[π] π} (he : Continuous βe) (hL : Continuous fun (p : V Γ W) => (L p.1) p.2) {f : V β E} (w : W) :
MeasureTheory.Integrable (fun (v : V) => e (-(L v) w) β’ f v) ΞΌ β

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

@[deprecated VectorFourier.fourierIntegral_convergent_iff]
theorem VectorFourier.fourier_integral_convergent_iff {π : Type u_1} [CommRing π] {V : Type u_2} [] [Module π V] [] {W : Type u_3} [] [Module π W] {E : Type u_4} [] [TopologicalSpace π] [TopologicalRing π] [] [] [] {e : AddChar π β₯circle} {ΞΌ : } {L : V ββ[π] W ββ[π] π} (he : Continuous βe) (hL : Continuous fun (p : V Γ W) => (L p.1) p.2) {f : V β E} (w : W) :
MeasureTheory.Integrable (fun (v : V) => e (-(L v) w) β’ f v) ΞΌ β

Alias of VectorFourier.fourierIntegral_convergent_iff.

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

theorem VectorFourier.fourierIntegral_add {π : Type u_1} [CommRing π] {V : Type u_2} [] [Module π V] [] {W : Type u_3} [] [Module π W] {E : Type u_4} [] [TopologicalSpace π] [TopologicalRing π] [] [] [] {e : AddChar π β₯circle} {ΞΌ : } {L : V ββ[π] W ββ[π] π} (he : Continuous βe) (hL : Continuous fun (p : V Γ W) => (L p.1) p.2) {f : V β E} {g : V β E} (hf : ) (hg : ) :
theorem VectorFourier.fourierIntegral_continuous {π : Type u_1} [CommRing π] {V : Type u_2} [] [Module π V] [] {W : Type u_3} [] [Module π W] {E : Type u_4} [] [TopologicalSpace π] [TopologicalRing π] [] [] [] {e : AddChar π β₯circle} {ΞΌ : } {L : V ββ[π] W ββ[π] π} (he : Continuous βe) (hL : Continuous fun (p : V Γ W) => (L p.1) p.2) {f : V β E} (hf : ) :

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} [] [Module π V] [] {W : Type u_3} [] [Module π W] {E : Type u_4} {F : Type u_5} {G : Type u_6} [] [] [] [TopologicalSpace π] [TopologicalRing π] [] [] [] [] [] {e : AddChar π β₯circle} {ΞΌ : } {L : V ββ[π] W ββ[π] π} {Ξ½ : } [] [] {f : V β E} {g : W β F} (M : E βL[β] ) (he : Continuous βe) (hL : Continuous fun (p : V Γ W) => (L p.1) p.2) (hf : ) (hg : ) :
β« (ΞΎ : W), (M ()) (g ΞΎ) βΞ½ = β« (x : V), (M (f x)) (VectorFourier.fourierIntegral e Ξ½ L.flip 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} [] [Module π V] [] {W : Type u_3} [] [Module π W] {F : Type u_5} [] [TopologicalSpace π] [TopologicalRing π] [] [] [] [] [] {e : AddChar π β₯circle} {ΞΌ : } {L : V ββ[π] W ββ[π] π} {Ξ½ : } [] {f : V β β} {g : W β F} (he : Continuous βe) (hL : Continuous fun (p : V Γ W) => (L p.1) p.2) (hf : ) (hg : ) :
β« (ΞΎ : W), β’ g ΞΎ βΞ½ = β« (x : V), f x β’ VectorFourier.fourierIntegral e Ξ½ L.flip g x βΞΌ

The Fourier transform satisfies β« π f * g = β« f * π g, i.e., it is self-adjoint.

theorem VectorFourier.fourierIntegral_continuousLinearMap_apply {π : Type u_1} {E : Type u_3} {F : Type u_4} {V : Type u_5} {W : Type u_6} [] [NormedSpace π V] [] [] [NormedSpace π W] {e : AddChar π β₯circle} {ΞΌ : } {L : V βL[π] W βL[π] π} [] [] {f : V β } {a : F} {w : W} (he : Continuous βe) (hf : ) :
(VectorFourier.fourierIntegral e ΞΌ L.toLinearMapβ f w) a = VectorFourier.fourierIntegral e ΞΌ L.toLinearMapβ (fun (x : V) => (f x) a) w
theorem VectorFourier.fourierIntegral_continuousMultilinearMap_apply {π : Type u_1} {ΞΉ : Type u_2} {E : Type u_3} {V : Type u_5} {W : Type u_6} [Fintype ΞΉ] [] [NormedSpace π V] [] [] [NormedSpace π W] {e : AddChar π β₯circle} {ΞΌ : } {L : V βL[π] W βL[π] π} [] {M : ΞΉ β Type u_7} [(i : ΞΉ) β NormedAddCommGroup (M i)] [(i : ΞΉ) β NormedSpace β (M i)] {f : V β } {m : (i : ΞΉ) β M i} {w : W} (he : Continuous βe) (hf : ) :
(VectorFourier.fourierIntegral e ΞΌ L.toLinearMapβ f w) m = VectorFourier.fourierIntegral e ΞΌ L.toLinearMapβ (fun (x : V) => (f x) m) w

## Fourier theory for functions on π#

def Fourier.fourierIntegral {π : Type u_1} [CommRing π] [MeasurableSpace π] {E : Type u_2} [] (e : AddChar π β₯circle) (ΞΌ : ) (f : π β E) (w : π) :
E

The Fourier transform integral for f : π β E, with respect to the measure ΞΌ and additive character e.

Equations
Instances For
theorem Fourier.fourierIntegral_def {π : Type u_1} [CommRing π] [MeasurableSpace π] {E : Type u_2} [] (e : AddChar π β₯circle) (ΞΌ : ) (f : π β E) (w : π) :
= β« (v : π), e (-(v * w)) β’ f v βΞΌ
theorem Fourier.fourierIntegral_smul_const {π : Type u_1} [CommRing π] [MeasurableSpace π] {E : Type u_2} [] (e : AddChar π β₯circle) (ΞΌ : ) (f : π β E) (r : β) :
theorem Fourier.norm_fourierIntegral_le_integral_norm {π : Type u_1} [CommRing π] [MeasurableSpace π] {E : Type u_2} [] (e : AddChar π β₯circle) (ΞΌ : ) (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} [CommRing π] [MeasurableSpace π] {E : Type u_2} [] [MeasurableAdd π] (e : AddChar π β₯circle) (ΞΌ : ) [ΞΌ.IsAddRightInvariant] (f : π β E) (vβ : π) :
Fourier.fourierIntegral e ΞΌ (f β fun (v : π) => v + vβ) = fun (w : π) => e (vβ * w) β’

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

The standard additive character of β, given by fun x β¦ exp (2 * Ο * x * I).

Equations
Instances For

The standard additive character of β, given by fun x β¦ exp (2 * Ο * x * I).

Equations
Instances For
theorem Real.fourierChar_apply (x : β) :
β(Real.fourierChar 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 : ) (ΞΌ : ) (f : V β E) (w : W) :
= β« (v : V), Complex.exp (β(-2 * Real.pi * (L v) w) * Complex.I) β’ f v βΞΌ
@[simp]
theorem Real.fourierIntegral_convergent_iff' {E : Type u_1} [] {V : Type u_2} {W : Type u_3} [] [] [] [] {ΞΌ : } {f : V β E} (L : ) (w : W) :
MeasureTheory.Integrable (fun (v : V) => Real.fourierChar (-(L v) w) β’ f v) ΞΌ β

The Fourier integral is well defined iff the function is integrable. Version with a general continuous bilinear function L. For the specialization to the inner product in an inner product space, see Real.fourierIntegral_convergent_iff.

theorem Real.fourierIntegral_continuousLinearMap_apply' {E : Type u_1} {F : Type u_3} {V : Type u_4} {W : Type u_5} [] [] [] [] {ΞΌ : } {L : } [] [] {f : V β } {a : F} {w : W} (hf : ) :
(VectorFourier.fourierIntegral Real.fourierChar ΞΌ L.toLinearMapβ f w) a = VectorFourier.fourierIntegral Real.fourierChar ΞΌ L.toLinearMapβ (fun (x : V) => (f x) a) w
theorem Real.fourierIntegral_continuousMultilinearMap_apply' {E : Type u_1} {ΞΉ : Type u_2} {V : Type u_4} {W : Type u_5} [Fintype ΞΉ] [] [] [] [] {ΞΌ : } {L : } [] {M : ΞΉ β Type u_6} [(i : ΞΉ) β NormedAddCommGroup (M i)] [(i : ΞΉ) β NormedSpace β (M i)] {f : V β } {m : (i : ΞΉ) β M i} {w : W} (hf : ) :
(VectorFourier.fourierIntegral Real.fourierChar ΞΌ L.toLinearMapβ f w) m = VectorFourier.fourierIntegral Real.fourierChar ΞΌ L.toLinearMapβ (fun (x : V) => (f x) m) w
def Real.fourierIntegral {E : Type u_1} [] {V : Type u_2} [] [] [] [] (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
Instances For
def Real.fourierIntegralInv {E : Type u_1} [] {V : Type u_2} [] [] [] [] (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
Instances For

The Fourier transform of a function on an inner product space, with respect to the standard additive character Ο β¦ exp (2 i Ο Ο).

Equations
Instances For

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
Instances For
theorem Real.fourierIntegral_eq {E : Type u_1} [] {V : Type u_2} [] [] [] [] (f : V β E) (w : V) :
= β« (v : V), Real.fourierChar (-βͺv, wβ«_β) β’ f v
theorem Real.fourierIntegral_eq' {E : Type u_1} [] {V : Type u_2} [] [] [] [] (f : V β E) (w : V) :
= β« (v : V), Complex.exp (β(-2 * Real.pi * βͺv, wβ«_β) * Complex.I) β’ f v
theorem Real.fourierIntegralInv_eq {E : Type u_1} [] {V : Type u_2} [] [] [] [] (f : V β E) (w : V) :
= β« (v : V), Real.fourierChar βͺv, wβ«_β β’ f v
theorem Real.fourierIntegralInv_eq' {E : Type u_1} [] {V : Type u_2} [] [] [] [] (f : V β E) (w : V) :
= β« (v : V), Complex.exp (β( * βͺv, wβ«_β) * Complex.I) β’ f v
theorem Real.fourierIntegral_comp_linearIsometry {E : Type u_1} [] {V : Type u_2} [] [] [] [] {W : Type u_3} [] [] [] [] (A : ) (f : V β E) (w : W) :
theorem Real.fourierIntegralInv_eq_fourierIntegral_neg {E : Type u_1} [] {V : Type u_2} [] [] [] [] (f : V β E) (w : V) :
theorem Real.fourierIntegralInv_eq_fourierIntegral_comp_neg {E : Type u_1} [] {V : Type u_2} [] [] [] [] (f : V β E) :
= Real.fourierIntegral fun (x : V) => f (-x)
theorem Real.fourierIntegralInv_comm {E : Type u_1} [] {V : Type u_2} [] [] [] [] (f : V β E) :
theorem Real.fourierIntegralInv_comp_linearIsometry {E : Type u_1} [] {V : Type u_2} [] [] [] [] {W : Type u_3} [] [] [] [] (A : ) (f : V β E) (w : W) :
theorem Real.fourierIntegral_real_eq {E : Type u_1} [] (f : β β E) (w : β) :
= β« (v : β), Real.fourierChar (-(v * w)) β’ f v
@[deprecated Real.fourierIntegral_real_eq]
theorem Real.fourierIntegral_def {E : Type u_1} [] (f : β β E) (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_1} [] (f : β β E) (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_1} [] (f : β β E) (w : β) :
= β« (v : β), Complex.exp (β(-2 * Real.pi * v * w) * Complex.I) β’ f v

Alias of Real.fourierIntegral_real_eq_integral_exp_smul.

@[simp]
theorem Real.fourierIntegral_convergent_iff {E : Type u_1} [] {V : Type u_2} [] [] [] {ΞΌ : } {f : V β E} (w : V) :
MeasureTheory.Integrable (fun (v : V) => Real.fourierChar (-βͺv, wβ«_β) β’ f v) ΞΌ β
theorem Real.fourierIntegral_continuousLinearMap_apply {E : Type u_1} [] {V : Type u_2} [] [] [] [] {F : Type u_4} [] {f : V β } {a : F} {v : V} (hf : MeasureTheory.Integrable f MeasureTheory.volume) :
() a = Real.fourierIntegral (fun (x : V) => (f x) a) v
theorem Real.fourierIntegral_continuousMultilinearMap_apply {E : Type u_1} [] {V : Type u_2} [] [] [] [] {ΞΉ : Type u_4} [Fintype ΞΉ] {M : ΞΉ β Type u_5} [(i : ΞΉ) β NormedAddCommGroup (M i)] [(i : ΞΉ) β NormedSpace β (M i)] {f : V β } {m : (i : ΞΉ) β M i} {v : V} (hf : MeasureTheory.Integrable f MeasureTheory.volume) :
() m = Real.fourierIntegral (fun (x : V) => (f x) m) v