Asymptotic operators $-J_0\partial_t - S$ on $L^2(S^1,\mathbb{R}^{2n})$ and fundamental solutions

Definition

AsymptoticOperator_Setting

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

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

Objects for the spectral theory of asymptotic operators on the circle, following Wendl, Lectures on Symplectic Field Theory, §3.2.

Circle and $L^2$ . $S^1=\mathbb{R}/\mathbb{Z}$ with its Haar probability measure. $L^2=L^2(S^1,\mathbb{R}^{2n})$ is the real Hilbert space of square-integrable maps to $\mathbb{R}^{2n}$ with the Euclidean inner product.
Loops of symmetric matrices. $S:S^1\to\mathbb{R}^{2n\times2n}$ is continuous; it is a symmetric loop if $S(t)^{\mathsf T}=S(t)$ for every $t$ .
Fourier coefficients. $\hat f_k=\int_{S^1}e^{-2\pi ikt}f(t)\,dt\in\mathbb{C}^{2n}$ , $k\in\mathbb{Z}$ , and $(Sf)^\wedge_k$ is the coefficient of $t\mapsto S(t)f(t)$ .
Sobolev space. $W^{1,2}$ is the set of $f\in L^2$ with $\sum_k(1+k^2)|\hat f_k|^2<\infty$ .
Asymptotic operator. With

J_0=\begin{pmatrix}0&-\mathrm{Id}\\ \mathrm{Id}&0\end{pmatrix},

$A_Sf=g$ means $f\in W^{1,2}$ and $\hat g_k=-2\pi ik\,J_0\hat f_k-(Sf)^\wedge_k$ for all $k$ , i.e. $A_S=-J_0\partial_t-S(t)$ (Wendl (3.4)). $A_S$ is the partially defined linear map on $L^2$ with this graph. 6. Eigenspaces and discrete spectrum. The $\mu$ -eigenspace is $\ker(A_S-\mu)\subset W^{1,2}$ . $A$ has a discrete eigenbasis if $L^2$ has an orthonormal basis $(e_i)$ of vectors in the domain with $Ae_i=\lambda_ie_i$ , $\lambda_i\in\mathbb{R}$ , and $|\lambda_i|\to\infty$ along the cofinite filter (only finitely many $i$ have $|\lambda_i|\le c$ , for every $c$ ). 7. Fundamental solution. $\Psi:\mathbb{R}\to\mathbb{R}^{2n\times2n}$ with $\Psi(0)=\mathrm{Id}$ and $\Psi'(t)=J_0S(t)\Psi(t)$ for all $t\in\mathbb{R}$ .

Formalization Note $L^2$ is Lp (EuclideanSpace ℝ (Fin n ⊕ Fin n)) 2 haarAddCircle on UnitAddCircle. Fourier coefficients are Mathlib's fourierCoeff of the componentwise complexification, and $J_0$ (Matrix.J) and $S(t)$ act on $\mathbb{C}^{2n}$ by the real-to-complex coercion. asymptoticOperator S is chosen as the LinearPMap whose graph is the set of pairs $(f,g)$ above and is $0$ if no such map exists; a separate theorem shows that it exists. Mat n, J₀, IsSymplectic and SP come from ConleyZehnder_Setting.

Definition code

import Definitions.Def_ConleyZehnder_Setting
import Mathlib.Analysis.Fourier.AddCircle
import Mathlib.Analysis.InnerProductSpace.LinearPMap
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Analysis.Normed.Operator.Compact.Basic
import Mathlib.MeasureTheory.Function.L2Space

/-!
# Asymptotic operators on the circle

Wendl, *Lectures on Symplectic Field Theory*, arXiv:1612.01009, §3.2, equation (3.4):
for a loop `S : S¹ → ℝ^{2n×2n}` of symmetric matrices, the asymptotic operator
`A_S = -J₀ ∂ₜ - S(t)` acts on `L²(S¹, ℝ²ⁿ)` with domain `W^{1,2}(S¹, ℝ²ⁿ)`.

Conventions. `S¹ = ℝ/ℤ` (`UnitAddCircle`) with its Haar probability measure. `ℝ²ⁿ` is
`EuclideanSpace ℝ (Fin n ⊕ Fin n)` and `J₀ = Matrix.J`, as in `ConleyZehnder_Setting`.
The `k`-th Fourier coefficient of `f : S¹ → ℝ²ⁿ` is `f̂ₖ = ∫ e^{-2πikt} f(t) dt ∈ ℂ²ⁿ`,
computed componentwise on the complexification. `W^{1,2}` is the set of `f ∈ L²` with
`∑ₖ (1 + k²) |f̂ₖ|² < ∞`, and `A_S f = g` means `ĝₖ = -2πik J₀ f̂ₖ - (S f)^ₖ` for all `k`,
i.e. `g = -J₀ f' - S f` with the derivative taken in `L²`.

