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

• haarAddCircle, Haar measure on AddCircle T, normalized to have total measure 1. (Note that this is not the same normalisation as the standard measure defined in Integral.Periodic, so we do not declare it as a MeasureSpace instance, to avoid confusion.)
• for n : ℤ, fourier n is the monomial fun x => exp (2 π i n x / T), bundled as a continuous map from AddCircle T to ℂ.
• fourierBasis is the Hilbert basis of Lp ℂ 2 haarAddCircle given by the images of the monomials fourier n.
• fourierCoeff f n, for f : AddCircle T → E (with E a complete normed ℂ-vector space), is the n-th Fourier coefficient of f, defined as an integral over AddCircle T. The lemma fourierCoeff_eq_interval_integral expresses this as an integral over [a, a + T] for any real a.
• fourierCoeffOn, for f : ℝ → E and a < b reals, is the n-th Fourier coefficient of the unique periodic function of period b - a which agrees with f on (a, b]. The lemma fourierCoeffOn_eq_integral expresses this as an integral over [a, b].

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 L² functions f, the Fourier series of f converges to f in the L² 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

def AddCircle.toCircle {T : ℝ} : AddCircle T → ↥circle

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

• AddCircle.toCircle = Function.Periodic.lift (_ : Function.Periodic (fun (x : ℝ) => expMapCircle (2 * Real.pi / T * x)) T)

theorem AddCircle.toCircle_add {T : ℝ} (x : AddCircle T) (y : AddCircle T) : AddCircle.toCircle (x + y) = AddCircle.toCircle x * AddCircle.toCircle y

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

def AddCircle.haarAddCircle {T : ℝ} [hT : Fact (0 < T)] : MeasureTheory.Measure (AddCircle T)

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

Equations

• AddCircle.haarAddCircle = MeasureTheory.Measure.addHaarMeasure ⊤

instance AddCircle.instIsAddHaarMeasureAddCircleRealInstLinearOrderedAddCommGroupRealToTopologicalSpaceToUniformSpacePseudoMetricSpaceInstOrderTopologyRealToTopologicalSpaceToUniformSpacePseudoMetricSpaceInstPreorderRealAddGroupToAddGroupToAddCommGroupToOrderedAddCommGroupZmultiplesNormal_of_commInstAddCommGroupRealTopologicalSpaceMeasurableSpaceMeasurableSpaceHaarAddCircle {T : ℝ} [hT : Fact (0 < T)] : MeasureTheory.Measure.IsAddHaarMeasure AddCircle.haarAddCircle

Equations

• (_ : MeasureTheory.Measure.IsAddHaarMeasure AddCircle.haarAddCircle) = (_ : MeasureTheory.Measure.IsAddHaarMeasure (MeasureTheory.Measure.addHaarMeasure ⊤))

instance AddCircle.instIsProbabilityMeasureAddCircleRealInstLinearOrderedAddCommGroupRealToTopologicalSpaceToUniformSpacePseudoMetricSpaceInstOrderTopologyRealToTopologicalSpaceToUniformSpacePseudoMetricSpaceInstPreorderRealMeasurableSpaceToAddGroupToAddCommGroupToOrderedAddCommGroupMeasurableSpaceZmultiplesHaarAddCircle {T : ℝ} [hT : Fact (0 < T)] : MeasureTheory.IsProbabilityMeasure AddCircle.haarAddCircle

Equations

• (_ : MeasureTheory.IsProbabilityMeasure AddCircle.haarAddCircle) = (_ : MeasureTheory.IsProbabilityMeasure AddCircle.haarAddCircle)

theorem AddCircle.volume_eq_smul_haarAddCircle {T : ℝ} [hT : Fact (0 < T)] : MeasureTheory.volume = ENNReal.ofReal T • AddCircle.haarAddCircle

def fourier {T : ℝ} (n : ℤ) : C(AddCircle T, ℂ)

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

• fourier n = ContinuousMap.mk fun (x : AddCircle T) => ↑(AddCircle.toCircle (n • x))

