mathlib documentation

analysis.fourier

Fourier analysis on the circle #

This file contains basic results on Fourier series.

Main definitions #

haar_circle, Haar measure on the circle, normalized to have total measure 1
instances measure_space, is_probability_measure for the circle with respect to this measure
for n : ℤ, fourier n is the monomial λ z, z ^ n, bundled as a continuous map from circle to ℂ
for n : ℤ and p : ℝ≥0∞, fourier_Lp p n is an abbreviation for the monomial fourier n considered as an element of the Lᵖ-space Lp ℂ p haar_circle, via the embedding continuous_map.to_Lp
fourier_series is the canonical isometric isomorphism from Lp ℂ 2 haar_circle to ℓ²(ℤ, ℂ) induced by taking Fourier series

Main statements #

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

The theorem span_fourier_Lp_closure_eq_top states that for 1 ≤ p < ∞ the span of the monomials fourier_Lp is dense in Lp ℂ p haar_circle, i.e. that its submodule.topological_closure is ⊤. This follows from the previous theorem using general theory on approximation of Lᵖ functions by continuous functions.

The theorem orthonormal_fourier states that the monomials fourier_Lp 2 n form an orthonormal set (in the L² space of the circle).

The last two results together provide that the functions fourier_Lp 2 n form a Hilbert basis for L²; this is named as fourier_series.

Parseval's identity, tsum_sq_fourier_series_repr, is a direct consequence of the construction of this Hilbert basis.

Choice of measure on the circle #

We make the circle into a measure space, using the Haar measure normalized to have total measure 1.

@[protected, instance]

noncomputable def circle.measurable_space :

measurable_space ↥circle

Equations

circle.measurable_space = borel ↥circle

@[protected, instance]

def circle.borel_space :

borel_space ↥circle

@[protected, instance]

def haar_circle.is_haar_measure :

haar_circle.is_haar_measure

noncomputable def haar_circle :

measure_theory.measure ↥circle

Haar measure on the circle, normalized to have total measure 1.

Equations

haar_circle = measure_theory.measure.haar_measure ⊤

Instances for haar_circle

@[protected, instance]

def haar_circle.measure_theory.is_probability_measure :

measure_theory.is_probability_measure haar_circle

@[protected, instance]

noncomputable def circle.measure_theory.measure_space :

measure_theory.measure_space ↥circle

Equations

circle.measure_theory.measure_space = {to_measurable_space := {measurable_set' := circle.measurable_space.measurable_set', measurable_set_empty := circle.measure_theory.measure_space._proof_1, measurable_set_compl := circle.measure_theory.measure_space._proof_2, measurable_set_Union := circle.measure_theory.measure_space._proof_3}, volume := haar_circle}

Monomials on the circle #

noncomputable def fourier (n : ℤ) :

C(↥circle , ℂ )

The family of monomials λ z, z ^ n, parametrized by n : ℤ and considered as bundled continuous maps from circle to ℂ.

Equations

fourier n = {to_fun := λ (z : ↥circle), ↑z ^ n, continuous_to_fun := _}

@[simp]

theorem fourier_apply (n : ℤ) (z : ↥circle) :

⇑(fourier n) z = ↑z ^ n

@[simp]

theorem fourier_zero {z : ↥circle} :

⇑(fourier 0) z = 1

@[simp]

theorem fourier_neg {n : ℤ} {z : ↥circle} :

⇑(fourier (-n)) z = ⇑(star_ring_end ℂ) (⇑(fourier n) z)

@[simp]

theorem fourier_add {m n : ℤ} {z : ↥circle} :

⇑(fourier (m + n)) z = ⇑(fourier m) z * ⇑(fourier n) z

noncomputable def fourier_subalgebra :

subalgebra ℂ C(↥circle , ℂ )

The subalgebra of C(circle, ℂ) generated by z ^ n for n ∈ ℤ; equivalently, polynomials in z and conj z.

Equations

fourier_subalgebra = algebra.adjoin ℂ (set.range fourier)

theorem fourier_subalgebra_coe :

fourier_subalgebra.to_submodule = submodule.span ℂ (set.range fourier)

