The asymptotic operator has compact resolvent

Proved

AsymptoticOperator.compact_resolvent

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 $\mu\in\mathbb{R}$ be such that $A_Sf=\mu f$ has no solution $f\ne0$ in $W^{1,2}$ . Then there is a compact bounded operator $R$ on $L^2(S^1,\mathbb{R}^{2n})$ with $R(L^2)\subset W^{1,2}$ , $(A_S-\mu)Rg=g$ for all $g\in L^2$ , and $R(A_S-\mu)f=f$ for all $f\in W^{1,2}$ .

So $A_S-\mu:W^{1,2}\to L^2$ is bijective with compact inverse.

Preamble

import Definitions.Def_AsymptoticOperator_Setting

Formal statement

namespace AsymptoticOperator

open ConleyZehnder

/-- Hofer–Wysocki–Zehnder (GAFA 1995), §3, p. 285 for `n = 1`: if `μ ∈ ℝ` is not an eigenvalue of `A_S`, then `A_S - μ : W^{1,2} → L²` is a
bijection whose inverse is a compact operator on `L²(S¹, ℝ²ⁿ)`. -/
theorem compact_resolvent {n : ℕ} (S : C(UnitAddCircle, Mat n)) (hS : IsSymLoop S) (μ : ℝ)
    (hμ : eigenspace (asymptoticOperator S) μ = ⊥) :
    ∃ R : L2 n →L[ℝ] L2 n, IsCompactOperator R ∧
      (∀ g : L2 n, ∃ h : R g ∈ (asymptoticOperator S).domain,
        (asymptoticOperator S) ⟨R g, h⟩ - μ • R g = g) ∧
      ∀ f : (asymptoticOperator S).domain,
        R ((asymptoticOperator S) f - μ • (f : L2 n)) = f := by sorry

end AsymptoticOperator

Source

Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, §3.2, p. 46 and Lemma 3.16 (the compact resolvent is not stated there explicitly); 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, after equation (35) (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. 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$ ), and 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$ and the associated norm topology. 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.

For $\mu \in \mathbb{R}$ , the eigenspace $E_\mu(A_S)$ is the real linear subspace $\{ f \in D(A_S) : A_S f = \mu f \}$ of $D(A_S)$ ; " $E_\mu(A_S) = 0$ " means it contains only the zero vector.

Statement. Let $n \in \mathbb{N}$ , let $S : \mathbb{T} \to \mathrm{Mat}_n$ be continuous with $S(t)$ symmetric for every $t \in \mathbb{T}$ , and let $\mu \in \mathbb{R}$ be such that $E_\mu(A_S) = \{0\}$ , i.e. the only $f \in D(A_S)$ with $A_S f = \mu f$ is $f = 0$ . Then there exists a bounded (continuous) real-linear operator $R : H \to H$ such that

$R$ is a compact operator (it maps some neighbourhood of $0$ into a set with compact closure);
for every $g \in H$ , $Rg \in D(A_S)$ and $A_S(Rg) - \mu\, Rg = g$ ;
for every $f \in D(A_S)$ , $R\big(A_S f - \mu f\big) = f$ .

No other hypotheses are assumed. For $n = 0$ , $H = \{0\}$ and $R = 0$ satisfies the conclusion.

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