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.

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.

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.

def FourierTransform.term𝓕 : Lean.ParserDescr

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

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

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

class FourierAdd (E : Type u_5) (F : outParam (Type u_6)) [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

class FourierSMul (R : Type u_5) (E : Type u_6) (F : outParam (Type u_7)) [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

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

The Fourier transform is continuous.

• continuous_fourier : Continuous FourierTransform.fourier

class FourierInvAdd (E : Type u_5) (F : outParam (Type u_6)) [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

class FourierInvSMul (R : Type u_5) (E : Type u_6) (F : outParam (Type u_7)) [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

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

The inverse Fourier transform is continuous.

• continuous_fourierInv : Continuous FourierTransformInv.fourierInv

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

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

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

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

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

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

@[simp]

theorem FourierTransform.fourier_zero {E : Type u_3} {F : Type u_4} [AddCommGroup E] [AddCommGroup F] [FourierTransform E F] [FourierAdd E F] : fourier 0 = 0

@[simp]

theorem FourierTransform.fourier_neg {E : Type u_3} {F : Type u_4} [AddCommGroup E] [AddCommGroup F] [FourierTransform E F] [FourierAdd E F] (f : E) : fourier (-f) = -fourier f

@[simp]

theorem FourierTransform.fourier_sum {ι : Type u_1} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [AddCommGroup F] [FourierTransform E F] [FourierAdd E F] (f : ι → E) (s : Finset ι) : fourier (∑ i ∈ s, f i) = ∑ i ∈ s, fourier (f i)

@[simp]

theorem FourierTransform.fourierInv_zero {E : Type u_3} {F : Type u_4} [AddCommGroup E] [AddCommGroup F] [FourierTransformInv E F] [FourierInvAdd E F] : fourierInv 0 = 0

@[simp]

theorem FourierTransform.fourierInv_neg {E : Type u_3} {F : Type u_4} [AddCommGroup E] [AddCommGroup F] [FourierTransformInv E F] [FourierInvAdd E F] (f : E) : fourierInv (-f) = -fourierInv f

@[simp]

theorem FourierTransform.fourierInv_sum {ι : Type u_1} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [AddCommGroup F] [FourierTransformInv E F] [FourierInvAdd E F] (f : ι → E) (s : Finset ι) : fourierInv (∑ i ∈ s, f i) = ∑ i ∈ s, fourierInv (f i)

def FourierTransform.fourierₗ (R : Type u_2) (E : Type u_3) {F : Type u_4} [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.

@[simp]

theorem FourierTransform.fourierₗ_apply {R : Type u_2} {E : Type u_3} {F : Type u_4} [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

def FourierTransform.fourierCLM (R : Type u_2) (E : Type u_3) {F : Type u_4} [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.

@[simp]

theorem FourierTransform.fourierCLM_apply {R : Type u_2} {E : Type u_3} {F : Type u_4} [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

def FourierTransform.fourierInvₗ (R : Type u_2) (E : Type u_3) {F : Type u_4} [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.

@[simp]

theorem FourierTransform.fourierInvₗ_apply {R : Type u_2} {E : Type u_3} {F : Type u_4} [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

def FourierTransform.fourierInvCLM (R : Type u_2) (E : Type u_3) {F : Type u_4} [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.

@[simp]

theorem FourierTransform.fourierInvCLM_apply {R : Type u_2} {E : Type u_3} {F : Type u_4} [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

class FourierPair (E : Type u_5) (F : Type u_6) [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

class FourierInvPair (E : Type u_5) (F : Type u_6) [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

def FourierTransform.fourierEquiv (R : Type u_5) (E : Type u_6) {F : Type u_7} [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.

@[simp]

theorem FourierTransform.fourierEquiv_apply {R : Type u_5} {E : Type u_6} {F : Type u_7} [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

@[simp]

theorem FourierTransform.fourierEquiv_symm_apply {R : Type u_5} {E : Type u_6} {F : Type u_7} [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

def FourierTransform.fourierCLE (R : Type u_5) (E : Type u_6) {F : Type u_7} [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.

@[simp]

theorem FourierTransform.fourierCLE_apply {R : Type u_5} {E : Type u_6} {F : Type u_7} [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

@[simp]

theorem FourierTransform.fourierCLE_symm_apply {R : Type u_5} {E : Type u_6} {F : Type u_7} [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