The fundamental solution of `S` is `Ψ : ℝ → ℝ^{2n×2n}` with `Ψ(0) = Id` and
`Ψ' = J₀ S Ψ`; these are the solutions of `(-J₀ ∂ₜ - S) Ψ = 0`.
-/

namespace AsymptoticOperator

noncomputable section

open MeasureTheory Matrix Classical ConleyZehnder

/-- `ℝ²ⁿ` with its Euclidean inner product, coordinates indexed by `Fin n ⊕ Fin n`. -/
abbrev Vec (n : ℕ) := EuclideanSpace ℝ (Fin n ⊕ Fin n)

/-- `L²(S¹, ℝ²ⁿ)` for `S¹ = ℝ/ℤ` with the Haar probability measure. -/
abbrev L2 (n : ℕ) := Lp (Vec n) 2 (AddCircle.haarAddCircle : Measure UnitAddCircle)

variable {n : ℕ}

/-- A loop `S : S¹ → ℝ^{2n×2n}` of symmetric matrices. -/
def IsSymLoop (S : C(UnitAddCircle, Mat n)) : Prop := ∀ t, (S t).IsSymm

/-- The complexification `ℝ²ⁿ → ℂ²ⁿ` of a vector. -/
def complexify (v : Vec n) : Fin n ⊕ Fin n → ℂ := fun i => ((v i : ℝ) : ℂ)

/-- The `k`-th Fourier coefficient `f̂ₖ = ∫ e^{-2πikt} f(t) dt ∈ ℂ²ⁿ`. -/
def coeff (f : UnitAddCircle → Vec n) (k : ℤ) : Fin n ⊕ Fin n → ℂ :=
  fourierCoeff (fun t => complexify (f t)) k

/-- The `k`-th Fourier coefficient of `t ↦ S(t) f(t)`. -/
def coeffMul (S : C(UnitAddCircle, Mat n)) (f : UnitAddCircle → Vec n) (k : ℤ) :
    Fin n ⊕ Fin n → ℂ :=
  fourierCoeff (fun t => (S t).map (fun x : ℝ => (x : ℂ)) *ᵥ complexify (f t)) k

/-- `f ∈ W^{1,2}(S¹, ℝ²ⁿ)`: `∑ₖ (1 + k²) |f̂ₖ|² < ∞`. -/
def InW12 (f : L2 n) : Prop :=
  Summable fun k : ℤ => (1 + (k : ℝ) ^ 2) * ∑ i, ‖coeff f k i‖ ^ 2

/-- `A_S f = g`: `f ∈ W^{1,2}` and `ĝₖ = -2πik J₀ f̂ₖ - (S f)^ₖ` for every `k ∈ ℤ`,
that is, `g = -J₀ f' - S f`. -/
def IsAsymptoticAction (S : C(UnitAddCircle, Mat n)) (f g : L2 n) : Prop :=
  InW12 f ∧ ∀ k : ℤ, coeff g k =
    -((2 * Real.pi * k : ℝ) * Complex.I) • ((J₀ n).map (fun x : ℝ => (x : ℂ)) *ᵥ coeff f k) -
      coeffMul S f k

/-- The graph `{(f, A_S f)}` of the asymptotic operator, as a set of pairs. -/
def graphSet (S : C(UnitAddCircle, Mat n)) : Set (L2 n × L2 n) :=
  {p | IsAsymptoticAction S p.1 p.2}

/-- Wendl (3.4): the asymptotic operator `A_S = -J₀ ∂ₜ - S` as an unbounded operator on
`L²(S¹, ℝ²ⁿ)`: the partially defined linear map whose graph is `graphSet S` (chosen,
with fallback `0` if no such map exists). -/
def asymptoticOperator (S : C(UnitAddCircle, Mat n)) : L2 n →ₗ.[ℝ] L2 n :=
  if h : ∃ A : L2 n →ₗ.[ℝ] L2 n, (A.graph : Set (L2 n × L2 n)) = graphSet S then h.choose
  else 0

