mathlib3 documentation

analysis.fourier.add_circle

Fourier analysis on the additive circle #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains basic results on Fourier series for functions on the additive circle add_circle T = ℝ / ℤ • T.

Main definitions #

haar_add_circle, Haar measure on add_circle T, normalized to have total measure 1. (Note that this is not the same normalisation as the standard measure defined in integral.periodic, so we do not declare it as a measure_space instance, to avoid confusion.)
for n : ℤ, fourier n is the monomial λ x, exp (2 π i n x / T), bundled as a continuous map from add_circle T to ℂ.
fourier_basis is the Hilbert basis of Lp ℂ 2 haar_add_circle given by the images of the monomials fourier n.
fourier_coeff f n, for f : add_circle T → E (with E a complete normed ℂ-vector space), is the n-th Fourier coefficient of f, defined as an integral over add_circle T. The lemma fourier_coeff_eq_interval_integral expresses this as an integral over [a, a + T] for any real a.
fourier_coeff_on, for f : ℝ → E and a < b reals, is the n-th Fourier coefficient of the unique periodic function of period b - a which agrees with f on (a, b]. The lemma fourier_coeff_on_eq_integral expresses this as an integral over [a, b].

Main statements #

The theorem span_fourier_closure_eq_top states that the span of the monomials fourier n is dense in C(add_circle T, ℂ), i.e. that its submodule.topological_closure is ⊤. This follows from the Stone-Weierstrass theorem after checking that the span is a subalgebra, is closed under conjugation, and separates points.

Using this and general theory on approximation of Lᵖ functions by continuous functions, we deduce (span_fourier_Lp_closure_eq_top) that for any 1 ≤ p < ∞, the span of the Fourier monomials is dense in the Lᵖ space of add_circle T. For p = 2 we show (orthonormal_fourier) that the monomials are also orthonormal, so they form a Hilbert basis for L², which is named as fourier_basis; in particular, for L² functions f, the Fourier series of f converges to f in the L² topology (has_sum_fourier_series_L2). Parseval's identity, tsum_sq_fourier_coeff, is a direct consequence.

For continuous maps f : add_circle T → ℂ, the theorem continuous_map.has_sum_fourier_series_of_summable states that if the sequence of Fourier coefficients of f is summable, then the Fourier series ∑ (i:ℤ), f.fourier_coeff i * fourier i converges to f in the uniform-convergence topology of C(add_circle T, ℂ).

Map from `add_circle` to `circle` #

theorem add_circle.scaled_exp_map_periodic {T : ℝ} :

function.periodic (λ (x : ℝ), ⇑exp_map_circle (2 * real.pi / T * x)) T

noncomputable def add_circle.to_circle {T : ℝ} :

add_circle T → ↥circle

The canonical map λ x, exp (2 π i x / T) from ℝ / ℤ • T to the unit circle in ℂ. If T = 0 we understand this as the constant function 1.

Equations

add_circle.to_circle = add_circle.scaled_exp_map_periodic.lift

theorem add_circle.to_circle_add {T : ℝ} (x y : add_circle T) :

(x + y).to_circle = x.to_circle * y.to_circle

theorem add_circle.continuous_to_circle {T : ℝ} :

continuous add_circle.to_circle

theorem add_circle.injective_to_circle {T : ℝ} (hT : T ≠ 0) :

function.injective add_circle.to_circle

Measure on `add_circle T` #

In this file we use the Haar measure on add_circle T normalised to have total measure 1 (which is not the same as the standard measure defined in topology.instances.add_circle).

noncomputable def add_circle.haar_add_circle {T : ℝ} [hT : fact (0 < T)] :

measure_theory.measure (add_circle T)

Haar measure on the additive circle, normalised to have total measure 1.

Equations

add_circle.haar_add_circle = measure_theory.measure.add_haar_measure ⊤

Instances for add_circle.haar_add_circle

@[protected, instance]

def add_circle.haar_add_circle.is_add_haar_measure {T : ℝ} [hT : fact (0 < T)] :

add_circle.haar_add_circle.is_add_haar_measure

@[protected, instance]

def add_circle.haar_add_circle.measure_theory.is_probability_measure {T : ℝ} [hT : fact (0 < T)] :

measure_theory.is_probability_measure add_circle.haar_add_circle

theorem add_circle.volume_eq_smul_haar_add_circle {T : ℝ} [hT : fact (0 < T)] :

measure_theory.measure_space.volume = ennreal.of_real T • add_circle.haar_add_circle

