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  :
Equations
@[protected, instance]
@[protected, instance]
noncomputable def haar_circle  :

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

Equations
Instances for haar_circle
@[protected, instance]
@[protected, instance]
noncomputable def circle.measure_theory.measure_space  :
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} :
(fourier (-n)) z = ((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  :

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 : ennreal) [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 coe_fn_fourier_Lp (p : ennreal) [fact (1 p)] (n : ) :
theorem span_fourier_Lp_closure_eq_top {p : ennreal} [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.

noncomputable def fourier_series  :

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]
theorem coe_fourier_series  :

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.

theorem has_sum_fourier_series (f : ) :
has_sum (λ (i : ), ((fourier_series.repr) f) i i) f

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.