/-- `A` has an orthonormal basis of eigenvectors in its domain with real eigenvalues
`ev i`, and `|ev i| → ∞` along the cofinite filter (each bounded set of eigenvalues is
attained by finitely many basis vectors). -/
def HasDiscreteEigenbasis (A : L2 n →ₗ.[ℝ] L2 n) : Prop :=
  ∃ (ι : Type) (b : HilbertBasis ι ℝ (L2 n)) (ev : ι → ℝ),
    (∀ i, ∃ h : b i ∈ A.domain, A ⟨b i, h⟩ = ev i • b i) ∧
      Filter.Tendsto (fun i => |ev i|) Filter.cofinite Filter.atTop

/-- The eigenspace `ker(A - μ)`, as a subspace of the domain of `A`. -/
def eigenspace (A : L2 n →ₗ.[ℝ] L2 n) (μ : ℝ) : Submodule ℝ A.domain :=
  LinearMap.ker (A.toFun - μ • A.domain.subtype)

/-- `Ψ : ℝ → ℝ^{2n×2n}` is the fundamental solution of `S`: `Ψ(0) = Id` and
`Ψ'(t) = J₀ S(t) Ψ(t)` for all `t`. -/
def IsFundamentalSolution (S : C(UnitAddCircle, Mat n)) (Ψ : ℝ → Mat n) : Prop :=
  Ψ 0 = 1 ∧ ∀ t : ℝ, HasDerivAt Ψ (J₀ n * S (t : UnitAddCircle) * Ψ t) t

end

end AsymptoticOperator

Source

Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Lecture 3: Section 3.2, equation (3.4), p. 46; Section 3.4, Exercise 3.29, 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, pp. 285-288, equation (35)

Read-back

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

Read-back of the definition module (namespace AsymptoticOperator). Throughout, $n \in \mathbb{N}$ is arbitrary, including $n = 0$ . Two notions are imported from the Conley–Zehnder setting: $\mathrm{Mat}_n$ is the space of real $2n \times 2n$ matrices whose rows and columns are indexed by the disjoint union $\{1,\dots,n\} \sqcup \{1,\dots,n\}$ (first block, second block), and $J_0$ is the block matrix

J_0 = \begin{pmatrix} 0 & -I_n \\ I_n & 0 \end{pmatrix}.

The circle is $S^1 = \mathbb{R}/\mathbb{Z}$ ; "continuous loop" means a continuous map $S^1 \to \mathrm{Mat}_n$ (matrix topology = entrywise topology). The measure on $S^1$ is the Haar probability measure $\lambda$ (total mass $1$ ; it is Lebesgue measure on $[0,1)$ under the obvious identification).

Spaces.

$V_n = \mathbb{R}^{2n}$ with coordinates indexed by $\{1,\dots,n\} \sqcup \{1,\dots,n\}$ and the standard Euclidean inner product $\langle u, v\rangle = \sum_i u_i v_i$ and norm $|v| = (\sum_i v_i^2)^{1/2}$ .
$L^2_n = L^2(S^1, \lambda; V_n)$ : equivalence classes (modulo $\lambda$ -a.e. equality) of measurable $f : S^1 \to V_n$ with $\int |f|^2\, d\lambda < \infty$ , a real Hilbert space with inner product $\langle f, g\rangle_{L^2} = \int_{S^1} \langle f(t), g(t)\rangle\, d\lambda(t)$ . Whenever a pointwise value of $f \in L^2_n$ is used below, it is taken from a fixed (arbitrary) measurable representative. For $n = 0$ , $V_0 = \{0\}$ and $L^2_0 = \{0\}$ .

Definitions.

Symmetric loop. For a continuous $S : S^1 \to \mathrm{Mat}_n$ , " $S$ is a symmetric loop" means $S(t)^{\mathsf T} = S(t)$ for every $t \in S^1$ .
Complexification. For $v \in V_n$ , $v^{\mathbb C} \in \mathbb{C}^{2n}$ is the vector with the same entries viewed as complex numbers.
Fourier coefficients. For any function $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)^{\mathbb C}\, d\lambda(t) \in \mathbb{C}^{2n},

a Bochner integral of a $\mathbb{C}^{2n}$ -valued function (here $e^{-2\pi i k t}$ is well defined on $\mathbb{R}/\mathbb{Z}$ ). By the Bochner-integral convention, if the integrand is not integrable the value is $0 \in \mathbb{C}^{2n}$ . For $f \in L^2_n$ this is applied to a representative of $f$ (the value does not depend on the choice).

Fourier coefficients of $Sf$ . For continuous $S : S^1 \to \mathrm{Mat}_n$ and $f : S^1 \to V_n$ ,

