# 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 introduced the notation `𝐞` in the scope `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 #

source
def VectorFourier.fourierIntegral {𝕜 : Type u_1} [CommRing 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] [MeasurableSpace V] {W : Type u_3} [AddCommGroup W] [Module 𝕜 W] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℂ E] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure V) (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

- VectorFourier.fourierIntegral e μ L f w = ∫ (v : V), e (-(L v) w) • f v ∂μ

Instances For

source
theorem VectorFourier.fourierIntegral_const_smul {𝕜 : Type u_1} [CommRing 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] [MeasurableSpace V] {W : Type u_3} [AddCommGroup W] [Module 𝕜 W] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℂ E] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure V) (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V → E) (r : ℂ) :
fourierIntegral e μ L (r • f) = r • fourierIntegral e μ L f
source
theorem VectorFourier.norm_fourierIntegral_le_integral_norm {𝕜 : Type u_1} [CommRing 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] [MeasurableSpace V] {W : Type u_3} [AddCommGroup W] [Module 𝕜 W] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℂ E] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure V) (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V → E) (w : W) :
‖fourierIntegral e μ L f w‖ ≤ ∫ (v : V), ‖f v‖ ∂μ

The uniform norm of the Fourier integral of `f` is bounded by the `L¹` norm of `f`.

source
theorem VectorFourier.fourierIntegral_comp_add_right {𝕜 : Type u_1} [CommRing 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] [MeasurableSpace V] {W : Type u_3} [AddCommGroup W] [Module 𝕜 W] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℂ E] [MeasurableAdd V] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure V) [μ.IsAddRightInvariant] (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V → E) (v₀ : V) :
fourierIntegral e μ L (f ∘ fun (v : V) => v + v₀) = fun (w : W) => e ((L v₀) w) • fourierIntegral e μ L f 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.

source
theorem VectorFourier.fourierIntegral_convergent_iff {𝕜 : Type u_1} [CommRing 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] [MeasurableSpace V] {W : Type u_3} [AddCommGroup W] [Module 𝕜 W] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℂ E] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] [TopologicalSpace V] [BorelSpace V] [TopologicalSpace W] {e : AddChar 𝕜 Circle} {μ : MeasureTheory.Measure V} {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) μ ↔ MeasureTheory.Integrable f μ

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

source
theorem VectorFourier.fourierIntegral_add {𝕜 : Type u_1} [CommRing 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] [MeasurableSpace V] {W : Type u_3} [AddCommGroup W] [Module 𝕜 W] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℂ E] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] [TopologicalSpace V] [BorelSpace V] [TopologicalSpace W] {e : AddChar 𝕜 Circle} {μ : MeasureTheory.Measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜} (he : Continuous ⇑e) (hL : Continuous fun (p : V × W) => (L p.1) p.2) {f g : V → E} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) :
fourierIntegral e μ L (f + g) = fourierIntegral e μ L f + fourierIntegral e μ L g
source
theorem VectorFourier.fourierIntegral_continuous {𝕜 : Type u_1} [CommRing 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] [MeasurableSpace V] {W : Type u_3} [AddCommGroup W] [Module 𝕜 W] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℂ E] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] [TopologicalSpace V] [BorelSpace V] [TopologicalSpace W] {e : AddChar 𝕜 Circle} {μ : MeasureTheory.Measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜} [FirstCountableTopology W] (he : Continuous ⇑e) (hL : Continuous fun (p : V × W) => (L p.1) p.2) {f : V → E} (hf : MeasureTheory.Integrable f μ) :
Continuous (fourierIntegral e μ L f)

The Fourier integral of an `L^1` function is a continuous function.

