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 introduce the notation 𝐞 in the locale 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

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 Complex E] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure V) (L : LinearMap (RingHom.id 𝕜) V (LinearMap (RingHom.id 𝕜) 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

• Eq (VectorFourier.fourierIntegral e μ L f w) (MeasureTheory.integral μ fun (v : V) => HSMul.hSMul (DFunLike.coe e (Neg.neg (DFunLike.coe (DFunLike.coe L v) w))) (f v))

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 Complex E] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure V) (L : LinearMap (RingHom.id 𝕜) V (LinearMap (RingHom.id 𝕜) W 𝕜)) (f : V → E) (r : Complex) : Eq (fourierIntegral e μ L (HSMul.hSMul r f)) (HSMul.hSMul r (fourierIntegral e μ L f))

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 Complex E] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure V) (L : LinearMap (RingHom.id 𝕜) V (LinearMap (RingHom.id 𝕜) W 𝕜)) (f : V → E) (w : W) : LE.le (Norm.norm (fourierIntegral e μ L f w)) (MeasureTheory.integral μ fun (v : V) => Norm.norm (f v))

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

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 Complex E] [MeasurableAdd V] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure V) [μ.IsAddRightInvariant] (L : LinearMap (RingHom.id 𝕜) V (LinearMap (RingHom.id 𝕜) W 𝕜)) (f : V → E) (v₀ : V) : Eq (fourierIntegral e μ L (Function.comp f fun (v : V) => HAdd.hAdd v v₀)) fun (w : W) => HSMul.hSMul (DFunLike.coe e (DFunLike.coe (DFunLike.coe 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.

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 Complex E] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] [TopologicalSpace V] [BorelSpace V] [TopologicalSpace W] {e : AddChar 𝕜 Circle} {μ : MeasureTheory.Measure V} {L : LinearMap (RingHom.id 𝕜) V (LinearMap (RingHom.id 𝕜) W 𝕜)} (he : Continuous (DFunLike.coe e)) (hL : Continuous fun (p : Prod V W) => DFunLike.coe (DFunLike.coe L p.fst) p.snd) {f : V → E} (w : W) : Iff (MeasureTheory.Integrable (fun (v : V) => HSMul.hSMul (DFunLike.coe e (Neg.neg (DFunLike.coe (DFunLike.coe L v) w))) (f v)) μ) (MeasureTheory.Integrable f μ)

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

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 Complex E] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] [TopologicalSpace V] [BorelSpace V] [TopologicalSpace W] {e : AddChar 𝕜 Circle} {μ : MeasureTheory.Measure V} {L : LinearMap (RingHom.id 𝕜) V (LinearMap (RingHom.id 𝕜) W 𝕜)} (he : Continuous (DFunLike.coe e)) (hL : Continuous fun (p : Prod V W) => DFunLike.coe (DFunLike.coe L p.fst) p.snd) {f g : V → E} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) : Eq (fourierIntegral e μ L (HAdd.hAdd f g)) (HAdd.hAdd (fourierIntegral e μ L f) (fourierIntegral e μ L g))

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 Complex E] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] [TopologicalSpace V] [BorelSpace V] [TopologicalSpace W] {e : AddChar 𝕜 Circle} {μ : MeasureTheory.Measure V} {L : LinearMap (RingHom.id 𝕜) V (LinearMap (RingHom.id 𝕜) W 𝕜)} [FirstCountableTopology W] (he : Continuous (DFunLike.coe e)) (hL : Continuous fun (p : Prod V W) => DFunLike.coe (DFunLike.coe L p.fst) p.snd) {f : V → E} (hf : MeasureTheory.Integrable f μ) : Continuous (fourierIntegral e μ L f)

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

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 Complex E] [NormedAddCommGroup F] [NormedSpace Complex F] [NormedAddCommGroup G] [NormedSpace Complex G] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] [TopologicalSpace V] [BorelSpace V] [TopologicalSpace W] [MeasurableSpace W] [BorelSpace W] {e : AddChar 𝕜 Circle} {μ : MeasureTheory.Measure V} {L : LinearMap (RingHom.id 𝕜) V (LinearMap (RingHom.id 𝕜) W 𝕜)} {ν : MeasureTheory.Measure W} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] [SecondCountableTopology V] [CompleteSpace E] [CompleteSpace F] {f : V → E} {g : W → F} (M : ContinuousLinearMap (RingHom.id Complex) E (ContinuousLinearMap (RingHom.id Complex) F G)) (he : Continuous (DFunLike.coe e)) (hL : Continuous fun (p : Prod V W) => DFunLike.coe (DFunLike.coe L p.fst) p.snd) (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g ν) : Eq (MeasureTheory.integral ν fun (ξ : W) => DFunLike.coe (DFunLike.coe M (fourierIntegral e μ L f ξ)) (g ξ)) (MeasureTheory.integral μ fun (x : V) => DFunLike.coe (DFunLike.coe 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.

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 Complex F] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] [TopologicalSpace V] [BorelSpace V] [TopologicalSpace W] [MeasurableSpace W] [BorelSpace W] {e : AddChar 𝕜 Circle} {μ : MeasureTheory.Measure V} {L : LinearMap (RingHom.id 𝕜) V (LinearMap (RingHom.id 𝕜) W 𝕜)} {ν : MeasureTheory.Measure W} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] [SecondCountableTopology V] [CompleteSpace F] {f : V → Complex} {g : W → F} (he : Continuous (DFunLike.coe e)) (hL : Continuous fun (p : Prod V W) => DFunLike.coe (DFunLike.coe L p.fst) p.snd) (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g ν) : Eq (MeasureTheory.integral ν fun (ξ : W) => HSMul.hSMul (fourierIntegral e μ L f ξ) (g ξ)) (MeasureTheory.integral μ fun (x : V) => HSMul.hSMul (f x) (fourierIntegral e ν L.flip g x))

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

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 : ContinuousLinearMap (RingHom.id 𝕜) V (ContinuousLinearMap (RingHom.id 𝕜) W 𝕜)} [NormedAddCommGroup F] [NormedSpace Real F] [NormedAddCommGroup E] [NormedSpace Complex E] {f : V → ContinuousLinearMap (RingHom.id Real) F E} {a : F} {w : W} (he : Continuous (DFunLike.coe e)) (hf : MeasureTheory.Integrable f μ) : Eq (DFunLike.coe (fourierIntegral e μ L.toLinearMap₂ f w) a) (fourierIntegral e μ L.toLinearMap₂ (fun (x : V) => DFunLike.coe (f x) a) w)

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 : ContinuousLinearMap (RingHom.id 𝕜) V (ContinuousLinearMap (RingHom.id 𝕜) W 𝕜)} [NormedAddCommGroup E] [NormedSpace Complex E] {M : ι → Type u_7} [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace Real (M i)] {f : V → ContinuousMultilinearMap Real M E} {m : (i : ι) → M i} {w : W} (he : Continuous (DFunLike.coe e)) (hf : MeasureTheory.Integrable f μ) : Eq (DFunLike.coe (fourierIntegral e μ L.toLinearMap₂ f w) m) (fourierIntegral e μ L.toLinearMap₂ (fun (x : V) => DFunLike.coe (f x) m) w)

