Cauchy–Riemann operators on the cylinder with nondegenerate asymptotics are Fredholm

Proved

CauchyRiemannIndex.isFredholm

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

cauchy-riemannconley-zehnder-indexfredholm-indexsobolev-spacessymplectic-geometry

Let $1<p<\infty$ , let $S^\pm$ be continuous loops of symmetric matrices and let $S:\mathbb{R}\times S^1\to\mathbb{R}^{2n\times2n}$ be continuous with $S(s,\cdot)\to S^\pm$ uniformly as $s\to\pm\infty$ ; $D_S=\partial_s+J_0\partial_t+S(s,t)$ . Assume that the asymptotic operators $A^\pm=-J_0\partial_t-S^\pm(t)$ are nondegenerate. Then $D_S:W^{1,p}(\mathbb{R}\times S^1,\mathbb{R}^{2n})\to L^p(\mathbb{R}\times S^1,\mathbb{R}^{2n})$ is Fredholm.

Formalization Note $p$ is in ℝ≥0∞ with Fact (1 ≤ p), $1<p$ and $p\ne\infty$ . The hypotheses on $S$ are IsSymLoop S± and IsAsymptoticTo S Splus Sminus. Nondegeneracy is IsNondegenerate S±: $\det(\mathrm{Id}-\Psi(1))\ne0$ for the fundamental solution $\Psi$ . "Fredholm" is IsFredholmCR p S: finite-dimensional kernel, closed range, finite-dimensional cokernel.

Preamble

import Definitions.Def_CauchyRiemannIndex_Setting
import Mathlib.Analysis.Calculus.ContDiff.Basic

Formal statement

namespace CauchyRiemannIndex

open MeasureTheory Matrix Filter Topology
open scoped ENNReal NNReal ContDiff RealInnerProductSpace

