Type classes for the Fourier transform #

In this file we define type classes for the Fourier transform and the inverse Fourier transform. We introduce the notation 𝓕 and 𝓕⁻ in these classes to denote the Fourier transform and the inverse Fourier transform, respectively.

Moreover, we provide type-classes that encode the linear structure and the Fourier inversion theorem.

source

class FourierTransform (E : Type u) (F : outParam (Type v)) :

Type (max u v)

The notation typeclass for the Fourier transform.

While the Fourier transform is a linear operator, the notation is for the function E → F without any additional properties. This makes it possible to use the notation for functions where integrability is an issue. Moreover, including a scalar multiplication causes problems for inferring the notation type class.

fourier : E → F
𝓕 f is the Fourier transform of f. The meaning of this notation is type-dependent.

Instances

source

class FourierTransformInv (E : Type u) (F : outParam (Type v)) :

Type (max u v)

The notation typeclass for the inverse Fourier transform.

While the inverse Fourier transform is a linear operator, the notation is for the function E → F without any additional properties. This makes it possible to use the notation for functions where integrability is an issue. Moreover, including a scalar multiplication causes problems for inferring the notation type class.

fourierInv : E → F
𝓕⁻ f is the inverse Fourier transform of f. The meaning of this notation is type-dependent.

Instances

source

def FourierTransform.term𝓕 :

Lean.ParserDescr

𝓕 f is the Fourier transform of f. The meaning of this notation is type-dependent.

Equations

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

Instances For

source

def FourierTransform.«term𝓕⁻» :

Lean.ParserDescr

𝓕⁻ f is the inverse Fourier transform of f. The meaning of this notation is type-dependent.

Equations

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

Instances For

source

class FourierAdd (E : Type u_4) (F : outParam (Type u_5)) [Add E] [Add F] [FourierTransform E F] :

Prop

A FourierAdd is a function space on which the Fourier transform is additive.

fourier_add (f g : E) : FourierTransform.fourier (f + g) = FourierTransform.fourier f + FourierTransform.fourier g

Instances

source

class FourierSMul (R : Type u_4) (E : Type u_5) (F : outParam (Type u_6)) [SMul R E] [SMul R F] [FourierTransform E F] :

Prop

A FourierSMul is a function space on which the Fourier transform is homogeneous.

fourier_smul (r : R) (f : E) : FourierTransform.fourier (r • f) = r • FourierTransform.fourier f

Instances

source

class ContinuousFourier (E : Type u_4) (F : outParam (Type u_5)) [TopologicalSpace E] [TopologicalSpace F] [FourierTransform E F] :

Prop

The Fourier transform is continuous.

continuous_fourier : Continuous FourierTransform.fourier

Instances

source

class FourierInvAdd (E : Type u_4) (F : outParam (Type u_5)) [Add E] [Add F] [FourierTransformInv E F] :

Prop

A FourierInvAdd is a function space on which the inverse Fourier transform is additive.

fourierInv_add (f g : E) : FourierTransformInv.fourierInv (f + g) = FourierTransformInv.fourierInv f + FourierTransformInv.fourierInv g

Instances

source

class FourierInvSMul (R : Type u_4) (E : Type u_5) (F : outParam (Type u_6)) [SMul R E] [SMul R F] [FourierTransformInv E F] :

Prop

A FourierInvSMul is a function space on which the inverse Fourier transform is homogeneous.

fourierInv_smul (r : R) (f : E) : FourierTransformInv.fourierInv (r • f) = r • FourierTransformInv.fourierInv f

Instances

source

class ContinuousFourierInv (E : Type u_4) (F : outParam (Type u_5)) [TopologicalSpace E] [TopologicalSpace F] [FourierTransformInv E F] :

Prop

The inverse Fourier transform is continuous.

continuous_fourierInv : Continuous FourierTransformInv.fourierInv

Instances

source

@[deprecated "use `FourierAdd` and `FourierSMul` instead" (since := "2026-01-06")]

