mathlib documentation

analysis.fourier

Fourier analysis on the circle #

This file contains basic technical results for a development of Fourier series.

Main definitions #

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

By definition, a Hilbert basis for an inner product space is an orthonormal set whose span is dense. Thus, the last two results together establish that the functions fourier_Lp 2 n form a Hilbert basis for L².

TODO #

Once mathlib has general theory showing that a Hilbert basis of an inner product space induces a unitary equivalence with L², the results in this file will give Fourier series applications such as Parseval's formula.

Choice of measure on the circle #

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

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

Equations
@[instance]
Equations

Monomials on the circle #

def fourier (n : ) :

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

Equations
@[simp]
theorem fourier_to_fun (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} :
@[simp]
theorem fourier_add {m n : } {z : circle} :
(fourier (m + n)) z = ((fourier m) z) * (fourier n) z

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

Equations

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

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

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

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

The linear span of the monomials z ^ n is dense in C(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 .

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

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

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