noncomputable def fourier {T : ℝ} (n : ℤ) :

C(add_circle T, ℂ )

The family of exponential monomials λ x, exp (2 π i n x / T), parametrized by n : ℤ and considered as bundled continuous maps from ℝ / ℤ • T to ℂ.

Equations

fourier n = {to_fun := λ (x : add_circle T), ↑((n • x).to_circle), continuous_to_fun := _}

@[simp]

theorem fourier_apply {T : ℝ} {n : ℤ} {x : add_circle T} :

⇑(fourier n) x = ↑((n • x).to_circle)

@[simp]

theorem fourier_coe_apply {T : ℝ} {n : ℤ} {x : ℝ} :

⇑(fourier n) ↑x = cexp (2 * ↑real.pi * complex.I * ↑n * ↑x / ↑T)

@[simp]

theorem fourier_zero {T : ℝ} {x : add_circle T} :

⇑(fourier 0) x = 1

@[simp]

theorem fourier_eval_zero {T : ℝ} (n : ℤ) :

⇑(fourier n) 0 = 1

@[simp]

theorem fourier_one {T : ℝ} {x : add_circle T} :

⇑(fourier 1) x = ↑(x.to_circle)

@[simp]

theorem fourier_neg {T : ℝ} {n : ℤ} {x : add_circle T} :

⇑(fourier (-n)) x = ⇑(star_ring_end ℂ) (⇑(fourier n) x)

@[simp]

theorem fourier_add {T : ℝ} {m n : ℤ} {x : add_circle T} :

⇑(fourier (m + n)) x = ⇑(fourier m) x * ⇑(fourier n) x

theorem fourier_norm {T : ℝ} [fact (0 < T)] (n : ℤ) :

‖fourier n‖ = 1

theorem fourier_add_half_inv_index {T : ℝ} {n : ℤ} (hn : n ≠ 0) (hT : 0 < T) (x : add_circle T) :

⇑(fourier n) (x + ↑(T / 2 / ↑n)) = -⇑(fourier n) x

For n ≠ 0, a translation by T / 2 / n negates the function fourier n.

noncomputable def fourier_subalgebra {T : ℝ} :

subalgebra ℂ C(add_circle T, ℂ )

The subalgebra of C(add_circle T, ℂ) generated by fourier n for n ∈ ℤ .

Equations

fourier_subalgebra = algebra.adjoin ℂ (set.range fourier)

theorem fourier_subalgebra_coe {T : ℝ} :

⇑subalgebra.to_submodule fourier_subalgebra = submodule.span ℂ (set.range fourier)

The subalgebra of C(add_circle T, ℂ) generated by fourier n for n ∈ ℤ is in fact the linear span of these functions.

theorem fourier_subalgebra_conj_invariant {T : ℝ} :

continuous_map.conj_invariant_subalgebra (subalgebra.restrict_scalars ℝ fourier_subalgebra)

The subalgebra of C(add_circle T, ℂ) generated by fourier n for n ∈ ℤ is invariant under complex conjugation.

theorem fourier_subalgebra_separates_points {T : ℝ} [hT : fact (0 < T)] :

fourier_subalgebra.separates_points

The subalgebra of C(add_circle T, ℂ) generated by fourier n for n ∈ ℤ separates points.

theorem fourier_subalgebra_closure_eq_top {T : ℝ} [hT : fact (0 < T)] :

fourier_subalgebra.topological_closure = ⊤

The subalgebra of C(add_circle T, ℂ) generated by fourier n for n ∈ ℤ is dense.

theorem span_fourier_closure_eq_top {T : ℝ} [hT : fact (0 < T)] :

(submodule.span ℂ (set.range fourier)).topological_closure = ⊤

The linear span of the monomials fourier n is dense in C(add_circle T, ℂ).

@[reducible]

noncomputable def fourier_Lp {T : ℝ} [hT : fact (0 < T)] (p : ennreal) [fact (1 ≤ p)] (n : ℤ) :

↥(measure_theory.Lp ℂ p add_circle.haar_add_circle)

The family of monomials fourier n, parametrized by n : ℤ and considered as elements of the Lp space of functions add_circle T → ℂ.

theorem coe_fn_fourier_Lp {T : ℝ} [hT : fact (0 < T)] (p : ennreal) [fact (1 ≤ p)] (n : ℤ) :

⇑(fourier_Lp p n) =ᵐ[add_circle.haar_add_circle ] ⇑(fourier n)