structure FourierModule (R : Type u_4) (E : Type u_5) (F : outParam (Type u_6)) [Add E] [Add F] [SMul R E] [SMul R F] extends FourierTransform E F :

Type (max u_5 u_6)

A FourierModule is a function space on which the Fourier transform is a linear map.

fourier : E → F
fourier_add (f g : E) : FourierTransform.fourier (f + g) = FourierTransform.fourier f + FourierTransform.fourier g
fourier_smul (r : R) (f : E) : FourierTransform.fourier (r • f) = r • FourierTransform.fourier f

Instances For

source

@[deprecated "use `FourierInvAdd` and `FourierInvSMul` instead" (since := "2026-01-06")]

structure FourierInvModule (R : Type u_4) (E : Type u_5) (F : outParam (Type u_6)) [Add E] [Add F] [SMul R E] [SMul R F] extends FourierTransformInv E F :

Type (max u_5 u_6)

A FourierInvModule is a function space on which the Fourier transform is a linear map.

fourierInv : E → F
fourierInv_add (f g : E) : FourierTransformInv.fourierInv (f + g) = FourierTransformInv.fourierInv f + FourierTransformInv.fourierInv g
fourierInv_smul (r : R) (f : E) : FourierTransformInv.fourierInv (r • f) = r • FourierTransformInv.fourierInv f

Instances For

source

def FourierTransform.fourierₗ (R : Type u_1) (E : Type u_2) {F : Type u_3} [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] [FourierTransform E F] [FourierAdd E F] [FourierSMul R E F] :

E →ₗ[R] F

The Fourier transform as a linear map.

Equations

