Documentation

Mathlib.Analysis.Fourier.AddCircle

Fourier analysis on the additive circle #

This file contains basic results on Fourier series for functions on the additive circle AddCircle T = ℝ / ℤ • T.

Main definitions #

Main statements #

The theorem span_fourier_closure_eq_top states that the span of the monomials fourier n is dense in C(AddCircle T, ℂ), i.e. that its Submodule.topologicalClosure is . This follows from the Stone-Weierstrass theorem after checking that the span is a subalgebra, is closed under conjugation, and separates points.

Using this and general theory on approximation of Lᵖ functions by continuous functions, we deduce (span_fourierLp_closure_eq_top) that for any 1 ≤ p < ∞, the span of the Fourier monomials is dense in the Lᵖ space of AddCircle T. For p = 2 we show (orthonormal_fourier) that the monomials are also orthonormal, so they form a Hilbert basis for L², which is named as fourierBasis; in particular, for functions f, the Fourier series of f converges to f in the topology (hasSum_fourier_series_L2). Parseval's identity, tsum_sq_fourierCoeff, is a direct consequence.

For continuous maps f : AddCircle T → ℂ, the theorem hasSum_fourier_series_of_summable states that if the sequence of Fourier coefficients of f is summable, then the Fourier series ∑ (i : ℤ), fourierCoeff f i * fourier i converges to f in the uniform-convergence topology of C(AddCircle T, ℂ).

Measure on AddCircle T #

In this file we use the Haar measure on AddCircle T normalised to have total measure 1 (which is not the same as the standard measure defined in Topology.Instances.AddCircle).

Haar measure on the additive circle, normalised to have total measure 1.

