An integrable function on [0,1) with vanishing Fourier coefficients is zero

Proved

FiniteEnergyPlane.ae_eq_zero_of_fourier_eq_zero

by Mazecto · Nov 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

fourier-analysisharmonic-analysismeasure-theory

Let $H : \mathbb{R} \to \mathbb{C}$ be integrable on $[0,1)$ and suppose

\int_0^1 e^{2\pi i k t} H(t)\, dt = 0 \quad \text{for every } k \in \mathbb{Z}.

Then $H = 0$ almost everywhere on $[0,1)$ .

Role. Uniqueness of Fourier coefficients for $L^1$ functions on the circle $\mathbb{R}/\mathbb{Z}$ , stated for functions on the interval $[0,1)$ (the form in which loops in the $t$ -variable of the cylinder $\mathbb{R}\times S^1$ appear).

Preamble

import Mathlib

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Filter Topology Set
open scoped ContDiff Real

/-- An integrable `H : ℝ → ℂ` on `[0, 1)` all of whose Fourier coefficients
`∫₀¹ e^{2πikt} H(t) dt`, `k ∈ ℤ`, vanish is zero almost everywhere on `[0, 1)`. -/
theorem ae_eq_zero_of_fourier_eq_zero (H : ℝ → ℂ) (hH : IntegrableOn H (Ico 0 1))
    (h : ∀ k : ℤ, ∫ t in Ico (0 : ℝ) 1, Complex.exp (2 * π * Complex.I * k * t) * H t = 0) :
    ∀ᵐ t ∂(volume.restrict (Ico (0 : ℝ) 1)), H t = 0 := by
  sorry

end FiniteEnergyPlane

Source

Standard Fourier uniqueness; Lemma in the setting of U. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. AMS 364 (2012), arXiv:0812.4076

View graph