Uniqueness of Fourier coefficients and Fourier coefficients of products on the circle

Mathlib's fourierCoeff f n = ∫ t, e_{-n}(t) • f t is defined for every function f on AddCircle T, and Parseval's theorem shows that an L² function is determined by its Fourier coefficients. This file proves the corresponding statements for integrable functions and for products of two square-integrable functions, which in general are only integrable.

Uniqueness. An integrable function, with values in any complete normed complex space, whose Fourier coefficients all vanish is zero almost everywhere. Integration against f is a continuous linear functional on C(AddCircle T, ℂ) of norm at most ‖f‖₁; it vanishes on the monomials by hypothesis, hence on the uniformly dense span of trigonometric polynomials and on every continuous function. An integrable function orthogonal to all bounded continuous functions vanishes almost everywhere (MeasureTheory.Integrable.ae_eq_zero_of_forall_integral_smul_eq_zero).

Products. If f and g are square integrable, then f * g is integrable (Mathlib's MeasureTheory.MemLp.integrable_mul) and its Fourier coefficients are the convolution of those of f and g: (f g)^(n) = ∑ₘ f̂(m) ĝ(n - m), the series converging unconditionally. This is Parseval's identity ⟪u, v⟫ = ∑ₘ conj(û(m)) v̂(m) for u = conj f and v = e_{-n} g. Consequently, if the Fourier coefficients of f and g vanish below a and b respectively, then those of f * g vanish below a + b, and similarly above.

Together these compute products in the boundary Hardy theory: for instance, if f has only negative and g only nonpositive Fourier modes, then all modes of f * g are negative, and a product of square-integrable functions with no Fourier modes at all is zero almost everywhere. This is the Fourier-analytic input to Coburn's theorem that a nonzero Toeplitz operator or its adjoint is injective.

Main results

• MeasureTheory.Integrable.ae_eq_zero_of_forall_fourierCoeff_eq_zero: an integrable function on the circle with vanishing Fourier coefficients is zero almost everywhere;
• MeasureTheory.Integrable.ae_eq_of_forall_fourierCoeff_eq: integrable functions with the same Fourier coefficients agree almost everywhere;
• MeasureTheory.MemLp.hasSum_fourierCoeff_mul: for square-integrable f and g, (f g)^(n) = ∑ₘ f̂(m) ĝ(n - m);
• MeasureTheory.MemLp.fourierCoeff_mul_eq_zero_of_lt_add and MeasureTheory.MemLp.fourierCoeff_mul_eq_zero_of_add_lt: one-sided spectral support of a product.

References

• Y. Katznelson, An Introduction to Harmonic Analysis, third edition, Cambridge University Press (2004), Chapter I, §§1–2 (Fourier coefficients of products, and uniqueness).
• E. Park, Toeplitz operators, for the use of these facts in Coburn's theorem.

theorem MeasureTheory.Integrable.ae_eq_zero_of_forall_fourierCoeff_eq_zero {T : ℝ} [Fact (0 < T)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : AddCircle T → E} (hf : Integrable f AddCircle.haarAddCircle) (h : ∀ (n : ℤ), fourierCoeff f n = 0) : f =ᵐ[AddCircle.haarAddCircle] 0

Uniqueness of Fourier coefficients for integrable functions. An integrable function on the circle whose Fourier coefficients all vanish is zero almost everywhere.

theorem MeasureTheory.Integrable.ae_eq_of_forall_fourierCoeff_eq {T : ℝ} [Fact (0 < T)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f g : AddCircle T → E} (hf : Integrable f AddCircle.haarAddCircle) (hg : Integrable g AddCircle.haarAddCircle) (h : ∀ (n : ℤ), fourierCoeff f n = fourierCoeff g n) : f =ᵐ[AddCircle.haarAddCircle] g

Integrable functions on the circle with the same Fourier coefficients agree almost everywhere.

theorem MeasureTheory.MemLp.hasSum_fourierCoeff_mul {T : ℝ} [Fact (0 < T)] {f g : AddCircle T → ℂ} (hf : MemLp f 2 AddCircle.haarAddCircle) (hg : MemLp g 2 AddCircle.haarAddCircle) (n : ℤ) : HasSum (fun (m : ℤ) => fourierCoeff f m * fourierCoeff g (n - m)) (fourierCoeff (f * g) n)

Fourier coefficients of a product. If f and g are square integrable on the circle, then the Fourier coefficients of f * g are the convolution of those of f and g: (f g)^(n) = ∑ₘ f̂(m) ĝ(n - m).

theorem MeasureTheory.MemLp.fourierCoeff_mul_eq_zero_of_lt_add {T : ℝ} [Fact (0 < T)] {f g : AddCircle T → ℂ} (hf : MemLp f 2 AddCircle.haarAddCircle) (hg : MemLp g 2 AddCircle.haarAddCircle) {a b n : ℤ} (hfa : ∀ m < a, fourierCoeff f m = 0) (hgb : ∀ m < b, fourierCoeff g m = 0) (hn : n < a + b) : fourierCoeff (f * g) n = 0

If the Fourier coefficients of the square-integrable functions f and g vanish below a and b respectively, then those of f * g vanish below a + b.

theorem MeasureTheory.MemLp.fourierCoeff_mul_eq_zero_of_add_lt {T : ℝ} [Fact (0 < T)] {f g : AddCircle T → ℂ} (hf : MemLp f 2 AddCircle.haarAddCircle) (hg : MemLp g 2 AddCircle.haarAddCircle) {a b n : ℤ} (hfa : ∀ (m : ℤ), a < m → fourierCoeff f m = 0) (hgb : ∀ (m : ℤ), b < m → fourierCoeff g m = 0) (hn : a + b < n) : fourierCoeff (f * g) n = 0

If the Fourier coefficients of the square-integrable functions f and g vanish above a and b respectively, then those of f * g vanish above a + b.