Prove2Me

Square-summable conjugate-symmetric sequences are Fourier coefficients of L2(S1,R2n)L^2(S^1,\mathbb{R}^{2n}) functions

Proved
AsymptoticOperator.exists_coeff_eq

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.

Let c:Z→C2nc:\mathbb Z\to\mathbb C^{2n} satisfy ∑k∈Z∣ck∣2<∞\sum_{k\in\mathbb Z}|c_k|^2<\infty and c−k=ck‾c_{-k}=\overline{c_k} (componentwise) for every kk. Then there is h∈Ln2h\in L^2_n with h^k=ck\hat h_k=c_k for every k∈Zk\in\mathbb Z.

Together with the uniqueness of Fourier coefficients, this identifies L2(S1,R2n)L^2(S^1,\mathbb R^{2n}) with the conjugate-symmetric square-summable sequences in C2n\mathbb C^{2n}. It is used to produce elements of Ln2L^2_n from prescribed Fourier coefficients, for example the image −J0∂tf-J_0\partial_tf of an element of W1,2W^{1,2}.

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 h k is the vector h^k\hat h_k. Square-summability is stated as summability of k↦∑i∣cki∣2k\mapsto\sum_i|c_k^i|^2, and conjugate symmetry componentwise with starRingEnd ℂ.

Preamble
import Definitions.Def_AsymptoticOperator_Setting
Formal statement
namespace AsymptoticOperator

open ConleyZehnder

/-- Every square-summable, conjugate-symmetric family `c : ℤ → ℂ²ⁿ` is the sequence of
Fourier coefficients of an element of `L²(S¹, ℝ²ⁿ)`. -/
theorem exists_coeff_eq {n : ℕ} (c : ℤ → Fin n ⊕ Fin n → ℂ)
    (hsum : Summable fun k : ℤ => ∑ i, ‖c k i‖ ^ 2)
    (hconj : ∀ k i, c (-k) i = (starRingEnd ℂ) (c k i)) :
    ∃ h : L2 n, ∀ k : ℤ, coeff h k = c k := by sorry

end AsymptoticOperator
Source
Riesz–Fischer theorem on the circle (Katznelson, An Introduction to Harmonic Analysis, Chapter I, Section 5); used for Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, §3.2, equation (3.4)

View graph