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.

• fourierTransform : 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.

• fourierTransformInv : 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.

Equations

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

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 "𝓕⁻")

class FourierModule (R : Type u_1) (E : Type u_2) (F : outParam (Type u_3)) [Add E] [Add F] [SMul R E] [SMul R F] extends FourierTransform E F : Type (max u_2 u_3)

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

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

class FourierInvModule (R : Type u_1) (E : Type u_2) (F : outParam (Type u_3)) [Add E] [Add F] [SMul R E] [SMul R F] extends FourierTransformInv E F : Type (max u_2 u_3)

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

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

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] [FourierModule R E F] : E →ₗ[R] F

The Fourier transform as a linear map.

Equations

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

@[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] [FourierModule R E F] (f : E) : (fourierₗ R E F) f = fourierTransform f

@[simp]

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] [FourierModule R E F] : fourierTransform 0 = 0

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] [FourierInvModule R E F] : E →ₗ[R] F

The inverse Fourier transform as a linear map.

Equations

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

@[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] [FourierInvModule R E F] (f : E) : (fourierInvₗ R E F) f = fourierTransformInv f

@[simp]

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] [FourierInvModule R E F] : fourierTransformInv 0 = 0

class FourierPair (E : Type u_1) (F : Type u_2) [FourierTransform E F] [FourierTransformInv F E] : Prop

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

• inv_fourier (f : E) : FourierTransformInv.fourierTransformInv (FourierTransform.fourierTransform f) = f

class FourierInvPair (E : Type u_1) (F : Type u_2) [FourierTransform F E] [FourierTransformInv E F] : Prop

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

• fourier_inv (f : E) : FourierTransform.fourierTransform (FourierTransformInv.fourierTransformInv f) = f

def FourierTransform.fourierEquiv (R : Type u_1) (E : Type u_2) (F : Type u_3) [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] [FourierModule R E F] [FourierInvModule R F E] [FourierPair E F] [FourierInvPair F E] : E ≃ₗ[R] F

The Fourier transform as a linear equivalence.

Equations

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

@[simp]

theorem FourierTransform.fourierEquiv_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] [FourierModule R E F] [FourierInvModule R F E] [FourierPair E F] [FourierInvPair F E] (f : E) : (fourierEquiv R E F) f = fourierTransform f

@[simp]

theorem FourierTransform.fourierEquiv_symm_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] [FourierModule R E F] [FourierInvModule R F E] [FourierPair E F] [FourierInvPair F E] (f : F) : (fourierEquiv R E F).symm f = fourierTransformInv f