Fourier theory for functions on 𝕜

def Fourier.fourierIntegral {𝕜 : Type u_1} [CommRing 𝕜] [MeasurableSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace Complex 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

• Eq (Fourier.fourierIntegral e μ f w) (VectorFourier.fourierIntegral e μ (LinearMap.mul 𝕜 𝕜) f w)

theorem Fourier.fourierIntegral_def {𝕜 : Type u_1} [CommRing 𝕜] [MeasurableSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace Complex E] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure 𝕜) (f : 𝕜 → E) (w : 𝕜) : Eq (fourierIntegral e μ f w) (MeasureTheory.integral μ fun (v : 𝕜) => HSMul.hSMul (DFunLike.coe e (Neg.neg (HMul.hMul v w))) (f v))

theorem Fourier.fourierIntegral_const_smul {𝕜 : Type u_1} [CommRing 𝕜] [MeasurableSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace Complex E] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure 𝕜) (f : 𝕜 → E) (r : Complex) : Eq (fourierIntegral e μ (HSMul.hSMul r f)) (HSMul.hSMul r (fourierIntegral e μ f))

theorem Fourier.norm_fourierIntegral_le_integral_norm {𝕜 : Type u_1} [CommRing 𝕜] [MeasurableSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace Complex E] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure 𝕜) (f : 𝕜 → E) (w : 𝕜) : LE.le (Norm.norm (fourierIntegral e μ f w)) (MeasureTheory.integral μ fun (x : 𝕜) => Norm.norm (f x))

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

theorem Fourier.fourierIntegral_comp_add_right {𝕜 : Type u_1} [CommRing 𝕜] [MeasurableSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace Complex E] [MeasurableAdd 𝕜] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure 𝕜) [μ.IsAddRightInvariant] (f : 𝕜 → E) (v₀ : 𝕜) : Eq (fourierIntegral e μ (Function.comp f fun (v : 𝕜) => HAdd.hAdd v v₀)) fun (w : 𝕜) => HSMul.hSMul (DFunLike.coe e (HMul.hMul v₀ w)) (fourierIntegral e μ f w)

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

def Real.fourierChar : AddChar Real Circle

The standard additive character of ℝ, given by fun x ↦ exp (2 * π * x * I). Denoted as 𝐞 within the Real.FourierTransform namespace.

Equations

• One or more equations did not get rendered due to their size.

def FourierTransform.«term𝐞» : Lean.ParserDescr

The standard additive character of ℝ, given by fun x ↦ exp (2 * π * x * I). Denoted as 𝐞 within the Real.FourierTransform namespace.

Equations

• Eq FourierTransform.«term𝐞» (Lean.ParserDescr.node `FourierTransform.«term𝐞» 1024 (Lean.ParserDescr.symbol "𝐞"))

theorem Real.fourierChar_apply (x : Real) : Eq (DFunLike.coe fourierChar x).val (Complex.exp (HMul.hMul (Complex.ofReal (HMul.hMul (HMul.hMul 2 Real.pi) x)) Complex.I))

theorem Real.continuous_fourierChar : Continuous (DFunLike.coe fourierChar)

theorem Real.vector_fourierIntegral_eq_integral_exp_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] {V : Type u_2} [AddCommGroup V] [Module Real V] [MeasurableSpace V] {W : Type u_3} [AddCommGroup W] [Module Real W] (L : LinearMap (RingHom.id Real) V (LinearMap (RingHom.id Real) W Real)) (μ : MeasureTheory.Measure V) (f : V → E) (w : W) : Eq (VectorFourier.fourierIntegral fourierChar μ L f w) (MeasureTheory.integral μ fun (v : V) => HSMul.hSMul (Complex.exp (HMul.hMul (Complex.ofReal (HMul.hMul (HMul.hMul (-2) Real.pi) (DFunLike.coe (DFunLike.coe L v) w))) Complex.I)) (f v))

theorem Real.fourierIntegral_convergent_iff' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] {V : Type u_2} {W : Type u_3} [NormedAddCommGroup V] [NormedSpace Real V] [NormedAddCommGroup W] [NormedSpace Real W] [MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure V} {f : V → E} (L : ContinuousLinearMap (RingHom.id Real) V (ContinuousLinearMap (RingHom.id Real) W Real)) (w : W) : Iff (MeasureTheory.Integrable (fun (v : V) => HSMul.hSMul (DFunLike.coe fourierChar (Neg.neg (DFunLike.coe (DFunLike.coe 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.

theorem Real.fourierIntegral_continuousLinearMap_apply' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] {F : Type u_3} {V : Type u_4} {W : Type u_5} [NormedAddCommGroup V] [NormedSpace Real V] [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup W] [NormedSpace Real W] {μ : MeasureTheory.Measure V} {L : ContinuousLinearMap (RingHom.id Real) V (ContinuousLinearMap (RingHom.id Real) W Real)} [NormedAddCommGroup F] [NormedSpace Real F] {f : V → ContinuousLinearMap (RingHom.id Real) F E} {a : F} {w : W} (hf : MeasureTheory.Integrable f μ) : Eq (DFunLike.coe (VectorFourier.fourierIntegral fourierChar μ L.toLinearMap₂ f w) a) (VectorFourier.fourierIntegral fourierChar μ L.toLinearMap₂ (fun (x : V) => DFunLike.coe (f x) a) w)

theorem Real.fourierIntegral_continuousMultilinearMap_apply' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] {ι : Type u_2} {V : Type u_4} {W : Type u_5} [Fintype ι] [NormedAddCommGroup V] [NormedSpace Real V] [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup W] [NormedSpace Real W] {μ : MeasureTheory.Measure V} {L : ContinuousLinearMap (RingHom.id Real) V (ContinuousLinearMap (RingHom.id Real) W Real)} {M : ι → Type u_6} [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace Real (M i)] {f : V → ContinuousMultilinearMap Real M E} {m : (i : ι) → M i} {w : W} (hf : MeasureTheory.Integrable f μ) : Eq (DFunLike.coe (VectorFourier.fourierIntegral fourierChar μ L.toLinearMap₂ f w) m) (VectorFourier.fourierIntegral fourierChar μ L.toLinearMap₂ (fun (x : V) => DFunLike.coe (f x) m) w)

theorem Real.fourierIntegral_convergent_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure V} {f : V → E} (w : V) : Iff (MeasureTheory.Integrable (fun (v : V) => HSMul.hSMul (DFunLike.coe fourierChar (Neg.neg (Inner.inner v w))) (f v)) μ) (MeasureTheory.Integrable f μ)

def Real.fourierIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional Real V] (f : V → E) (w : V) : E

The Fourier transform of a function on an inner product space, with respect to the standard additive character ω ↦ exp (2 i π ω). Denoted as 𝓕 within the Real.FourierTransform namespace.

Equations

• Eq (Real.fourierIntegral f w) (VectorFourier.fourierIntegral Real.fourierChar MeasureTheory.MeasureSpace.volume (innerₗ V) f w)

def Real.fourierIntegralInv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional Real V] (f : V → E) (w : V) : E

The inverse Fourier transform of a function on an inner product space, defined as the Fourier transform but with opposite sign in the exponential. Denoted as 𝓕⁻¹ within the Real.FourierTransform namespace.

Equations

• Eq (Real.fourierIntegralInv f w) (VectorFourier.fourierIntegral Real.fourierChar MeasureTheory.MeasureSpace.volume (Neg.neg (innerₗ V)) f w)

def FourierTransform.term𝓕 : Lean.ParserDescr

The Fourier transform of a function on an inner product space, with respect to the standard additive character ω ↦ exp (2 i π ω). Denoted as 𝓕 within the Real.FourierTransform namespace.

Equations

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

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

The inverse Fourier transform of a function on an inner product space, defined as the Fourier transform but with opposite sign in the exponential. Denoted as 𝓕⁻¹ within the Real.FourierTransform namespace.

Equations

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

theorem Real.fourierIntegral_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional Real V] (f : V → E) (w : V) : Eq (fourierIntegral f w) (MeasureTheory.integral MeasureTheory.MeasureSpace.volume fun (v : V) => HSMul.hSMul (DFunLike.coe fourierChar (Neg.neg (Inner.inner v w))) (f v))

theorem Real.fourierIntegral_eq' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional Real V] (f : V → E) (w : V) : Eq (fourierIntegral f w) (MeasureTheory.integral MeasureTheory.MeasureSpace.volume fun (v : V) => HSMul.hSMul (Complex.exp (HMul.hMul (Complex.ofReal (HMul.hMul (HMul.hMul (-2) Real.pi) (Inner.inner v w))) Complex.I)) (f v))

theorem Real.fourierIntegralInv_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional Real V] (f : V → E) (w : V) : Eq (fourierIntegralInv f w) (MeasureTheory.integral MeasureTheory.MeasureSpace.volume fun (v : V) => HSMul.hSMul (DFunLike.coe fourierChar (Inner.inner v w)) (f v))

theorem Real.fourierIntegralInv_eq' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional Real V] (f : V → E) (w : V) : Eq (fourierIntegralInv f w) (MeasureTheory.integral MeasureTheory.MeasureSpace.volume fun (v : V) => HSMul.hSMul (Complex.exp (HMul.hMul (Complex.ofReal (HMul.hMul (HMul.hMul 2 Real.pi) (Inner.inner v w))) Complex.I)) (f v))

theorem Real.fourierIntegral_comp_linearIsometry {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MeasurableSpace V] [BorelSpace V] {W : Type u_3} [NormedAddCommGroup W] [InnerProductSpace Real W] [MeasurableSpace W] [BorelSpace W] [FiniteDimensional Real W] [FiniteDimensional Real V] (A : LinearIsometryEquiv (RingHom.id Real) W V) (f : V → E) (w : W) : Eq (fourierIntegral (Function.comp f (DFunLike.coe A)) w) (fourierIntegral f (DFunLike.coe A w))

theorem Real.fourierIntegralInv_eq_fourierIntegral_neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional Real V] (f : V → E) (w : V) : Eq (fourierIntegralInv f w) (fourierIntegral f (Neg.neg w))

theorem Real.fourierIntegralInv_eq_fourierIntegral_comp_neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional Real V] (f : V → E) : Eq (fourierIntegralInv f) (fourierIntegral fun (x : V) => f (Neg.neg x))

theorem Real.fourierIntegralInv_comm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional Real V] (f : V → E) : Eq (fourierIntegral (fourierIntegralInv f)) (fourierIntegralInv (fourierIntegral f))

theorem Real.fourierIntegralInv_comp_linearIsometry {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MeasurableSpace V] [BorelSpace V] {W : Type u_3} [NormedAddCommGroup W] [InnerProductSpace Real W] [MeasurableSpace W] [BorelSpace W] [FiniteDimensional Real W] [FiniteDimensional Real V] (A : LinearIsometryEquiv (RingHom.id Real) W V) (f : V → E) (w : W) : Eq (fourierIntegralInv (Function.comp f (DFunLike.coe A)) w) (fourierIntegralInv f (DFunLike.coe A w))

theorem Real.fourierIntegral_real_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] (f : Real → E) (w : Real) : Eq (fourierIntegral f w) (MeasureTheory.integral MeasureTheory.MeasureSpace.volume fun (v : Real) => HSMul.hSMul (DFunLike.coe fourierChar (Neg.neg (HMul.hMul v w))) (f v))

theorem Real.fourierIntegral_real_eq_integral_exp_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] (f : Real → E) (w : Real) : Eq (fourierIntegral f w) (MeasureTheory.integral MeasureTheory.MeasureSpace.volume fun (v : Real) => HSMul.hSMul (Complex.exp (HMul.hMul (Complex.ofReal (HMul.hMul (HMul.hMul (HMul.hMul (-2) Real.pi) v) w)) Complex.I)) (f v))

theorem Real.fourierIntegral_continuousLinearMap_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional Real V] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace Real F] {f : V → ContinuousLinearMap (RingHom.id Real) F E} {a : F} {v : V} (hf : MeasureTheory.Integrable f MeasureTheory.MeasureSpace.volume) : Eq (DFunLike.coe (fourierIntegral f v) a) (fourierIntegral (fun (x : V) => DFunLike.coe (f x) a) v)

theorem Real.fourierIntegral_continuousMultilinearMap_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional Real V] {ι : Type u_4} [Fintype ι] {M : ι → Type u_5} [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace Real (M i)] {f : V → ContinuousMultilinearMap Real M E} {m : (i : ι) → M i} {v : V} (hf : MeasureTheory.Integrable f MeasureTheory.MeasureSpace.volume) : Eq (DFunLike.coe (fourierIntegral f v) m) (fourierIntegral (fun (x : V) => DFunLike.coe (f x) m) v)