theorem span_fourier_Lp_closure_eq_top {T : ℝ} [hT : fact (0 < T)] {p : ennreal} [fact (1 ≤ p)] (hp : p ≠ ⊤) :

(submodule.span ℂ (set.range (fourier_Lp p))).topological_closure = ⊤

For each 1 ≤ p < ∞, the linear span of the monomials fourier n is dense in Lp ℂ p haar_circle.

theorem orthonormal_fourier {T : ℝ} [hT : fact (0 < T)] :

orthonormal ℂ (fourier_Lp 2)

The monomials fourier n are an orthonormal set with respect to normalised Haar measure.

noncomputable def fourier_coeff {T : ℝ} [hT : fact (0 < T)] {E : Type} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] (f : add_circle T → E) (n : ℤ) :

E

The n-th Fourier coefficient of a function add_circle T → E, for E a complete normed ℂ-vector space, defined as the integral over add_circle T of fourier (-n) t • f t.

Equations

fourier_coeff f n = ∫ (t : add_circle T), ⇑(fourier (-n)) t • f t ∂add_circle.haar_add_circle

theorem fourier_coeff_eq_interval_integral {T : ℝ} [hT : fact (0 < T)] {E : Type} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] (f : add_circle T → E) (n : ℤ) (a : ℝ) :

fourier_coeff f n = (1 / T) • ∫ (x : ℝ) in a..a + T, ⇑(fourier (-n)) ↑x • f ↑x

The Fourier coefficients of a function on add_circle T can be computed as an integral over [a, a + T], for any real a.

theorem fourier_coeff.const_smul {T : ℝ} [hT : fact (0 < T)] {E : Type} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] (f : add_circle T → E) (c : ℂ) (n : ℤ) :

fourier_coeff (c • f) n = c • fourier_coeff f n

theorem fourier_coeff.const_mul {T : ℝ} [hT : fact (0 < T)] (f : add_circle T → ℂ) (c : ℂ) (n : ℤ) :

fourier_coeff (λ (x : add_circle T), c * f x) n = c * fourier_coeff f n

noncomputable def fourier_coeff_on {E : Type} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] {a b : ℝ} (hab : a < b) (f : ℝ → E) (n : ℤ) :

E

For a function on ℝ, the Fourier coefficients of f on [a, b] are defined as the Fourier coefficients of the unique periodic function agreeing with f on Ioc a b.

Equations

fourier_coeff_on hab f n = fourier_coeff (add_circle.lift_Ioc (b - a) a f) n

theorem fourier_coeff_on_eq_integral {E : Type} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] {a b : ℝ} (f : ℝ → E) (n : ℤ) (hab : a < b) :

fourier_coeff_on hab f n = (1 / (b - a)) • ∫ (x : ℝ) in a..b, ⇑(fourier (-n)) ↑x • f x

theorem fourier_coeff_on.const_smul {E : Type} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] {a b : ℝ} (f : ℝ → E) (c : ℂ) (n : ℤ) (hab : a < b) :

fourier_coeff_on hab (c • f) n = c • fourier_coeff_on hab f n

theorem fourier_coeff_on.const_mul {a b : ℝ} (f : ℝ → ℂ) (c : ℂ) (n : ℤ) (hab : a < b) :

fourier_coeff_on hab (λ (x : ℝ), c * f x) n = c * fourier_coeff_on hab f n

theorem fourier_coeff_lift_Ioc_eq {T : ℝ} [hT : fact (0 < T)] {a : ℝ} (f : ℝ → ℂ) (n : ℤ) :

fourier_coeff (add_circle.lift_Ioc T a f) n = fourier_coeff_on _ f n

theorem fourier_coeff_lift_Ico_eq {T : ℝ} [hT : fact (0 < T)] {a : ℝ} (f : ℝ → ℂ) (n : ℤ) :

fourier_coeff (add_circle.lift_Ico T a f) n = fourier_coeff_on _ f n

noncomputable def fourier_basis {T : ℝ} [hT : fact (0 < T)] :

hilbert_basis ℤ ℂ ↥(measure_theory.Lp ℂ 2 add_circle.haar_add_circle)

We define fourier_basis to be a ℤ-indexed Hilbert basis for Lp ℂ 2 haar_add_circle, which by definition is an isometric isomorphism from Lp ℂ 2 haar_add_circle to ℓ²(ℤ, ℂ).

Equations

fourier_basis = hilbert_basis.mk orthonormal_fourier fourier_basis._proof_2

@[simp]

theorem coe_fourier_basis {T : ℝ} [hT : fact (0 < T)] :

⇑fourier_basis = fourier_Lp 2