source
theorem VectorFourier.integral_fourierIntegral_swap {𝕜 : Type u_1} [CommRing 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] [MeasurableSpace V] {W : Type u_3} [AddCommGroup W] [Module 𝕜 W] {E : Type u_4} {F : Type u_5} {G : Type u_6} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [NormedAddCommGroup G] [NormedSpace ℂ G] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] [TopologicalSpace V] [BorelSpace V] [TopologicalSpace W] [MeasurableSpace W] [BorelSpace W] {e : AddChar 𝕜 Circle} {μ : MeasureTheory.Measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜} {ν : MeasureTheory.Measure W} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] [SecondCountableTopology V] {σ : ℂ →+* ℂ} [RingHomIsometric σ] {f : V → E} {g : W → F} (M : F →L[ℂ] E →SL[σ] G) (he : Continuous ⇑e) (hL : Continuous fun (p : V × W) => (L p.1) p.2) (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g ν) :
∫ (ξ : W), ∫ (x : V), (M (g ξ)) (e (-(L x) ξ) • f x) ∂μ ∂ν = ∫ (x : V), ∫ (ξ : W), (M (g ξ)) (e (-(L x) ξ) • f x) ∂ν ∂μ

Fubini's theorem for the Fourier integral.

This is the main technical step in proving both Parseval's identity and self-adjointness of the Fourier transform.

