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 measure1
- 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 fromcircle
toℂ
- for
n : ℤ
andp : ℝ≥0∞
,fourier_Lp p n
is an abbreviation for the monomialfourier n
considered as an element of the Lᵖ-spaceLp ℂ p haar_circle
, via the embeddingcontinuous_map.to_Lp
fourier_series
is the canonical isometric isomorphism fromLp ℂ 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.
Equations
Haar measure on the circle, normalized to have total measure 1.
Equations
Instances for haar_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 #
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, ℂ)
.
For each 1 ≤ p < ∞
, the linear span of the monomials z ^ n
is dense in
Lp ℂ p haar_circle
.
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
- fourier_series = hilbert_basis.mk orthonormal_fourier fourier_series._proof_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
.
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.