FourierTransform.fourierₗ R E = { toFun := FourierTransform.fourier, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

@[simp]

theorem FourierTransform.fourierₗ_apply {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] [FourierTransform E F] [FourierAdd E F] [FourierSMul R E F] (f : E) :

(fourierₗ R E) f = fourier f

source

theorem FourierTransform.fourier_zero (R : Type u_1) {E : Type u_2} {F : Type u_3} [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] [FourierTransform E F] [FourierAdd E F] [FourierSMul R E F] :

fourier 0 = 0

source

def FourierTransform.fourierCLM (R : Type u_1) (E : Type u_2) {F : Type u_3} [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] [FourierTransform E F] [FourierAdd E F] [FourierSMul R E F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousFourier E F] :

E →L[R] F

The Fourier transform as a continuous linear map.

Equations

FourierTransform.fourierCLM R E = { toLinearMap := FourierTransform.fourierₗ R E, cont := ⋯ }

Instances For

source

@[simp]

theorem FourierTransform.fourierCLM_apply {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] [FourierTransform E F] [FourierAdd E F] [FourierSMul R E F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousFourier E F] (f : E) :

(fourierCLM R E) f = fourier f

source

def FourierTransform.fourierInvₗ (R : Type u_1) (E : Type u_2) {F : Type u_3} [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] [FourierTransformInv E F] [FourierInvAdd E F] [FourierInvSMul R E F] :

E →ₗ[R] F

The inverse Fourier transform as a linear map.

Equations

FourierTransform.fourierInvₗ R E = { toFun := FourierTransformInv.fourierInv, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

@[simp]

theorem FourierTransform.fourierInvₗ_apply {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] [FourierTransformInv E F] [FourierInvAdd E F] [FourierInvSMul R E F] (f : E) :

(fourierInvₗ R E) f = fourierInv f

source

theorem FourierTransform.fourierInv_zero (R : Type u_1) {E : Type u_2} {F : Type u_3} [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] [FourierTransformInv E F] [FourierInvAdd E F] [FourierInvSMul R E F] :

fourierInv 0 = 0

source

def FourierTransform.fourierInvCLM (R : Type u_1) (E : Type u_2) {F : Type u_3} [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] [FourierTransformInv E F] [FourierInvAdd E F] [FourierInvSMul R E F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousFourierInv E F] :

E →L[R] F

The inverse Fourier transform as a continuous linear map.

Equations

FourierTransform.fourierInvCLM R E = { toFun := FourierTransformInv.fourierInv, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

Instances For

source

@[simp]

theorem FourierTransform.fourierInvCLM_apply {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] [FourierTransformInv E F] [FourierInvAdd E F] [FourierInvSMul R E F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousFourierInv E F] (f : E) :

(fourierInvCLM R E) f = fourierInv f

source

class FourierPair (E : Type u_4) (F : Type u_5) [FourierTransform E F] [FourierTransformInv F E] :

Prop

A FourierPair is a pair of spaces E and F such that 𝓕⁻ ∘ 𝓕 = id on E.

fourierInv_fourier_eq (f : E) : FourierTransformInv.fourierInv (FourierTransform.fourier f) = f

Instances

source

class FourierInvPair (E : Type u_4) (F : Type u_5) [FourierTransform F E] [FourierTransformInv E F] :

Prop

A FourierInvPair is a pair of spaces E and F such that 𝓕 ∘ 𝓕⁻ = id on E.

fourier_fourierInv_eq (f : E) : FourierTransform.fourier (FourierTransformInv.fourierInv f) = f

Instances

source

def FourierTransform.fourierEquiv (R : Type u_4) (E : Type u_5) {F : Type u_6} [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] [FourierTransform E F] [FourierAdd E F] [FourierSMul R E F] [FourierTransformInv F E] [FourierPair E F] [FourierInvPair F E] :

E ≃ₗ[R] F

The Fourier transform as a linear equivalence.

Equations

FourierTransform.fourierEquiv R E = { toLinearMap := FourierTransform.fourierₗ R E, invFun := FourierTransformInv.fourierInv, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem FourierTransform.fourierEquiv_apply {R : Type u_4} {E : Type u_5} {F : Type u_6} [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] [FourierTransform E F] [FourierAdd E F] [FourierSMul R E F] [FourierTransformInv F E] [FourierPair E F] [FourierInvPair F E] (f : E) :

(fourierEquiv R E) f = fourier f

source

@[simp]

theorem FourierTransform.fourierEquiv_symm_apply {R : Type u_4} {E : Type u_5} {F : Type u_6} [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] [FourierTransform E F] [FourierAdd E F] [FourierSMul R E F] [FourierTransformInv F E] [FourierPair E F] [FourierInvPair F E] (f : F) :

(fourierEquiv R E).symm f = fourierInv f

source

def FourierTransform.fourierCLE (R : Type u_4) (E : Type u_5) {F : Type u_6} [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] [FourierTransform E F] [FourierAdd E F] [FourierSMul R E F] [FourierTransformInv F E] [FourierPair E F] [FourierInvPair F E] [TopologicalSpace E] [TopologicalSpace F] [ContinuousFourier E F] [ContinuousFourierInv F E] :

E ≃L[R] F

The Fourier transform as a continuous linear equivalence.

Equations

FourierTransform.fourierCLE R E = { toLinearEquiv := FourierTransform.fourierEquiv R E, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source

@[simp]

theorem FourierTransform.fourierCLE_apply {R : Type u_4} {E : Type u_5} {F : Type u_6} [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] [FourierTransform E F] [FourierAdd E F] [FourierSMul R E F] [FourierTransformInv F E] [FourierPair E F] [FourierInvPair F E] [TopologicalSpace E] [TopologicalSpace F] [ContinuousFourier E F] [ContinuousFourierInv F E] (f : E) :

(fourierCLE R E) f = fourier f

source

@[simp]

theorem FourierTransform.fourierCLE_symm_apply {R : Type u_4} {E : Type u_5} {F : Type u_6} [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] [FourierTransform E F] [FourierAdd E F] [FourierSMul R E F] [FourierTransformInv F E] [FourierPair E F] [FourierInvPair F E] [TopologicalSpace E] [TopologicalSpace F] [ContinuousFourier E F] [ContinuousFourierInv F E] (f : F) :

(fourierCLE R E).symm f = fourierInv f

Documentation

Mathlib.Analysis.Fourier.Notation

Type classes for the Fourier transform #