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 βˆ‚ΞΌ,

where e [x] is notational sugar for (e (Multiplicative.ofAdd x) : β„‚) (available in locale fourier_transform). 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). The Fourier integral in this case is defined as Real.fourierIntegral.

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 : Multiplicative π•œ β†’* { x // x ∈ 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.

Instances For
    theorem VectorFourier.fourierIntegral_smul_const {π•œ : 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 : Multiplicative π•œ β†’* { x // x ∈ 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 : Multiplicative π•œ β†’* { x // x ∈ 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 : Multiplicative π•œ β†’* { x // x ∈ circle }) (ΞΌ : MeasureTheory.Measure V) [MeasureTheory.Measure.IsAddRightInvariant ΞΌ] (L : V β†’β‚—[π•œ] W β†’β‚—[π•œ] π•œ) (f : V β†’ E) (vβ‚€ : V) :
    VectorFourier.fourierIntegral e ΞΌ L (f ∘ fun v => v + vβ‚€) = fun w => ↑(↑e (↑Multiplicative.ofAdd (↑(↑L vβ‚€) w))) β€’ VectorFourier.fourierIntegral e ΞΌ L f w

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

    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 : Multiplicative π•œ β†’* { x // x ∈ circle }} {ΞΌ : MeasureTheory.Measure V} {L : V β†’β‚—[π•œ] W β†’β‚—[π•œ] π•œ} (he : Continuous ↑e) (hL : Continuous fun p => ↑(↑L p.fst) p.snd) {f : V β†’ E} (w : W) :
    MeasureTheory.Integrable f ↔ MeasureTheory.Integrable fun v => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) β€’ f v

    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 : Multiplicative π•œ β†’* { x // x ∈ circle }} {ΞΌ : MeasureTheory.Measure V} {L : V β†’β‚—[π•œ] W β†’β‚—[π•œ] π•œ} (he : Continuous ↑e) (hL : Continuous fun p => ↑(↑L p.fst) p.snd) {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 : Multiplicative π•œ β†’* { x // x ∈ circle }} {ΞΌ : MeasureTheory.Measure V} {L : V β†’β‚—[π•œ] W β†’β‚—[π•œ] π•œ} [TopologicalSpace.FirstCountableTopology W] (he : Continuous ↑e) (hL : Continuous fun p => ↑(↑L p.fst) p.snd) {f : V β†’ E} (hf : MeasureTheory.Integrable f) :

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

    Fourier theory for functions on π•œ #

    def Fourier.fourierIntegral {π•œ : Type u_1} [CommRing π•œ] [MeasurableSpace π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace β„‚ E] (e : Multiplicative π•œ β†’* { x // x ∈ circle }) (ΞΌ : MeasureTheory.Measure π•œ) (f : π•œ β†’ E) (w : π•œ) :
    E

    The Fourier transform integral for f : π•œ β†’ E, with respect to the measure ΞΌ and additive character e.

    Instances For
      theorem Fourier.fourierIntegral_def {π•œ : Type u_1} [CommRing π•œ] [MeasurableSpace π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace β„‚ E] (e : Multiplicative π•œ β†’* { x // x ∈ circle }) (ΞΌ : MeasureTheory.Measure π•œ) (f : π•œ β†’ E) (w : π•œ) :
      Fourier.fourierIntegral e ΞΌ f w = ∫ (v : π•œ), ↑(↑e (↑Multiplicative.ofAdd (-(v * w)))) β€’ f v βˆ‚ΞΌ
      theorem Fourier.fourierIntegral_smul_const {π•œ : Type u_1} [CommRing π•œ] [MeasurableSpace π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace β„‚ E] (e : Multiplicative π•œ β†’* { x // x ∈ 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 : Multiplicative π•œ β†’* { x // x ∈ 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 : Multiplicative π•œ β†’* { x // x ∈ circle }) (ΞΌ : MeasureTheory.Measure π•œ) [MeasureTheory.Measure.IsAddRightInvariant ΞΌ] (f : π•œ β†’ E) (vβ‚€ : π•œ) :
      Fourier.fourierIntegral e ΞΌ (f ∘ fun v => v + vβ‚€) = fun w => ↑(↑e (↑Multiplicative.ofAdd (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).

      Instances For
        theorem Real.fourierChar_apply (x : ℝ) :
        ↑(↑Real.fourierChar (↑Multiplicative.ofAdd x)) = Complex.exp (↑(2 * Real.pi * x) * Complex.I)
        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 Real.fourierChar ΞΌ L f w = ∫ (v : V), Complex.exp (↑(-2 * Real.pi * ↑(↑L v) w) * Complex.I) β€’ f v βˆ‚ΞΌ
        def Real.fourierIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] (f : ℝ β†’ E) (w : ℝ) :
        E

        The Fourier integral for f : ℝ β†’ E, with respect to the standard additive character and measure on ℝ.

        Instances For
          theorem Real.fourierIntegral_def {E : Type u_1} [NormedAddCommGroup E] [NormedSpace β„‚ E] (f : ℝ β†’ E) (w : ℝ) :
          Real.fourierIntegral f w = ∫ (v : ℝ), ↑(↑Real.fourierChar (↑Multiplicative.ofAdd (-(v * w)))) β€’ f v