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 IntervalIntegral.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_intervalIntegral 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, hasSum_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).

noncomputable 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 ⊤

@[implicit_reducible]

noncomputable instance AddCircle.instIsAddHaarMeasureRealHaarAddCircle {T : ℝ} [hT : Fact (0 < T)] : haarAddCircle.IsAddHaarMeasure

Equations

• ⋯ = ⋯

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

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

theorem AddCircle.integral_haarAddCircle {T : ℝ} [hT : Fact (0 < T)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : AddCircle T → E} : ∫ (t : AddCircle T), f t ∂haarAddCircle = T⁻¹ • ∫ (t : AddCircle T), f t

theorem MeasureTheory.memLp_haarAddCircle_iff {T : ℝ} [hT : Fact (0 < T)] {f : AddCircle T → ℂ} {p : ENNReal} : MemLp f p AddCircle.haarAddCircle ↔ MemLp f p volume

theorem MeasureTheory.MemLp.haarAddCircle {T : ℝ} [hT : Fact (0 < T)] {f : AddCircle T → ℂ} {p : ENNReal} : MemLp f p volume → MemLp f p AddCircle.haarAddCircle

Alias of the reverse direction of MeasureTheory.memLp_haarAddCircle_iff.

theorem MeasureTheory.MemLp.of_haarAddCircle {T : ℝ} [hT : Fact (0 < T)] {f : AddCircle T → ℂ} {p : ENNReal} : MemLp f p AddCircle.haarAddCircle → MemLp f p volume

Alias of the forward direction of MeasureTheory.memLp_haarAddCircle_iff.

noncomputable 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 = { toFun := fun (x : AddCircle T) => ↑(n • x).toCircle, continuous_toFun := ⋯ }

@[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

theorem fourier_zero' {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 = ↑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 : ℤ) : ‖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.

noncomputable 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' := ⋯ }

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]

noncomputable 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

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

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

noncomputable def fourierCoeff {T : ℝ} [hT : Fact (0 < T)] {E : Type u_1} [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 u_1} [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 MeasureTheory.Integrable.fourier_smul {T : ℝ} [hT : Fact (0 < T)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : AddCircle T → E} (hf : Integrable f AddCircle.haarAddCircle) (n : ℤ) : Integrable (fun (t : AddCircle T) => (fourier n) t • f t) AddCircle.haarAddCircle

theorem fourierCoeff.add {T : ℝ} [hT : Fact (0 < T)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : AddCircle T → E} (hf : MeasureTheory.Integrable f AddCircle.haarAddCircle) (hg : MeasureTheory.Integrable g AddCircle.haarAddCircle) : fourierCoeff (f + g) = fourierCoeff f + fourierCoeff g

theorem fourierCoeff.sum {T : ℝ} [hT : Fact (0 < T)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {ι : Type u_2} (s : Finset ι) (f : ι → AddCircle T → E) (hf : ∀ i ∈ s, MeasureTheory.Integrable (f i) AddCircle.haarAddCircle) : fourierCoeff (∑ i ∈ s, f i) = ∑ i ∈ s, fourierCoeff (f i)

theorem fourierCoeff.const_smul {T : ℝ} [hT : Fact (0 < T)] {E : Type u_1} [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

theorem fourierCoeff_congr_ae {T : ℝ} [hT : Fact (0 < T)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : AddCircle T → E} (h : f =ᵐ[AddCircle.haarAddCircle] g) : fourierCoeff f = fourierCoeff g

noncomputable def fourierCoeffOn {E : Type u_1} [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 u_1} [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 u_1} [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 fourierCoeffOn_congr_ae {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {a b : ℝ} (hab : a < b) {f g : ℝ → E} (h : f =ᵐ[MeasureTheory.volume.restrict (Set.Ioc a b)] g) : fourierCoeffOn hab f = fourierCoeffOn hab g

theorem fourierCoeff_liftIoc_eq {T : ℝ} [hT : Fact (0 < T)] {a : ℝ} (f : ℝ → ℂ) (n : ℤ) : fourierCoeff (AddCircle.liftIoc T a f) n = fourierCoeffOn ⋯ f n

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

noncomputable 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

• fourierBasis = HilbertBasis.mk ⋯ ⋯

@[simp]

theorem coe_fourierBasis {T : ℝ} [hT : Fact (0 < T)] : ⇑fourierBasis = 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 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 L² space of AddCircle T.

theorem hasSum_sq_fourierCoeff {T : ℝ} [hT : Fact (0 < T)] (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) : HasSum (fun (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 tsum_sq_fourierCoeff {T : ℝ} [hT : Fact (0 < T)] (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) : ∑' (i : ℤ), ‖fourierCoeff (↑↑f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂AddCircle.haarAddCircle

theorem hasSum_sq_fourierCoeffOn {a b : ℝ} {f : ℝ → ℂ} (hab : a < b) (hL2 : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (Set.Ioc a b))) : HasSum (fun (i : ℤ) => ‖fourierCoeffOn hab f i‖ ^ 2) ((b - a)⁻¹ • ∫ (x : ℝ) in a..b, ‖f x‖ ^ 2)

Parseval's identity: for a function f which is square integrable on (a,b], the sum of the squared norms of the Fourier coefficients equals the L² norm of f.

theorem tsum_sq_fourierCoeffOn {a b : ℝ} {f : ℝ → ℂ} (hab : a < b) (hL2 : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (Set.Ioc a b))) : ∑' (i : ℤ), ‖fourierCoeffOn hab f i‖ ^ 2 = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, ‖f x‖ ^ 2

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 fourierCoeff_fourier {T : ℝ} [hT : Fact (0 < T)] (n : ℤ) : fourierCoeff ⇑(fourier n) = Pi.single n 1

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' : ∀ x ∈ Set.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' : ∀ x ∈ Set.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 : ∀ 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.