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 #

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 functions f, the Fourier series of f converges to f in the 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 #

noncomputable def add_circle.to_circle {T : } :

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

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)] :

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

Equations
Instances for add_circle.haar_add_circle
noncomputable def fourier {T : } (n : ) :

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
@[simp]
theorem fourier_apply {T : } {n : } {x : add_circle T} :
@[simp]
theorem fourier_coe_apply {T : } {n : } {x : } :
@[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} :
@[simp]
theorem fourier_neg {T : } {n : } {x : add_circle T} :
@[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 : ) :
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 : } :

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

Equations

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

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

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

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

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 : ) :

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 : ) :
theorem span_fourier_Lp_closure_eq_top {T : } [hT : fact (0 < T)] {p : ennreal} [fact (1 p)] (hp : p ) :

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)] :

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
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 : ) :
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
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 : ) :
theorem fourier_coeff_lift_Ico_eq {T : } [hT : fact (0 < T)] {a : } (f : ) (n : ) :

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
@[simp]
theorem coe_fourier_basis {T : } [hT : fact (0 < T)] :

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 .

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.

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

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

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 : ) :
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.