analysis.fourier

# Fourier analysis on the circle #

This file contains basic technical results for a development of 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

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

@[instance]
Equations
@[instance]

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

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

theorem span_fourier_Lp_closure_eq_top {p : ℝ≥0∞} [fact (1 p)] (hp : p ) :

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.

theorem orthonormal_fourier  :

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