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, ℂ).

Map from AddCircle to Circle #

theorem AddCircle.scaled_exp_map_periodic {T : } :
Function.Periodic (fun (x : ) => expMapCircle (2 * Real.pi / T * x)) T

The canonical map fun x => exp (2 π i x / T) from ℝ / ℤ • T to the unit circle in . If T = 0 we understand this as the constant function 1.

Equations
Instances For
    theorem AddCircle.continuous_toCircle {T : } :
    Continuous AddCircle.toCircle
    theorem AddCircle.injective_toCircle {T : } (hT : T 0) :
    Function.Injective AddCircle.toCircle

    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
      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 = (AddCircle.toCircle (n x))
        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} :
        theorem fourier_neg {T : } {n : } {x : AddCircle T} :
        (fourier (-n)) x = (starRingEnd ) ((fourier n) x)
        @[simp]
        theorem fourier_neg' {T : } {n : } {x : AddCircle T} :
        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} :
        (AddCircle.toCircle ((m + n) x)) = (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)] :
          Subalgebra.SeparatesPoints fourierSubalgebra.toSubalgebra

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

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

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

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

          @[inline, reducible]
          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) =ᶠ[MeasureTheory.Measure.ae AddCircle.haarAddCircle] (fourier n)

            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 : ) => (LinearIsometryEquiv.symm fourierBasis.repr) (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_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.