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

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
theorem add_circle.to_circle_add {T : } (x y : add_circle T) :
(x + y).to_circle =
theorem add_circle.injective_to_circle {T : } (hT : T 0) :

### 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
@[protected, instance]
@[protected, instance]
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} :
(fourier (-n)) x = ((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 : ) :
= 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 : } :

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.

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

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

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

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} [ E] (f : 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} [ E] (f : E) (n : ) (a : ) :
= (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} [ E] (f : E) (c : ) (n : ) :
fourier_coeff (c f) n = c
theorem fourier_coeff.const_mul {T : } [hT : fact (0 < T)] (f : ) (c : ) (n : ) :
fourier_coeff (λ (x : , c * f x) n = c *
noncomputable def fourier_coeff_on {E : Type} [ 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} [ E] {a b : } (f : E) (n : ) (hab : a < b) :
f n = (1 / (b - a)) (x : ) in a..b, (fourier (-n)) x f x
theorem fourier_coeff_on.const_smul {E : Type} [ E] {a b : } (f : E) (c : ) (n : ) (hab : a < b) :
(c f) n = c f n
theorem fourier_coeff_on.const_mul {a b : } (f : ) (c : ) (n : ) (hab : a < b) :
(λ (x : ), c * f x) n = c * 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 : ) :
noncomputable def fourier_basis {T : } [hT : fact (0 < T)] :

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 L².

theorem fourier_basis_repr {T : } [hT : fact (0 < T)] (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)]  :
has_sum (λ (i : ), 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)]  :

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(, )) (n : ) :
theorem has_sum_fourier_series_of_summable {T : } [hT : fact (0 < T)] {f : C(, )} (h : summable ) :
has_sum (λ (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(, )} (h : summable ) (x : add_circle T) :
has_sum (λ (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) * 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 b (f' x) x) (hf' : b) :
f n = 1 / ((-2) * real.pi * complex.I * n) * ((fourier (-n)) a * (f b - f a) - (b - a) * f' n)

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