\widehat{(Sf)}_k = \int_{S^1} e^{-2\pi i k t}\, S(t)^{\mathbb C} f(t)^{\mathbb C}\, d\lambda(t) \in \mathbb{C}^{2n},

where $S(t)^{\mathbb C}$ is $S(t)$ with entries viewed in $\mathbb{C}$ (same junk convention: $0$ if not integrable). For $f \in L^2_n$ ( $\lambda$ is a probability measure) and continuous $S$ , the integrands in 3 and 4 are integrable, so the junk value does not arise for elements of $L^2_n$ .

The space $W^{1,2}$ . $f \in L^2_n$ is "in $W^{1,2}$ " iff the family of nonnegative reals

k \mapsto (1 + k^2) \sum_{i} \big|(\hat f_k)_i\big|^2, \qquad k \in \mathbb{Z},

is summable over $\mathbb{Z}$ , where $|\cdot|$ is the complex modulus and $i$ runs over all $2n$ coordinates. (For $n = 0$ every $f$ qualifies.)

The action relation. For continuous $S$ and $f, g \in L^2_n$ , " $A_S f = g$ " means: $f \in W^{1,2}$ (as in 5) and for every $k \in \mathbb{Z}$ ,

\hat g_k = -(2\pi k\, i)\, J_0^{\mathbb C}\, \hat f_k \;-\; \widehat{(Sf)}_k

as an identity in $\mathbb{C}^{2n}$ , with $J_0^{\mathbb C}$ the complexified matrix $J_0$ . No condition is imposed on $g$ other than these coefficient identities, and no symmetry of $S$ is assumed.

The graph set. $\Gamma_S = \{(f, g) \in L^2_n \times L^2_n : A_S f = g \text{ in the sense of } 6\}$ , a plain subset of $L^2_n \times L^2_n$ .
The asymptotic operator. $\mathcal A_S$ is a partially defined real-linear operator on $L^2_n$ (a linear subspace $D \subseteq L^2_n$ , its domain, together with a linear map $D \to L^2_n$ ). It is defined by cases: if there exists a partially defined linear operator $A$ whose graph $\{(x, Ax) : x \in \operatorname{dom} A\}$ equals $\Gamma_S$ as a set, then $\mathcal A_S$ is one such operator picked by the axiom of choice; otherwise (fallback / junk value) $\mathcal A_S$ is the zero operator, whose domain is all of $L^2_n$ and which sends every element to $0$ . (Remark: a partially defined operator is determined by its graph.)
Discrete eigenbasis. For a partially defined linear operator $A$ on $L^2_n$ , " $A$ has a discrete eigenbasis" means: there exist an index set $\iota$ , a Hilbert (complete orthonormal) basis $(b_i)_{i\in\iota}$ of the real Hilbert space $L^2_n$ , and real numbers $(\mathrm{ev}_i)_{i\in\iota}$ such that
- every $b_i$ lies in the domain of $A$ and $A b_i = \mathrm{ev}_i\, b_i$ ; and
- $|\mathrm{ev}_i| \to \infty$ along the cofinite filter on $\iota$ , i.e. for every $R$ only finitely many $i$ have $|\mathrm{ev}_i| \le R$ (if $\iota$ is finite this condition holds automatically; for $n = 0$ , $\iota = \varnothing$ is admissible).
Eigenspace. For $A$ as in 9 and $\mu \in \mathbb{R}$ , $E_\mu(A)$ is the kernel of $x \mapsto Ax - \mu x$ on the domain of $A$ , i.e. $\{x \in \operatorname{dom} A : Ax = \mu x\}$ , regarded as a linear subspace of $\operatorname{dom} A$ (not of $L^2_n$ ).
Fundamental solution. For continuous $S : S^1 \to \mathrm{Mat}_n$ and any function $\Psi : \mathbb{R} \to \mathrm{Mat}_n$ , " $\Psi$ is a fundamental solution of $S$ " means $\Psi(0) = I_{2n}$ and, for every real $t$ , $\Psi$ is differentiable at $t$ with

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

where $[t]$ is the class of $t$ in $\mathbb{R}/\mathbb{Z}$ (so $S$ is evaluated $1$ -periodically) and the products are matrix products.

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

Asymptotic operators −J0∂t−S-J_0\partial_t - S−J0​∂t​−S on L2(S1,R2n)L^2(S^1,\mathbb{R}^{2n})L2(S1,R2n) and fundamental solutions

Asymptotic operators $-J_0\partial_t - S$ on $L^2(S^1,\mathbb{R}^{2n})$ and fundamental solutions