Documentation

Mathlib.Analysis.Fourier.FourierTransform

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:

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 β„‚ 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
Instances For
    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 : β„‚) :
    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) :
    β€–VectorFourier.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.

    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) :
    VectorFourier.fourierIntegral e ΞΌ L (f ∘ fun (v : V) => v + vβ‚€) = fun (w : W) => e ((L vβ‚€) w) β€’ VectorFourier.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 β„‚ E] [TopologicalSpace π•œ] [TopologicalRing π•œ] [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.

    @[deprecated VectorFourier.fourierIntegral_convergent_iff]
    theorem VectorFourier.fourier_integral_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 π•œ] [TopologicalRing π•œ] [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 ΞΌ

    Alias of VectorFourier.fourierIntegral_convergent_iff.


    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 β„‚ E] [TopologicalSpace π•œ] [TopologicalRing π•œ] [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} {g : V β†’ E} (hf : MeasureTheory.Integrable f ΞΌ) (hg : MeasureTheory.Integrable 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 β„‚ E] [TopologicalSpace π•œ] [TopologicalRing π•œ] [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 ΞΌ) :

    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 β„‚ E] [NormedAddCommGroup F] [NormedSpace β„‚ F] [NormedAddCommGroup G] [NormedSpace β„‚ G] [TopologicalSpace π•œ] [TopologicalRing π•œ] [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 (VectorFourier.fourierIntegral e ΞΌ L f ΞΎ)) (g ΞΎ) βˆ‚Ξ½ = ∫ (x : V), (M (f x)) (VectorFourier.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 β„‚ F] [TopologicalSpace π•œ] [TopologicalRing π•œ] [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), VectorFourier.fourierIntegral e ΞΌ L f ΞΎ β€’ g ΞΎ βˆ‚Ξ½ = ∫ (x : V), f x β€’ VectorFourier.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 : 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 ΞΌ) :
    (VectorFourier.fourierIntegral e ΞΌ L.toLinearMapβ‚‚ f w) a = VectorFourier.fourierIntegral e ΞΌ L.toLinearMapβ‚‚ (fun (x : V) => (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 : 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 ΞΌ) :
    (VectorFourier.fourierIntegral e ΞΌ L.toLinearMapβ‚‚ f w) m = VectorFourier.fourierIntegral e ΞΌ L.toLinearMapβ‚‚ (fun (x : V) => (f x) m) w

    Fourier theory for functions on π•œ #

    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
    Instances For
      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 : π•œ) :
      Fourier.fourierIntegral e ΞΌ f w = ∫ (v : π•œ), e (-(v * w)) β€’ f v βˆ‚ΞΌ
      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 : β„‚) :
      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 : π•œ) :
      β€–Fourier.fourierIntegral e ΞΌ f wβ€– ≀ ∫ (x : π•œ), β€–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 β„‚ E] [MeasurableAdd π•œ] (e : AddChar π•œ Circle) (ΞΌ : MeasureTheory.Measure π•œ) [ΞΌ.IsAddRightInvariant] (f : π•œ β†’ E) (vβ‚€ : π•œ) :
      Fourier.fourierIntegral e ΞΌ (f ∘ fun (v : π•œ) => v + vβ‚€) = fun (w : π•œ) => e (vβ‚€ * w) β€’ Fourier.fourierIntegral e ΞΌ f w

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

      The standard additive character of ℝ, given by fun x ↦ exp (2 * Ο€ * x * I).

      Equations
      Instances For

        The standard additive character of ℝ, given by fun x ↦ exp (2 * Ο€ * x * I).

        Equations
        Instances For
          theorem Real.fourierChar_apply (x : ℝ) :
          ↑(Real.fourierChar x) = Complex.exp (↑(2 * Real.pi * x) * Complex.I)
          @[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) => Real.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.

          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 Real.fourierChar ΞΌ L.toLinearMapβ‚‚ f w) m = VectorFourier.fourierIntegral Real.fourierChar ΞΌ L.toLinearMapβ‚‚ (fun (x : V) => (f x) m) w
          @[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) => Real.fourierChar (-inner v w) β€’ f v) ΞΌ ↔ MeasureTheory.Integrable f ΞΌ

          The Fourier transform of a function on an inner product space, with respect to the standard additive character Ο‰ ↦ exp (2 i Ο€ Ο‰).

          Equations
          Instances For

            The inverse Fourier transform of a function on an inner product space, defined as the Fourier transform but with opposite sign in the exponential.

            Equations
            Instances For

              The Fourier transform of a function on an inner product space, with respect to the standard additive character Ο‰ ↦ exp (2 i Ο€ Ο‰).

              Equations
              Instances For

                The inverse Fourier transform of a function on an inner product space, defined as the Fourier transform but with opposite sign in the exponential.

                Equations
                Instances For
                  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) :
                  Real.fourierIntegral f w = ∫ (v : V), Real.fourierChar (-inner v w) β€’ f v
                  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) :
                  Real.fourierIntegralInv f w = ∫ (v : V), Real.fourierChar (inner v w) β€’ f v
                  theorem Real.fourierIntegral_real_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] (f : ℝ β†’ E) (w : ℝ) :
                  Real.fourierIntegral f w = ∫ (v : ℝ), Real.fourierChar (-(v * w)) β€’ f v
                  @[deprecated Real.fourierIntegral_real_eq]
                  theorem Real.fourierIntegral_def {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] (f : ℝ β†’ E) (w : ℝ) :
                  Real.fourierIntegral f w = ∫ (v : ℝ), Real.fourierChar (-(v * w)) β€’ f v

                  Alias of Real.fourierIntegral_real_eq.

                  @[deprecated Real.fourierIntegral_real_eq_integral_exp_smul]

                  Alias of Real.fourierIntegral_real_eq_integral_exp_smul.

                  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) :
                  (Real.fourierIntegral f v) m = Real.fourierIntegral (fun (x : V) => (f x) m) v