Spectral theory of asymptotic operators on the circle

Proved

AsymptoticOperator.spectral_theory

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$ , and let $A_S=-J_0\partial_t-S$ with domain $W^{1,2}(S^1,\mathbb{R}^{2n})$ . Then:

$A_S$ is self-adjoint on $L^2(S^1,\mathbb{R}^{2n})$ ;
$L^2(S^1,\mathbb{R}^{2n})$ has an orthonormal basis of eigenvectors of $A_S$ in $W^{1,2}$ , with real eigenvalues of finite multiplicity accumulating only at $\pm\infty$ ;
for the fundamental solution $\Psi$ ( $\Psi(0)=\mathrm{Id}$ , $\Psi'=J_0S\Psi$ ), $\ker A_S\cong\ker(\Psi(1)-\mathrm{Id})$ .

These are the basic analytic properties of the operator through which periodic orbits enter the Fredholm theory of Cauchy–Riemann operators.

Preamble

import Definitions.Def_AsymptoticOperator_Setting

Formal statement

namespace AsymptoticOperator

open ConleyZehnder

/-- Spectral theory of the asymptotic operator: for a loop `S` of symmetric matrices,
`A_S = -J₀ ∂ₜ - S` with domain `W^{1,2}` is self-adjoint, `L²(S¹, ℝ²ⁿ)` has an
orthonormal eigenbasis whose real eigenvalues have finite multiplicity and accumulate
only at `±∞`, and `ker A_S ≅ ker(Ψ(1) - Id)` for the fundamental solution `Ψ`. -/
theorem spectral_theory {n : ℕ} (S : C(UnitAddCircle, Mat n)) (hS : IsSymLoop S) :
    IsSelfAdjoint (asymptoticOperator S) ∧ HasDiscreteEigenbasis (asymptoticOperator S) ∧
      ∀ Ψ : ℝ → Mat n, IsFundamentalSolution S Ψ →
        Nonempty (eigenspace (asymptoticOperator S) 0 ≃ₗ[ℝ]
          LinearMap.ker (Matrix.toLin' (Ψ 1 - 1))) := by sorry

end AsymptoticOperator

Source

Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, §3.2, equation (3.4), p. 46; §3.4, Exercise 3.29 and p. 61; Hofer-Wysocki-Zehnder, Properties of pseudoholomorphic curves in symplectisations II, GAFA 5 (1995) 270-328, https://doi.org/10.1007/BF01895669, Section 3, p. 285, equation (35) and the paragraph after it (n = 1)

Read-back

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

Setting. Let $n \in \mathbb{N}$ be arbitrary ( $n = 0$ is allowed). Let $I = \{1,\dots,n\} \sqcup \{1,\dots,n\}$ (a first and a second copy), $V_n = \mathbb{R}^I \cong \mathbb{R}^{2n}$ with the standard Euclidean inner product, and $\mathrm{Mat}_n$ the real $I \times I$ (i.e. $2n \times 2n$ ) matrices, with identity $\mathrm{Id}$ . In block form with respect to the two copies, $J_0 = \begin{pmatrix} 0 & -\mathrm{Id}_n \\ \mathrm{Id}_n & 0 \end{pmatrix}$ . Let $\mathbb{T} = \mathbb{R}/\mathbb{Z}$ with its Haar probability measure $dt$ (total mass $1$ ); for $t \in \mathbb{R}$ write $[t]$ for its class in $\mathbb{T}$ . Let $H = L^2(\mathbb{T}, V_n)$ be the real Hilbert space of a.e.-classes of square-integrable functions, with $\langle f, g \rangle = \int_{\mathbb{T}} \langle f(t), g(t) \rangle \, dt$ . For $n = 0$ , $V_0 = \{0\}$ and $H = \{0\}$ .

For $f \in H$ (any representative) and $k \in \mathbb{Z}$ , the Fourier coefficient is the vector $\hat f_k = \int_{\mathbb{T}} e^{-2\pi i k t} f(t)\, dt \in \mathbb{C}^I$ , where $f(t)$ is regarded as a complex vector componentwise; for a continuous map $S : \mathbb{T} \to \mathrm{Mat}_n$ , $\widehat{(Sf)}_k = \int_{\mathbb{T}} e^{-2\pi i k t} S(t) f(t)\, dt \in \mathbb{C}^I$ (with $S(t)$ regarded as a complex matrix). These are Bochner integrals (which by convention are $0$ when the integrand is not integrable). Say $f \in W^{1,2}$ if the family $\big((1 + k^2) \sum_{i \in I} |(\hat f_k)_i|^2\big)_{k \in \mathbb{Z}}$ is summable. Let $G_S \subseteq H \times H$ be the set of pairs $(f, g)$ with $f \in W^{1,2}$ and

\hat g_k = -2\pi i k \, J_0 \hat f_k - \widehat{(Sf)}_k \quad \text{for all } k \in \mathbb{Z}.

The operator $A_S$ is defined as follows: if there exists a partially defined linear map on $H$ (a linear subspace $D \subseteq H$ and a linear map $T : D \to H$ ) whose graph $\{(x, Tx) : x \in D\}$ equals $G_S$ , then $A_S$ is such a map, chosen by the axiom of choice (its domain $D(A_S)$ is then $\{f : \exists g,\ (f,g) \in G_S\}$ and $A_S f$ is the corresponding $g$ ); if no such map exists, $A_S$ is the zero map with domain all of $H$ . The statement does not itself assert which case occurs.

Self-adjointness. For a partially defined linear map $A$ on $H$ with domain $D(A)$ , its adjoint $A^*$ has domain $D(A^*) = \{ y \in H : x \mapsto \langle y, Ax \rangle \text{ is continuous on } D(A) \}$ ; if $D(A)$ is dense in $H$ , $A^* y$ is the unique $z \in H$ with $\langle z, x \rangle = \langle y, Ax \rangle$ for all $x \in D(A)$ , and if $D(A)$ is not dense, $A^*$ is by convention the zero map on $D(A^*)$ . " $A$ is self-adjoint" means $A^* = A$ as partially defined maps: $D(A^*) = D(A)$ and $A^* y = A y$ for all $y$ in this common domain.

Discrete eigenbasis. " $A$ has a discrete eigenbasis" means: there exist an index set $\iota$ , a Hilbert basis $(b_i)_{i \in \iota}$ of $H$ (an orthonormal family with dense linear span), and real numbers $(\lambda_i)_{i \in \iota}$ such that every $b_i$ lies in $D(A)$ with $A b_i = \lambda_i b_i$ , and $|\lambda_i| \to \infty$ along the cofinite filter on $\iota$ , i.e. for every $C \in \mathbb{R}$ the set $\{ i \in \iota : |\lambda_i| \le C \}$ is finite (automatic when $\iota$ is finite).

Kernel. $E_0(A_S) = \{ f \in D(A_S) : A_S f = 0 \}$ , a real linear subspace of $D(A_S)$ .

Fundamental solution. A map $\Psi : \mathbb{R} \to \mathrm{Mat}_n$ is a fundamental solution of $S$ if $\Psi(0) = \mathrm{Id}$ and, for every $t \in \mathbb{R}$ , $\Psi$ is differentiable at $t$ (entrywise) with

\Psi'(t) = J_0 \, S([t]) \, \Psi(t).

Statement. Let $n \in \mathbb{N}$ and let $S : \mathbb{T} \to \mathrm{Mat}_n$ be continuous with $S(t)$ symmetric ( $S(t)^{\mathsf T} = S(t)$ ) for every $t \in \mathbb{T}$ . Then all three of the following hold:

$A_S$ is self-adjoint in the above sense.
$A_S$ has a discrete eigenbasis in the above sense.
For every $\Psi : \mathbb{R} \to \mathrm{Mat}_n$ that is a fundamental solution of $S$ , there exists a real-linear isomorphism

E_0(A_S) \;\cong\; \ker\big(\Psi(1) - \mathrm{Id}\big) = \{ v \in \mathbb{R}^I : \Psi(1) v = v \},

where $\Psi(1) - \mathrm{Id}$ acts on column vectors $v \in \mathbb{R}^I \cong \mathbb{R}^{2n}$ by matrix multiplication. The isomorphism is only required to exist; no particular map is specified. Part 3 is quantified over all fundamental solutions and asserts nothing if none exists.

No other hypotheses are assumed. For $n = 0$ , $H = \{0\}$ and $\mathbb{R}^I = \mathbb{R}^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