source
theorem VectorFourier.integral_bilin_fourierIntegral_eq_flip {𝕜 : Type u_1} [CommRing 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] [MeasurableSpace V] {W : Type u_3} [AddCommGroup W] [Module 𝕜 W] {E : Type u_4} {F : Type u_5} {G : Type u_6} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [NormedAddCommGroup G] [NormedSpace ℂ G] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] [TopologicalSpace V] [BorelSpace V] [TopologicalSpace W] [MeasurableSpace W] [BorelSpace W] {e : AddChar 𝕜 Circle} {μ : MeasureTheory.Measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜} {ν : MeasureTheory.Measure W} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] [SecondCountableTopology V] [CompleteSpace E] [CompleteSpace F] {f : V → E} {g : W → F} (M : E →L[ℂ] F →L[ℂ] G) (he : Continuous ⇑e) (hL : Continuous fun (p : V × W) => (L p.1) p.2) (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g ν) :
∫ (ξ : W), (M (fourierIntegral e μ L f ξ)) (g ξ) ∂ν = ∫ (x : V), (M (f x)) (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`.

source
theorem VectorFourier.integral_fourierIntegral_smul_eq_flip {𝕜 : Type u_1} [CommRing 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] [MeasurableSpace V] {W : Type u_3} [AddCommGroup W] [Module 𝕜 W] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace ℂ F] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] [TopologicalSpace V] [BorelSpace V] [TopologicalSpace W] [MeasurableSpace W] [BorelSpace W] {e : AddChar 𝕜 Circle} {μ : MeasureTheory.Measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜} {ν : MeasureTheory.Measure W} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] [SecondCountableTopology V] [CompleteSpace F] {f : V → ℂ} {g : W → F} (he : Continuous ⇑e) (hL : Continuous fun (p : V × W) => (L p.1) p.2) (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g ν) :
∫ (ξ : W), fourierIntegral e μ L f ξ • g ξ ∂ν = ∫ (x : V), f x • fourierIntegral e ν L.flip g x ∂μ

The Fourier transform satisfies `∫ 𝓕 f * g = ∫ f * 𝓕 g`, i.e., it is self-adjoint.

source
theorem VectorFourier.integral_sesq_fourierIntegral_eq_neg_flip {𝕜 : Type u_1} [CommRing 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] [MeasurableSpace V] {W : Type u_3} [AddCommGroup W] [Module 𝕜 W] {E : Type u_4} {F : Type u_5} {G : Type u_6} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [NormedAddCommGroup G] [NormedSpace ℂ G] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] [TopologicalSpace V] [BorelSpace V] [TopologicalSpace W] [MeasurableSpace W] [BorelSpace W] {e : AddChar 𝕜 Circle} {μ : MeasureTheory.Measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜} {ν : MeasureTheory.Measure W} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] [SecondCountableTopology V] [CompleteSpace E] [CompleteSpace F] {f : V → E} {g : W → F} (M : E →L⋆[ℂ] F →L[ℂ] G) (he : Continuous ⇑e) (hL : Continuous fun (p : V × W) => (L p.1) p.2) (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g ν) :
∫ (ξ : W), (M (fourierIntegral e μ L f ξ)) (g ξ) ∂ν = ∫ (x : V), (M (f x)) (fourierIntegral e ν (-L.flip) g x) ∂μ

The Fourier transform satisfies `∫ 𝓕 f * conj g = ∫ f * conj (𝓕⁻¹ g)`, which together with the Fourier inversion theorem yields Plancherel's theorem. The stated version is more convenient since it does only require integrability of `f` and `g`.

Version where the multiplication is replaced by a general bilinear form `M`.

source
theorem VectorFourier.fourierIntegral_probChar {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_7} {W : Type u_8} {x✝ : MeasurableSpace V} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ) (μ : MeasureTheory.Measure V) (f : V → E) (w : W) :
fourierIntegral Real.probChar μ L f w = ∫ (v : V), Complex.exp (-↑((L v) w) * Complex.I) • f v ∂μ
source
theorem VectorFourier.fourierIntegral_continuousLinearMap_apply {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} {V : Type u_5} {W : Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] {e : AddChar 𝕜 Circle} {μ : MeasureTheory.Measure V} {L : V →L[𝕜] W →L[𝕜] 𝕜} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup E] [NormedSpace ℂ E] {f : V → F →L[ℝ] E} {a : F} {w : W} (he : Continuous ⇑e) (hf : MeasureTheory.Integrable f μ) :
(fourierIntegral e μ L.toLinearMap₁₂ f w) a = fourierIntegral e μ L.toLinearMap₁₂ (fun (x : V) => (f x) a) w
source
theorem VectorFourier.fourierIntegral_continuousMultilinearMap_apply {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {V : Type u_5} {W : Type u_6} [Fintype ι] [NontriviallyNormedField 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] {e : AddChar 𝕜 Circle} {μ : MeasureTheory.Measure V} {L : V →L[𝕜] W →L[𝕜] 𝕜} [NormedAddCommGroup E] [NormedSpace ℂ E] {M : ι → Type u_7} [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace ℝ (M i)] {f : V → ContinuousMultilinearMap ℝ M E} {m : (i : ι) → M i} {w : W} (he : Continuous ⇑e) (hf : MeasureTheory.Integrable f μ) :
(fourierIntegral e μ L.toLinearMap₁₂ f w) m = fourierIntegral e μ L.toLinearMap₁₂ (fun (x : V) => (f x) m) w

## Fourier theory for functions on `𝕜` #

source
def Fourier.fourierIntegral {𝕜 : Type u_1} [CommRing 𝕜] [MeasurableSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure 𝕜) (f : 𝕜 → E) (w : 𝕜) :
E

The Fourier transform integral for `f : 𝕜 → E`, with respect to the measure `μ` and additive character `e`.

Equations

- Fourier.fourierIntegral e μ f w = VectorFourier.fourierIntegral e μ (LinearMap.mul 𝕜 𝕜) f w

Instances For

source
theorem Fourier.fourierIntegral_def {𝕜 : Type u_1} [CommRing 𝕜] [MeasurableSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure 𝕜) (f : 𝕜 → E) (w : 𝕜) :
fourierIntegral e μ f w = ∫ (v : 𝕜), e (-(v * w)) • f v ∂μ
source
theorem Fourier.fourierIntegral_const_smul {𝕜 : Type u_1} [CommRing 𝕜] [MeasurableSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure 𝕜) (f : 𝕜 → E) (r : ℂ) :
fourierIntegral e μ (r • f) = r • fourierIntegral e μ f
source
theorem Fourier.norm_fourierIntegral_le_integral_norm {𝕜 : Type u_1} [CommRing 𝕜] [MeasurableSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure 𝕜) (f : 𝕜 → E) (w : 𝕜) :
‖fourierIntegral e μ f w‖ ≤ ∫ (x : 𝕜), ‖f x‖ ∂μ

The uniform norm of the Fourier transform of `f` is bounded by the `L¹` norm of `f`.

source
theorem Fourier.fourierIntegral_comp_add_right {𝕜 : Type u_1} [CommRing 𝕜] [MeasurableSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [MeasurableAdd 𝕜] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure 𝕜) [μ.IsAddRightInvariant] (f : 𝕜 → E) (v₀ : 𝕜) :
fourierIntegral e μ (f ∘ fun (v : 𝕜) => v + v₀) = fun (w : 𝕜) => e (v₀ * w) • fourierIntegral e μ f w

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

source
theorem Real.vector_fourierIntegral_eq_integral_exp_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_2} [AddCommGroup V] [Module ℝ V] [MeasurableSpace V] {W : Type u_3} [AddCommGroup W] [Module ℝ W] (L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ) (μ : MeasureTheory.Measure V) (f : V → E) (w : W) :
VectorFourier.fourierIntegral fourierChar μ L f w = ∫ (v : V), Complex.exp (↑(-2 * Real.pi * (L v) w) * Complex.I) • f v ∂μ
source
@[simp]
theorem Real.fourierIntegral_convergent_iff' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_2} {W : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure V} {f : V → E} (L : V →L[ℝ] W →L[ℝ] ℝ) (w : W) :
MeasureTheory.Integrable (fun (v : V) => fourierChar (-(L v) w) • f v) μ ↔ MeasureTheory.Integrable f μ

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

source
theorem Real.fourierIntegral_continuousLinearMap_apply' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type u_3} {V : Type u_4} {W : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup W] [NormedSpace ℝ W] {μ : MeasureTheory.Measure V} {L : V →L[ℝ] W →L[ℝ] ℝ} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : V → F →L[ℝ] E} {a : F} {w : W} (hf : MeasureTheory.Integrable f μ) :
(VectorFourier.fourierIntegral fourierChar μ L.toLinearMap₁₂ f w) a = VectorFourier.fourierIntegral fourierChar μ L.toLinearMap₁₂ (fun (x : V) => (f x) a) w
source
theorem Real.fourierIntegral_continuousMultilinearMap_apply' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {ι : Type u_2} {V : Type u_4} {W : Type u_5} [Fintype ι] [NormedAddCommGroup V] [NormedSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup W] [NormedSpace ℝ W] {μ : MeasureTheory.Measure V} {L : V →L[ℝ] W →L[ℝ] ℝ} {M : ι → Type u_6} [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace ℝ (M i)] {f : V → ContinuousMultilinearMap ℝ M E} {m : (i : ι) → M i} {w : W} (hf : MeasureTheory.Integrable f μ) :
(VectorFourier.fourierIntegral fourierChar μ L.toLinearMap₁₂ f w) m = VectorFourier.fourierIntegral fourierChar μ L.toLinearMap₁₂ (fun (x : V) => (f x) m) w
source
@[simp]
theorem Real.fourierIntegral_convergent_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure V} {f : V → E} (w : V) :
MeasureTheory.Integrable (fun (v : V) => fourierChar (-inner ℝ v w) • f v) μ ↔ MeasureTheory.Integrable f μ
source
instance Real.FourierTransform {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] :
_root_.FourierTransform (V → E) (V → E)
Equations

- Real.FourierTransform = { fourierTransform := fun (f : V → E) => VectorFourier.fourierIntegral Real.fourierChar MeasureTheory.volume (innerₗ V) f }

source
instance Real.FourierTransformInv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] :
_root_.FourierTransformInv (V → E) (V → E)
Equations

- Real.FourierTransformInv = { fourierTransformInv := fun (f : V → E) (w : V) => VectorFourier.fourierIntegral Real.fourierChar MeasureTheory.volume (-innerₗ V) f w }

source
@[deprecated FourierTransform.fourierTransform (since := "2025-11-12")]
def Real.fourierIntegral {E : Type u} {F : outParam (Type v)} [self : _root_.FourierTransform E F] :
E → F

Alias of `FourierTransform.fourierTransform`.

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

Equations

- @Real.fourierIntegral = @FourierTransform.fourierTransform

Instances For

source
@[deprecated FourierTransformInv.fourierTransformInv (since := "2025-11-12")]
def Real.fourierIntegralInv {E : Type u} {F : outParam (Type v)} [self : _root_.FourierTransformInv E F] :
E → F

Alias of `FourierTransformInv.fourierTransformInv`.

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

Equations

- @Real.fourierIntegralInv = @FourierTransformInv.fourierTransformInv

Instances For

source
theorem Real.fourierIntegral_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] (f : V → E) (w : V) :
FourierTransform.fourierTransform f w = ∫ (v : V), fourierChar (-inner ℝ v w) • f v
source
theorem Real.fourierIntegral_eq' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] (f : V → E) (w : V) :
FourierTransform.fourierTransform f w = ∫ (v : V), Complex.exp (↑(-2 * Real.pi * inner ℝ v w) * Complex.I) • f v
source
theorem Real.fourierIntegralInv_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] (f : V → E) (w : V) :
FourierTransformInv.fourierTransformInv f w = ∫ (v : V), fourierChar (inner ℝ v w) • f v
source
theorem Real.fourierIntegralInv_eq' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] (f : V → E) (w : V) :
FourierTransformInv.fourierTransformInv f w = ∫ (v : V), Complex.exp (↑(2 * Real.pi * inner ℝ v w) * Complex.I) • f v
source
theorem Real.fourierIntegral_comp_linearIsometry {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] {W : Type u_3} [NormedAddCommGroup W] [InnerProductSpace ℝ W] [MeasurableSpace W] [BorelSpace W] [FiniteDimensional ℝ W] [FiniteDimensional ℝ V] (A : W ≃ₗᵢ[ℝ] V) (f : V → E) (w : W) :
FourierTransform.fourierTransform (f ∘ ⇑A) w = FourierTransform.fourierTransform f (A w)
source
theorem Real.fourierIntegralInv_eq_fourierIntegral_neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] (f : V → E) (w : V) :
FourierTransformInv.fourierTransformInv f w = FourierTransform.fourierTransform f (-w)
source
theorem Real.fourierIntegralInv_eq_fourierIntegral_comp_neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] (f : V → E) :
FourierTransformInv.fourierTransformInv f = FourierTransform.fourierTransform fun (x : V) => f (-x)
source
theorem Real.fourierIntegralInv_comm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] (f : V → E) :
FourierTransform.fourierTransform (FourierTransformInv.fourierTransformInv f) = FourierTransformInv.fourierTransformInv (FourierTransform.fourierTransform f)
source
theorem Real.fourierIntegralInv_comp_linearIsometry {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] {W : Type u_3} [NormedAddCommGroup W] [InnerProductSpace ℝ W] [MeasurableSpace W] [BorelSpace W] [FiniteDimensional ℝ W] [FiniteDimensional ℝ V] (A : W ≃ₗᵢ[ℝ] V) (f : V → E) (w : W) :
FourierTransformInv.fourierTransformInv (f ∘ ⇑A) w = FourierTransformInv.fourierTransformInv f (A w)
source
theorem Real.fourierIntegral_real_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℝ → E) (w : ℝ) :
FourierTransform.fourierTransform f w = ∫ (v : ℝ), fourierChar (-(v * w)) • f v
source
theorem Real.fourierIntegral_real_eq_integral_exp_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℝ → E) (w : ℝ) :
FourierTransform.fourierTransform f w = ∫ (v : ℝ), Complex.exp (↑(-2 * Real.pi * v * w) * Complex.I) • f v
source
theorem Real.fourierIntegral_continuousLinearMap_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : V → F →L[ℝ] E} {a : F} {v : V} (hf : MeasureTheory.Integrable f MeasureTheory.volume) :
(FourierTransform.fourierTransform f v) a = FourierTransform.fourierTransform (fun (x : V) => (f x) a) v
source
theorem Real.fourierIntegral_continuousMultilinearMap_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] {ι : Type u_4} [Fintype ι] {M : ι → Type u_5} [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace ℝ (M i)] {f : V → ContinuousMultilinearMap ℝ M E} {m : (i : ι) → M i} {v : V} (hf : MeasureTheory.Integrable f MeasureTheory.volume) :
(FourierTransform.fourierTransform f v) m = FourierTransform.fourierTransform (fun (x : V) => (f x) m) v