The elements of the Hilbert basis fourier_basis are the functions fourier_Lp 2, i.e. the monomials fourier n on the circle considered as elements of L².

theorem fourier_basis_repr {T : ℝ} [hT : fact (0 < T)] (f : ↥(measure_theory.Lp ℂ 2 add_circle.haar_add_circle)) (i : ℤ) :

⇑(⇑(fourier_basis.repr) f) i = fourier_coeff ⇑f i

Under the isometric isomorphism fourier_basis from Lp ℂ 2 haar_circle to ℓ²(ℤ, ℂ), the i-th coefficient is fourier_coeff f i, i.e., the integral over add_circle T of λ t, fourier (-i) t * f t with respect to the Haar measure of total mass 1.

theorem has_sum_fourier_series_L2 {T : ℝ} [hT : fact (0 < T)] (f : ↥(measure_theory.Lp ℂ 2 add_circle.haar_add_circle)) :

has_sum (λ (i : ℤ), fourier_coeff ⇑f i • fourier_Lp 2 i) f

The Fourier series of an L2 function f sums to f, in the L² space of add_circle T.

theorem tsum_sq_fourier_coeff {T : ℝ} [hT : fact (0 < T)] (f : ↥(measure_theory.Lp ℂ 2 add_circle.haar_add_circle)) :

∑' (i : ℤ), ‖fourier_coeff ⇑f i‖ ^ 2 = ∫ (t : add_circle T), ‖⇑f t‖ ^ 2 ∂add_circle.haar_add_circle

Parseval's identity: for an L² function f on add_circle T, the sum of the squared norms of the Fourier coefficients equals the L² norm of f.

theorem fourier_coeff_to_Lp {T : ℝ} [hT : fact (0 < T)] (f : C(add_circle T, ℂ )) (n : ℤ) :

fourier_coeff ⇑(⇑(continuous_map.to_Lp 2 add_circle.haar_add_circle ℂ) f) n = fourier_coeff ⇑f n

theorem has_sum_fourier_series_of_summable {T : ℝ} [hT : fact (0 < T)] {f : C(add_circle T, ℂ )} (h : summable (fourier_coeff ⇑f)) :

has_sum (λ (i : ℤ), fourier_coeff ⇑f i • fourier i) f

If the sequence of Fourier coefficients of f is summable, then the Fourier series converges uniformly to f.

theorem has_pointwise_sum_fourier_series_of_summable {T : ℝ} [hT : fact (0 < T)] {f : C(add_circle T, ℂ )} (h : summable (fourier_coeff ⇑f)) (x : add_circle T) :

has_sum (λ (i : ℤ), fourier_coeff ⇑f i • ⇑(fourier i) x) (⇑f x)

If the sequence of Fourier coefficients of f is summable, then the Fourier series of f converges everywhere pointwise to f.

theorem has_deriv_at_fourier (T : ℝ) (n : ℤ) (x : ℝ) :

has_deriv_at (λ (y : ℝ), ⇑(fourier n) ↑y) (2 * ↑real.pi * complex.I * ↑n / ↑T * ⇑(fourier n) ↑x) x

theorem has_deriv_at_fourier_neg (T : ℝ) (n : ℤ) (x : ℝ) :

has_deriv_at (λ (y : ℝ), ⇑(fourier (-n)) ↑y) ((-2) * ↑real.pi * complex.I * ↑n / ↑T * ⇑(fourier (-n)) ↑x) x

theorem has_antideriv_at_fourier_neg {T : ℝ} (hT : fact (0 < T)) {n : ℤ} (hn : n ≠ 0) (x : ℝ) :

has_deriv_at (λ (y : ℝ), ↑T / ((-2) * ↑real.pi * complex.I * ↑n) * ⇑(fourier (-n)) ↑y) (⇑(fourier (-n)) ↑x) x

theorem fourier_coeff_on_of_has_deriv_at {a b : ℝ} (hab : a < b) {f f' : ℝ → ℂ} {n : ℤ} (hn : n ≠ 0) (hf : ∀ (x : ℝ), x ∈ set.uIcc a b → has_deriv_at f (f' x) x) (hf' : interval_integrable f' measure_theory.measure_space.volume a b) :

fourier_coeff_on hab f n = 1 / ((-2) * ↑real.pi * complex.I * ↑n) * (⇑(fourier (-n)) ↑a * (f b - f a) - (↑b - ↑a) * fourier_coeff_on hab f' n)

Express Fourier coefficients of f on an interval in terms of those of its derivative.