Cauchy–Riemann operators with nondegenerate asymptotics are semi-Fredholm

Proved

CauchyRiemannIndex.semiFredholm

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}\to L^p$ has finite-dimensional kernel and closed range.

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$ .

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, Corollary 4.14 (p. 74), case `k = 1`: if `D_S` is asymptotic to nondegenerate loops
`S±` of symmetric matrices and `1 < p < ∞`, then `D_S : W^{1,p} → L^p` is semi-Fredholm: its
kernel is finite-dimensional and its range is closed. -/
theorem semiFredholm (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) :
    FiniteDimensional ℝ (crKernel p S) ∧ IsClosed (crRange p S : Set (LpCyl n p)) := by
  sorry

end CauchyRiemannIndex

Source

C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Lecture 4, Corollary 4.14, p. 74 (case k = 1)

Read-back

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

Read-back: `CauchyRiemannIndex.semiFredholm`

Setting. $n$ ; $p\in[1,\infty]$ ; loops $S^\pm$ ; a coefficient $S$ .

Hypotheses. $1<p<\infty$ . $S^\pm$ are symmetric loops. IsAsymptoticTo S S⁺ S⁻. $S^+$ and $S^-$ are nondegenerate.

Definitions used. crKernel p S $=\{w\in W^{1,p}:D_Sw=0\}$ , a submodule of $(L^p)^3$ . crRange p S $=D_S(W^{1,p})\subseteq L^p$ . Both spans are redundant, since the sets are already subspaces. See the Setting.

Conclusion.

\dim_{\mathbb R}\ker\big(D_S:W^{1,p}\to L^p\big)<\infty\quad\text{and}\quad D_S(W^{1,p})\text{ is closed in }L^p(\mathbb R\times S^1,\mathbb R^{2n}).

Degenerate cases. For $n=0$ it is trivial. $S$ is bounded (continuous, periodic, asymptotic), so $D_S$ is bounded $W^{1,p}\to L^p$ , and every $w\in W^{1,p}$ contributes to the range.

Remarks. FiniteDimensional ℝ (crKernel p S) uses the subtype module structure. The kernel lives in triples, but since $w\mapsto w_1$ is injective on $W^{1,p}$ , it is isomorphic to the kernel of $D_S$ on $W^{1,p}$ .

Soundness checks.

IsClosed is taken on the coerced set in LpCyl n p with its $L^p$ topology, which is correct. There are no junk values. There are no quantifiers beyond the hypotheses.
Not vacuous: e.g. $S(s,t)=S_\infty(t)$ nondegenerate. It is true, as the semi-Fredholm property of a CR operator with nondegenerate asymptotics. It follows from the global estimate and the compact restriction, via the abstract lemma. Without nondegeneracy the range is not closed, and the hypotheses are exactly the needed ones.

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 with nondegenerate asymptotics are semi-Fredholm

Read-back: CauchyRiemannIndex.semiFredholm

Read-back: `CauchyRiemannIndex.semiFredholm`