The subalgebra of C(circle, ℂ) generated by z ^ n for n ∈ ℤ is in fact the linear span of these functions.

theorem fourier_subalgebra_separates_points :

fourier_subalgebra.separates_points

The subalgebra of C(circle, ℂ) generated by z ^ n for n ∈ ℤ separates points.

theorem fourier_subalgebra_conj_invariant :

continuous_map.conj_invariant_subalgebra (subalgebra.restrict_scalars ℝ fourier_subalgebra)

The subalgebra of C(circle, ℂ) generated by z ^ n for n ∈ ℤ is invariant under complex conjugation.

theorem fourier_subalgebra_closure_eq_top :

fourier_subalgebra.topological_closure = ⊤

The subalgebra of C(circle, ℂ) generated by z ^ n for n ∈ ℤ is dense.

theorem span_fourier_closure_eq_top :

(submodule.span ℂ (set.range fourier)).topological_closure = ⊤

The linear span of the monomials z ^ n is dense in C(circle, ℂ).

@[reducible]

noncomputable def fourier_Lp (p : ennreal) [fact (1 ≤ p)] (n : ℤ) :

↥(measure_theory.Lp ℂ p haar_circle)

The family of monomials λ z, z ^ n, parametrized by n : ℤ and considered as elements of the Lp space of functions on circle taking values in ℂ.

theorem coe_fn_fourier_Lp (p : ennreal) [fact (1 ≤ p)] (n : ℤ) :

⇑(fourier_Lp p n) =ᵐ[haar_circle ] ⇑(fourier n)

theorem span_fourier_Lp_closure_eq_top {p : ennreal} [fact (1 ≤ p)] (hp : p ≠ ⊤) :

(submodule.span ℂ (set.range (fourier_Lp p))).topological_closure = ⊤

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

theorem fourier_add_half_inv_index {n : ℤ} (hn : n ≠ 0) (z : ↥circle) :

⇑(fourier n) (⇑exp_map_circle ((↑n)⁻¹ * real.pi) * z) = -⇑(fourier n) z

For n ≠ 0, a rotation by n⁻¹ * real.pi negates the monomial z ^ n.

theorem orthonormal_fourier :

orthonormal ℂ (fourier_Lp 2)

The monomials z ^ n are an orthonormal set with respect to Haar measure on the circle.

noncomputable def fourier_series :

hilbert_basis ℤ ℂ ↥(measure_theory.Lp ℂ 2 haar_circle)

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

Equations

fourier_series = hilbert_basis.mk orthonormal_fourier fourier_series._proof_2

@[simp]

theorem coe_fourier_series :

⇑fourier_series = fourier_Lp 2

The elements of the Hilbert basis fourier_series for Lp ℂ 2 haar_circle are the functions fourier_Lp 2, the monomials λ z, z ^ n on the circle considered as elements of L2.

theorem fourier_series_repr (f : ↥(measure_theory.Lp ℂ 2 haar_circle)) (i : ℤ) :

⇑(⇑(fourier_series.repr) f) i = ∫ (t : ↥circle), ↑t ^ -i * ⇑f t ∂haar_circle

Under the isometric isomorphism fourier_series from Lp ℂ 2 haar_circle to ℓ²(ℤ, ℂ), the i-th coefficient is the integral over the circle of λ t, t ^ (-i) * f t.

theorem has_sum_fourier_series (f : ↥(measure_theory.Lp ℂ 2 haar_circle)) :

has_sum (λ (i : ℤ), ⇑(⇑(fourier_series.repr) f) i • fourier_Lp 2 i) f

The Fourier series of an L2 function f sums to f, in the L2 topology on the circle.

theorem tsum_sq_fourier_series_repr (f : ↥(measure_theory.Lp ℂ 2 haar_circle)) :

∑' (i : ℤ), ∥⇑(⇑(fourier_series.repr) f) i∥ ^ 2 = ∫ (t : ↥circle), ∥⇑f t∥ ^ 2 ∂haar_circle

Parseval's identity: the sum of the squared norms of the Fourier coefficients equals the L2 norm of the function.