Prove2Me

An element of L2(S1,R2n)L^2(S^1,\mathbb{R}^{2n}) with vanishing Fourier coefficients is zero

Proved
AsymptoticOperator.eq_zero_of_coeff_eq_zero

by Mazecto · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

asymptotic-operatorconley-zehnder-indexfourier-seriesunbounded-operator

Let S1=R/ZS^1=\mathbb R/\mathbb Z with its Haar probability measure and let Ln2=L2(S1,R2n)L^2_n=L^2(S^1,\mathbb R^{2n}). For f∈Ln2f\in L^2_n and k∈Zk\in\mathbb Z let f^k=∫S1e−2πiktf(t) dt∈C2n\hat f_k=\int_{S^1}e^{-2\pi ikt}f(t)\,dt\in\mathbb C^{2n} be its kk-th Fourier coefficient, computed componentwise after viewing the real entries of ff as complex numbers.

If g∈Ln2g\in L^2_n satisfies g^k=0\hat g_k=0 for every k∈Zk\in\mathbb Z, then g=0g=0 in Ln2L^2_n.

So an element of L2(S1,R2n)L^2(S^1,\mathbb R^{2n}) is determined by its Fourier coefficients. This is the basic uniqueness statement behind every definition in this mission that specifies an element of Ln2L^2_n through its Fourier coefficients, such as the asymptotic operator AS=−J0∂t−SA_S=-J_0\partial_t-S.

Formalization note: L2 n and coeff come from the definition module AsymptoticOperator_Setting; L2 n is Lp (EuclideanSpace ℝ (Fin n ⊕ Fin n)) 2 over UnitAddCircle with AddCircle.haarAddCircle, and coeff g k is the vector g^k\hat g_k.

Preamble
import Definitions.Def_AsymptoticOperator_Setting
Formal statement
namespace AsymptoticOperator

open ConleyZehnder

/-- An element of `L²(S¹, ℝ²ⁿ)` all of whose Fourier coefficients `ĝₖ ∈ ℂ²ⁿ` vanish is zero. -/
theorem eq_zero_of_coeff_eq_zero {n : ℕ} (g : L2 n) (h : ∀ k : ℤ, coeff g k = 0) :
    g = 0 := by sorry

end AsymptoticOperator
Source
Classical uniqueness of Fourier coefficients on L^2 of the circle (Katznelson, An Introduction to Harmonic Analysis, Chapter I, Section 2, uniqueness theorem); used for Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, §3.2, equation (3.4)

View graph