The asymptotic operator of a symmetric loop is symmetric

Proved

AsymptoticOperator.isSymmetric

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

asymptotic-operatorconley-zehnder-indexspectral-theorysymplectic-geometryunbounded-operator

Let $S:S^1\to\mathbb{R}^{2n\times2n}$ be continuous with $S(t)^{\mathsf T}=S(t)$ for all $t$ . Then

\langle A_Sf,g\rangle_{L^2}=\langle f,A_Sg\rangle_{L^2}\qquad\text{for all }f,g\in W^{1,2}(S^1,\mathbb{R}^{2n}).

Preamble

import Definitions.Def_AsymptoticOperator_Setting

Formal statement

namespace AsymptoticOperator

open ConleyZehnder

/-- Wendl §3.2, p. 55: for a loop of symmetric matrices, `A_S` is symmetric:
`⟨A_S f, g⟩ = ⟨f, A_S g⟩` for `f, g ∈ W^{1,2}`. -/
theorem isSymmetric {n : ℕ} (S : C(UnitAddCircle, Mat n)) (hS : IsSymLoop S) :
    (asymptoticOperator S).IsFormalAdjoint (asymptoticOperator S) := by sorry

end AsymptoticOperator

Source

Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, §3.2, p. 55

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Statement. For every $n \in \mathbb{N}$ (including $n = 0$ ) and every continuous map $S : S^1 \to \mathrm{Mat}_n$ such that $S(t)^{\mathsf T} = S(t)$ for every $t \in S^1$ , the operator $\mathcal A_S$ (defined below) satisfies

\langle \mathcal A_S f,\, g\rangle_{L^2} = \langle f,\, \mathcal A_S g\rangle_{L^2} \qquad\text{for all } f, g \in \operatorname{dom}\mathcal A_S .

Nothing else is asserted: in particular no density of the domain and no identification of the domain is part of this statement.

Meaning of the symbols.

$S^1 = \mathbb{R}/\mathbb{Z}$ with its Haar probability measure $\lambda$ ; $\mathrm{Mat}_n$ is the space of real $2n\times 2n$ matrices indexed by $\{1,\dots,n\}\sqcup\{1,\dots,n\}$ ; $J_0 = \begin{pmatrix} 0 & -I_n \\ I_n & 0\end{pmatrix}$ .
$V_n = \mathbb{R}^{2n}$ with the Euclidean inner product, and $L^2_n = L^2(S^1,\lambda;V_n)$ , the real Hilbert space of a.e.-classes of square-integrable maps with $\langle f, g\rangle_{L^2} = \int_{S^1} \langle f(t), g(t)\rangle\, d\lambda(t)$ . Pointwise values of an element of $L^2_n$ are those of an arbitrary measurable representative.
Fourier coefficients: $\hat f_k = \int_{S^1} e^{-2\pi i k t} f(t)\, d\lambda(t) \in \mathbb{C}^{2n}$ and $\widehat{(Sf)}_k = \int_{S^1} e^{-2\pi i k t} S(t) f(t)\, d\lambda(t)$ , $k\in\mathbb{Z}$ (real entries viewed in $\mathbb{C}$ ; Bochner integral, value $0$ if not integrable).
$f$ is "in $W^{1,2}$ " iff $\sum_{k\in\mathbb{Z}} (1+k^2)\sum_i |(\hat f_k)_i|^2$ is summable, $|\cdot|$ the complex modulus, $i$ over all $2n$ coordinates.
$\Gamma_S$ is the set of pairs $(f, g)\in L^2_n\times L^2_n$ with $f$ in $W^{1,2}$ and $\hat g_k = -(2\pi k\, i) J_0 \hat f_k - \widehat{(Sf)}_k$ for all $k\in\mathbb{Z}$ .
$\mathcal A_S$ is defined by cases: if some partially defined real-linear operator on $L^2_n$ has graph exactly $\Gamma_S$ , then $\mathcal A_S$ is such an operator (picked by choice); otherwise $\mathcal A_S$ is the zero operator with domain all of $L^2_n$ (for which the identity above holds trivially, both sides being $0$ ). The theorem is about this $\mathcal A_S$ whichever case occurs.

For $n = 0$ , $L^2_0 = \{0\}$ and the identity reads $0 = 0$ .

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Mazecto · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph