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

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

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

Instances

source
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

Instances

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] [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' := ⋯ }

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

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

Instances

source
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

Instances

source
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 := ⋯ }

Instances For

source
@[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
source
@[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