Equations
Instances For
    instance AddCircle.instIsAddHaarMeasureRealHaarAddCircle {T : } [hT : Fact (0 < T)] :
    AddCircle.haarAddCircle.IsAddHaarMeasure
    Equations
    • =
    Equations
    • =
    theorem AddCircle.volume_eq_smul_haarAddCircle {T : } [hT : Fact (0 < T)] :
    MeasureTheory.volume = ENNReal.ofReal T AddCircle.haarAddCircle
    def fourier {T : } (n : ) :

    The family of exponential monomials fun x => exp (2 π i n x / T), parametrized by n : ℤ and considered as bundled continuous maps from ℝ / ℤ • T to .

    Equations
    Instances For
      @[simp]
      theorem fourier_apply {T : } {n : } {x : AddCircle T} :
      (fourier n) x = (n x).toCircle
      theorem fourier_coe_apply {T : } {n : } {x : } :
      (fourier n) x = Complex.exp (2 * Real.pi * Complex.I * n * x / T)
      @[simp]
      theorem fourier_coe_apply' {T : } {n : } {x : } :
      (AddCircle.toCircle (n x)) = Complex.exp (2 * Real.pi * Complex.I * n * x / T)
      theorem fourier_zero {T : } {x : AddCircle T} :
      (fourier 0) x = 1
      @[simp]
      theorem fourier_zero' {T : } {x : AddCircle T} :
      theorem fourier_eval_zero {T : } (n : ) :
      (fourier n) 0 = 1
      theorem fourier_one {T : } {x : AddCircle T} :
      (fourier 1) x = x.toCircle
      theorem fourier_neg {T : } {n : } {x : AddCircle T} :
      (fourier (-n)) x = (starRingEnd ) ((fourier n) x)
      @[simp]
      theorem fourier_neg' {T : } {n : } {x : AddCircle T} :
      (-(n x)).toCircle = (starRingEnd ) ((fourier n) x)
      theorem fourier_add {T : } {m : } {n : } {x : AddCircle T} :
      (fourier (m + n)) x = (fourier m) x * (fourier n) x
      @[simp]
      theorem fourier_add' {T : } {m : } {n : } {x : AddCircle T} :
      ((m + n) x).toCircle = (fourier m) x * (fourier n) x
      theorem fourier_norm {T : } [Fact (0 < T)] (n : ) :
      theorem fourier_add_half_inv_index {T : } {n : } (hn : n 0) (hT : 0 < T) (x : AddCircle T) :
      (fourier n) (x + (T / 2 / n)) = -(fourier n) x

      For n ≠ 0, a translation by T / 2 / n negates the function fourier n.

      The star subalgebra of C(AddCircle T, ℂ) generated by fourier n for n ∈ ℤ .

      Equations
      Instances For
        theorem fourierSubalgebra_coe {T : } :
        Subalgebra.toSubmodule fourierSubalgebra.toSubalgebra = Submodule.span (Set.range fourier)

        The star subalgebra of C(AddCircle T, ℂ) generated by fourier n for n ∈ ℤ is in fact the linear span of these functions.

        theorem fourierSubalgebra_separatesPoints {T : } [hT : Fact (0 < T)] :
        fourierSubalgebra.SeparatesPoints

        The subalgebra of C(AddCircle T, ℂ) generated by fourier n for n ∈ ℤ separates points.

        theorem fourierSubalgebra_closure_eq_top {T : } [hT : Fact (0 < T)] :
        fourierSubalgebra.topologicalClosure =

        The subalgebra of C(AddCircle T, ℂ) generated by fourier n for n ∈ ℤ is dense.

        theorem span_fourier_closure_eq_top {T : } [hT : Fact (0 < T)] :
        (Submodule.span (Set.range fourier)).topologicalClosure =

        The linear span of the monomials fourier n is dense in C(AddCircle T, ℂ).

        @[reducible, inline]
        abbrev fourierLp {T : } [hT : Fact (0 < T)] (p : ENNReal) [Fact (1 p)] (n : ) :
        (MeasureTheory.Lp p AddCircle.haarAddCircle)

        The family of monomials fourier n, parametrized by n : ℤ and considered as elements of the Lp space of functions AddCircle T → ℂ.

        Equations
        Instances For
          theorem coeFn_fourierLp {T : } [hT : Fact (0 < T)] (p : ENNReal) [Fact (1 p)] (n : ) :
          (fourierLp p n) =ᵐ[AddCircle.haarAddCircle] (fourier n)
          theorem span_fourierLp_closure_eq_top {T : } [hT : Fact (0 < T)] {p : ENNReal} [Fact (1 p)] (hp : p ) :
          (Submodule.span (Set.range (fourierLp p))).topologicalClosure =

          For each 1 ≤ p < ∞, the linear span of the monomials fourier n is dense in Lp ℂ p haarAddCircle.

          theorem orthonormal_fourier {T : } [hT : Fact (0 < T)] :

          The monomials fourier n are an orthonormal set with respect to normalised Haar measure.

          def fourierCoeff {T : } [hT : Fact (0 < T)] {E : Type} [NormedAddCommGroup E] [NormedSpace E] (f : AddCircle TE) (n : ) :
          E

          The n-th Fourier coefficient of a function AddCircle T → E, for E a complete normed -vector space, defined as the integral over AddCircle T of fourier (-n) t • f t.

          Equations
          Instances For
            theorem fourierCoeff_eq_intervalIntegral {T : } [hT : Fact (0 < T)] {E : Type} [NormedAddCommGroup E] [NormedSpace E] (f : AddCircle TE) (n : ) (a : ) :
            fourierCoeff f n = (1 / T) ∫ (x : ) in a..a + T, (fourier (-n)) x f x

            The Fourier coefficients of a function on AddCircle T can be computed as an integral over [a, a + T], for any real a.

            theorem fourierCoeff.const_smul {T : } [hT : Fact (0 < T)] {E : Type} [NormedAddCommGroup E] [NormedSpace E] (f : AddCircle TE) (c : ) (n : ) :
            theorem fourierCoeff.const_mul {T : } [hT : Fact (0 < T)] (f : AddCircle T) (c : ) (n : ) :
            fourierCoeff (fun (x : AddCircle T) => c * f x) n = c * fourierCoeff f n
            def fourierCoeffOn {E : Type} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } (hab : a < b) (f : E) (n : ) :
            E

            For a function on , the Fourier coefficients of f on [a, b] are defined as the Fourier coefficients of the unique periodic function agreeing with f on Ioc a b.

            Equations
            Instances For
              theorem fourierCoeffOn_eq_integral {E : Type} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } (f : E) (n : ) (hab : a < b) :
              fourierCoeffOn hab f n = (1 / (b - a)) ∫ (x : ) in a..b, (fourier (-n)) x f x
              theorem fourierCoeffOn.const_smul {E : Type} [NormedAddCommGroup E] [NormedSpace E] {a : } {b : } (f : E) (c : ) (n : ) (hab : a < b) :
              fourierCoeffOn hab (c f) n = c fourierCoeffOn hab f n
              theorem fourierCoeffOn.const_mul {a : } {b : } (f : ) (c : ) (n : ) (hab : a < b) :
              fourierCoeffOn hab (fun (x : ) => c * f x) n = c * fourierCoeffOn hab f n
              theorem fourierCoeff_liftIoc_eq {T : } [hT : Fact (0 < T)] {a : } (f : ) (n : ) :
              theorem fourierCoeff_liftIco_eq {T : } [hT : Fact (0 < T)] {a : } (f : ) (n : ) :
              def fourierBasis {T : } [hT : Fact (0 < T)] :
              HilbertBasis (MeasureTheory.Lp 2 AddCircle.haarAddCircle)

              We define fourierBasis to be a -indexed Hilbert basis for Lp ℂ 2 haarAddCircle, which by definition is an isometric isomorphism from Lp ℂ 2 haarAddCircle to ℓ²(ℤ, ℂ).

              Equations
              Instances For
                @[simp]
                theorem coe_fourierBasis {T : } [hT : Fact (0 < T)] :
                (fun (i : ) => fourierBasis.repr.symm (lp.single 2 i 1)) = fourierLp 2

                The elements of the Hilbert basis fourierBasis are the functions fourierLp 2, i.e. the monomials fourier n on the circle considered as elements of .

                theorem fourierBasis_repr {T : } [hT : Fact (0 < T)] (f : (MeasureTheory.Lp 2 AddCircle.haarAddCircle)) (i : ) :
                (fourierBasis.repr f) i = fourierCoeff (f) i

                Under the isometric isomorphism fourierBasis from Lp ℂ 2 haarAddCircle to ℓ²(ℤ, ℂ), the i-th coefficient is fourierCoeff f i, i.e., the integral over AddCircle T of fun t => fourier (-i) t * f t with respect to the Haar measure of total mass 1.

                theorem hasSum_fourier_series_L2 {T : } [hT : Fact (0 < T)] (f : (MeasureTheory.Lp 2 AddCircle.haarAddCircle)) :
                HasSum (fun (i : ) => fourierCoeff (f) i fourierLp 2 i) f

                The Fourier series of an L2 function f sums to f, in the space of AddCircle T.

                theorem tsum_sq_fourierCoeff {T : } [hT : Fact (0 < T)] (f : (MeasureTheory.Lp 2 AddCircle.haarAddCircle)) :
                ∑' (i : ), fourierCoeff (f) i ^ 2 = ∫ (t : AddCircle T), f t ^ 2AddCircle.haarAddCircle

                Parseval's identity: for an function f on AddCircle T, the sum of the squared norms of the Fourier coefficients equals the norm of f.

                theorem fourierCoeff_toLp {T : } [hT : Fact (0 < T)] (f : C(AddCircle T, )) (n : ) :
                fourierCoeff (((ContinuousMap.toLp 2 AddCircle.haarAddCircle ) f)) n = fourierCoeff (f) n
                theorem hasSum_fourier_series_of_summable {T : } [hT : Fact (0 < T)] {f : C(AddCircle T, )} (h : Summable (fourierCoeff f)) :
                HasSum (fun (i : ) => fourierCoeff (f) i fourier i) f

                If the sequence of Fourier coefficients of f is summable, then the Fourier series converges uniformly to f.

                theorem has_pointwise_sum_fourier_series_of_summable {T : } [hT : Fact (0 < T)] {f : C(AddCircle T, )} (h : Summable (fourierCoeff f)) (x : AddCircle T) :
                HasSum (fun (i : ) => fourierCoeff (f) i (fourier i) x) (f x)

                If the sequence of Fourier coefficients of f is summable, then the Fourier series of f converges everywhere pointwise to f.

                theorem hasDerivAt_fourier (T : ) (n : ) (x : ) :
                HasDerivAt (fun (y : ) => (fourier n) y) (2 * Real.pi * Complex.I * n / T * (fourier n) x) x
                theorem hasDerivAt_fourier_neg (T : ) (n : ) (x : ) :
                HasDerivAt (fun (y : ) => (fourier (-n)) y) (-2 * Real.pi * Complex.I * n / T * (fourier (-n)) x) x
                theorem has_antideriv_at_fourier_neg {T : } (hT : Fact (0 < T)) {n : } (hn : n 0) (x : ) :
                HasDerivAt (fun (y : ) => T / (-2 * Real.pi * Complex.I * n) * (fourier (-n)) y) ((fourier (-n)) x) x
                theorem fourierCoeffOn_of_hasDeriv_right {a : } {b : } (hab : a < b) {f : } {f' : } {n : } (hn : n 0) (hf : ContinuousOn f (Set.uIcc a b)) (hff' : xSet.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) (hf' : IntervalIntegrable f' MeasureTheory.volume a b) :
                fourierCoeffOn hab f n = 1 / (-2 * Real.pi * Complex.I * n) * ((fourier (-n)) a * (f b - f a) - (b - a) * fourierCoeffOn hab f' n)

                Express Fourier coefficients of f on an interval in terms of those of its derivative.

                theorem fourierCoeffOn_of_hasDerivAt_Ioo {a : } {b : } (hab : a < b) {f : } {f' : } {n : } (hn : n 0) (hf : ContinuousOn f (Set.uIcc a b)) (hff' : xSet.Ioo (min a b) (max a b), HasDerivAt f (f' x) x) (hf' : IntervalIntegrable f' MeasureTheory.volume a b) :
                fourierCoeffOn hab f n = 1 / (-2 * Real.pi * Complex.I * n) * ((fourier (-n)) a * (f b - f a) - (b - a) * fourierCoeffOn hab f' n)

                Express Fourier coefficients of f on an interval in terms of those of its derivative.

                theorem fourierCoeffOn_of_hasDerivAt {a : } {b : } (hab : a < b) {f : } {f' : } {n : } (hn : n 0) (hf : xSet.uIcc a b, HasDerivAt f (f' x) x) (hf' : IntervalIntegrable f' MeasureTheory.volume a b) :
                fourierCoeffOn hab f n = 1 / (-2 * Real.pi * Complex.I * n) * ((fourier (-n)) a * (f b - f a) - (b - a) * fourierCoeffOn hab f' n)

                Express Fourier coefficients of f on an interval in terms of those of its derivative.