Fourier coefficients of a real $L^2$ loop are conjugate-symmetric

Proved

AsymptoticOperator.coeff_neg

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

asymptotic-operatorfourier-analysisspectral-theory

Let $f\in L^2(\mathbb{R}/\mathbb{Z},\mathbb{R}^{2n})$ (with the Haar probability measure) and let $\hat f_k=\int_{\mathbb{R}/\mathbb{Z}} e^{-2\pi i k t} f(t)\,dt\in\mathbb{C}^{2n}$ be its Fourier coefficients, computed componentwise on the complexification. Then for every $k\in\mathbb{Z}$ and every coordinate $i$ ,

(\hat f_{-k})_i=\overline{(\hat f_k)_i}.

Role: the reality condition on Fourier coefficients of real loops, used throughout the spectral theory of the asymptotic operators $A_S=-J_0\partial_t-S$ .

Formalization note: L2 n, coeff are from Definitions.Def_AsymptoticOperator_Setting; coordinates are indexed by Fin n ⊕ Fin n; complex conjugation is starRingEnd ℂ.

Preamble

import Definitions.Def_AsymptoticOperator_Setting

Formal statement

namespace AsymptoticOperator

open ConleyZehnder

/-- The Fourier coefficients of a real `L²` function on the circle are conjugate-symmetric:
`f̂₋ₖ = conj f̂ₖ` componentwise. -/
theorem coeff_neg {n : ℕ} (f : L2 n) (k : ℤ) (i : Fin n ⊕ Fin n) :
    coeff f (-k) i = (starRingEnd ℂ) (coeff f k i) := by sorry

end AsymptoticOperator

Source

Standard Fourier-analysis fact; used for Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, §3.4, p. 63

View graph

Fourier coefficients of a real L2L^2L2 loop are conjugate-symmetric

Fourier coefficients of a real $L^2$ loop are conjugate-symmetric