The asymptotic operator $-J_0\partial_t - S$ is a well-defined linear operator on $L^2(S^1,\mathbb{R}^{2n})$

Proved

AsymptoticOperator.graph_existsUnique

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. There is exactly one partially defined linear map $A$ on $L^2(S^1,\mathbb{R}^{2n})$ whose graph is the set of pairs $(f,g)$ with $f\in W^{1,2}$ and

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

So $A_S=-J_0\partial_t-S$ is a well-defined unbounded operator, and asymptoticOperator S is this map.

Preamble

import Definitions.Def_AsymptoticOperator_Setting

Formal statement

namespace AsymptoticOperator

open ConleyZehnder

/-- Wendl §3.2, (3.4): `A_S = -J₀ ∂ₜ - S` is a well-defined linear operator on
`L²(S¹, ℝ²ⁿ)`: exactly one partially defined linear map has graph `graphSet S`. -/
theorem graph_existsUnique {n : ℕ} (S : C(UnitAddCircle, Mat n)) :
    ∃! A : L2 n →ₗ.[ℝ] L2 n, (A.graph : Set (L2 n × L2 n)) = graphSet S := 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); 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) (n = 1)

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$ — no symmetry or other hypothesis on $S$ — there exists exactly one partially defined real-linear operator $A$ on $L^2_n$ (a linear subspace $\operatorname{dom} A \subseteq L^2_n$ with a linear map $\operatorname{dom} A \to L^2_n$ ) whose graph $\{(x, Ax) : x \in \operatorname{dom} A\}$ equals the set $\Gamma_S$ below.

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)$ (a.e.-classes of square-integrable maps, inner product $\int \langle f, g\rangle\, d\lambda$ ). Pointwise values of an element of $L^2_n$ are those of an arbitrary measurable representative.
For $f : S^1 \to V_n$ and $k \in \mathbb{Z}$ : $\hat f_k = \int_{S^1} e^{-2\pi i k t} f(t)\, d\lambda(t) \in \mathbb{C}^{2n}$ (entries of $f$ viewed as complex numbers; Bochner integral, set to $0$ if the integrand is not integrable), and $\widehat{(Sf)}_k = \int_{S^1} e^{-2\pi i k t} S(t) f(t)\, d\lambda(t) \in \mathbb{C}^{2n}$ (same conventions).
$f \in L^2_n$ is "in $W^{1,2}$ " iff $\sum_{k\in\mathbb{Z}} (1+k^2)\sum_i |(\hat f_k)_i|^2$ is summable (finite), with $|\cdot|$ the complex modulus over all $2n$ coordinates.
$\Gamma_S$ is the set of pairs $(f, g) \in L^2_n \times L^2_n$ such that $f$ is in $W^{1,2}$ and, for every $k \in \mathbb{Z}$ ,

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

So the assertion is: $\Gamma_S$ is the graph of some partially defined linear operator (i.e. it is a linear subspace of $L^2_n\times L^2_n$ in which each first coordinate occurs with at most one second coordinate), and that operator is unique. For $n = 0$ all spaces are $\{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

The asymptotic operator −J0∂t−S-J_0\partial_t - S−J0​∂t​−S is a well-defined linear operator on L2(S1,R2n)L^2(S^1,\mathbb{R}^{2n})L2(S1,R2n)

The asymptotic operator $-J_0\partial_t - S$ is a well-defined linear operator on $L^2(S^1,\mathbb{R}^{2n})$