@[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} : ↑(AddCircle.toCircle 0) = 1

theorem fourier_eval_zero {T : ℝ} (n : ℤ) : (fourier n) 0 = 1

theorem fourier_one {T : ℝ} {x : AddCircle T} : (fourier 1) x = ↑(AddCircle.toCircle x)

theorem fourier_neg {T : ℝ} {n : ℤ} {x : AddCircle T} : (fourier (-n)) x = (starRingEnd ℂ) ((fourier n) x)

@[simp]

theorem fourier_neg' {T : ℝ} {n : ℤ} {x : AddCircle T} : ↑(AddCircle.toCircle (-(n • x))) = (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} : ↑(AddCircle.toCircle ((m + n) • x)) = (fourier m) x * (fourier n) x

theorem fourier_norm {T : ℝ} [Fact (0 < T)] (n : ℤ) : ‖fourier n‖ = 1

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.

def fourierSubalgebra {T : ℝ} : StarSubalgebra ℂ C(AddCircle T, ℂ)

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

Equations

• fourierSubalgebra = { toSubalgebra := Algebra.adjoin ℂ (Set.range fourier), star_mem' := (_ : Algebra.adjoin ℂ (Set.range fourier) ≤ star (Algebra.adjoin ℂ (Set.range fourier))) }

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)] : StarSubalgebra.topologicalClosure fourierSubalgebra = ⊤

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.topologicalClosure (Submodule.span ℂ (Set.range fourier)) = ⊤

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)

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

Equations

• fourierLp p n = (ContinuousMap.toLp p AddCircle.haarAddCircle ℂ) (fourier n)

theorem coeFn_fourierLp {T : ℝ} [hT : Fact (0 < T)] (p : ENNReal) [Fact (1 ≤ p)] (n : ℤ) : ↑↑(fourierLp p n) =ᶠ[MeasureTheory.Measure.ae AddCircle.haarAddCircle] ⇑(fourier n)

theorem span_fourierLp_closure_eq_top {T : ℝ} [hT : Fact (0 < T)] {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) : Submodule.topologicalClosure (Submodule.span ℂ (Set.range (fourierLp p))) = ⊤

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)] : Orthonormal ℂ (fourierLp 2)

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 T → E) (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

• fourierCoeff f n = ∫ (t : AddCircle T), (fourier (-n)) t • f t ∂AddCircle.haarAddCircle

theorem fourierCoeff_eq_intervalIntegral {T : ℝ} [hT : Fact (0 < T)] {E : Type} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : AddCircle T → E) (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 T → E) (c : ℂ) (n : ℤ) : fourierCoeff (c • f) n = c • fourierCoeff f 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

• fourierCoeffOn hab f n = fourierCoeff (AddCircle.liftIoc (b - a) a f) n

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 : ℤ) : fourierCoeff (AddCircle.liftIoc T a f) n = fourierCoeffOn (_ : a < a + T) f n

theorem fourierCoeff_liftIco_eq {T : ℝ} [hT : Fact (0 < T)] {a : ℝ} (f : ℝ → ℂ) (n : ℤ) : fourierCoeff (AddCircle.liftIco T a f) n = fourierCoeffOn (_ : a < a + T) f n

def fourierBasis {T : ℝ} [hT : Fact (0 < T)] : HilbertBasis ℤ ℂ ↥(MeasureTheory.Lp ℂ 2)

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

• fourierBasis = HilbertBasis.mk (_ : Orthonormal ℂ (fourierLp 2)) (_ : ⊤ ≤ Submodule.topologicalClosure (Submodule.span ℂ (Set.range (fourierLp 2))))

@[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 L².

theorem fourierBasis_repr {T : ℝ} [hT : Fact (0 < T)] (f : ↥(MeasureTheory.Lp ℂ 2)) (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)) : HasSum (fun (i : ℤ) => fourierCoeff (↑↑f) i • fourierLp 2 i) f

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

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

Parseval's identity: for an L² function f on AddCircle T, the sum of the squared norms of the Fourier coefficients equals the L² 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 : ∀ x ∈ Set.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.