/-- Wendl, Theorem 4.3 (p. 69), Fredholm property, case `k = 1`, on the cylinder: if `D_S` is
asymptotic to nondegenerate loops `S±` of symmetric matrices and `1 < p < ∞`, then
`D_S : W^{1,p}(ℝ × S¹, ℝ²ⁿ) → L^p(ℝ × S¹, ℝ²ⁿ)` is Fredholm. -/
theorem isFredholm (n : ℕ) (p : ℝ≥0∞) [Fact (1 ≤ p)] (hp : 1 < p) (hp' : p ≠ ⊤)
    (Splus Sminus : ℝ → Mat n) (hSplus : IsSymLoop Splus) (hSminus : IsSymLoop Sminus)
    (S : ℝ × ℝ → Mat n) (hS : IsAsymptoticTo S Splus Sminus) (hplus : IsNondegenerate Splus) (hminus : IsNondegenerate Sminus) :
    IsFredholmCR p S := by
  sorry

end CauchyRiemannIndex

Source

C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Lecture 4, Theorem 4.3, p. 69 (case k = 1, cylinder)

Read-back

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

Read-back: `CauchyRiemannIndex.isFredholm`

Setting. $n\in\mathbb N$ ; $p\in[1,\infty]$ (instance Fact (1 ≤ p)); loops $S^\pm:\mathbb R\to\mathbb R^{2n\times2n}$ ; coefficient $S:\mathbb R\times\mathbb R\to\mathbb R^{2n\times2n}$ . Matrices are indexed by Fin n ⊕ Fin n; $J_0=$ Matrix.J $=\begin{pmatrix}0&-I\\ I&0\end{pmatrix}$ (checked in Mathlib: fromBlocks 0 (-1) 1 0), i.e. multiplication by $i$ under $(x,y)\mapsto x+iy$ .

Hypotheses. $1<p<\infty$ . $S^\pm$ are continuous, 1-periodic, pointwise symmetric (IsSymLoop). $S$ is continuous, 1-periodic in $t$ , and $S(s,t)\to S^\pm(t)$ entrywise uniformly in $t$ as $s\to\pm\infty$ (IsAsymptoticTo). $S^\pm$ are nondegenerate: for (every, equivalently the unique) fundamental solution $\Psi^\pm$ , $\Psi'=J_0S^\pm\Psi$ , $\Psi(0)=I$ , one has $\det(I-\Psi^\pm(1))\neq0$ .

Definitions used.

cylMeasure = Lebesgue on the strip $\mathbb R\times[0,1)$ ; LpCyl n p $=L^p(\text{strip};\mathbb R^{2n})$ .
W1p p n = closure in $L^p\times L^p\times L^p$ (product norm) of the span of triples $(u,\partial_su,\partial_tu)$ with $u$ smooth, 1-periodic in $t$ , vanishing for $|s|>R$ . This is $W^{1,p}(\mathbb R\times S^1;\mathbb R^{2n})$ as a graph space; second/third components are the weak derivatives.
crApply S (u,v,w)(x) $=v(x)+J_0w(x)+S(x)u(x)$ (a.e. representatives).
crKernel p S = span of $\{w\in W^{1,p}: D_Sw=0\text{ a.e. on strip}\}$ (already a subspace).
crRange p S = span of $\{f\in L^p:\exists w\in W^{1,p},\ f=D_Sw\text{ a.e.}\}$ .
IsFredholmCR p S $:=\dim_{\mathbb R}\ker<\infty\ \wedge$ range closed in $L^p$ $\wedge\ \dim_{\mathbb R}L^p/\operatorname{range}<\infty$ .

Conclusion. $D_S=\partial_s+J_0\partial_t+S(s,t):W^{1,p}(\mathbb R\times S^1,\mathbb R^{2n})\to L^p(\mathbb R\times S^1,\mathbb R^{2n})$ has finite-dimensional kernel, closed range and finite-dimensional cokernel.

Degenerate cases. $n=0$ : all spaces are $0$ ; trivially Fredholm. $S$ independent of $s$ (then $S=S^+=S^-$ forced by IsAsymptoticTo): $D_S$ is invertible by nondegeneracy, consistent.

Remarks. $S$ is not required symmetric for finite $s$ , as in Wendl (only the asymptotes are). $S$ continuous + asymptotically convergent + periodic implies $S$ bounded, so $D_Sw\in L^p$ for $w\in W^{1,p}$ and the range set is the genuine image. The redundant Fact (1 ≤ p) is implied by hp.

Soundness checks.

Junk values / coercions / scope.
- $L^p$ elements are evaluated through their a.e. representatives; all equalities are =ᵐ[cylMeasure], so the arbitrary values off the strip are irrelevant.
- IsNondegenerate quantifies over all fundamental solutions; for continuous $S^\pm$ one exists and is unique (linear ODE), so it is not vacuous.
- Kernel and cokernel dimensions are real dimensions (FiniteDimensional ℝ).
- toEuclideanLin M v = M *ᵥ v, standard.
- All quantifiers are universal over the data; no existential misplacement.
Hypotheses are satisfiable (e.g. $n=1$ , $S=c(s)I$ with $c\to\pm\varepsilon$ , $0<\varepsilon<2\pi$ ; then $\Psi^\pm(1)=$ rotation by $\pm\varepsilon$ , nondegenerate). Not vacuous, not trivially true. In that example the kernel is $\{e^{-\int_0^sc}\,v:v\in\mathbb R^2\}$ (2-dimensional, smooth, exponentially decaying, in the closure), cokernel $0$ ; Fredholm as claimed. The statement is Wendl Thm 4.3 ( $k=1$ ) on the cylinder and is true.

Verdict: no mis-formalization observed

Human review

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

View graph

Cauchy–Riemann operators on the cylinder with nondegenerate asymptotics are Fredholm

Read-back: CauchyRiemannIndex.isFredholm

Read-back: `CauchyRiemannIndex.isFredholm`