mathlib documentation

analysis.fourier

Fourier analysis on the circle #

This file contains basic results on 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).

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]
Equations
@[protected, instance]

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

Equations
@[protected, instance]
Equations

Monomials on the circle #

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

noncomputable def fourier_Lp (p : ℝ≥0∞) [fact (1 p)] (n : ) :

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.

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

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.

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.

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

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