Kernel and cokernel of Cauchy–Riemann operators with a large antilinear zeroth-order term

Proved

CauchyRiemannIndex.large_antilinear_perturbation_index

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

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

Let $n=1$ , let $S^\pm$ be continuous loops of symmetric $2\times2$ matrices with nondegenerate asymptotic operators, and let $S:\mathbb{R}\times S^1\to\mathbb{R}^{2\times2}$ be continuous with $S(s,\cdot)\to S^\pm$ uniformly as $s\to\pm\infty$ . Let $\beta:\mathbb{R}\times S^1\to\mathbb{C}$ be smooth with bounded first derivative, such that $|\beta|$ and $1/|\beta|$ are bounded for large $|s|$ , and such that its zeros form finite sets $Z^+$ (positive zeros) and $Z^-$ (negative zeros) with the following normal form: for some $r>0$ and every $\zeta\in Z^\pm$ , on the disc $|z|<r$ around $\zeta$ one has $S=0$ and

\beta(\zeta+z)=z\ \ (\zeta\in Z^+),\qquad\beta(\zeta+z)=\bar z\ \ (\zeta\in Z^-).

For $\sigma>0$ let $D_\sigma\eta=\partial_s\eta+J_0\partial_t\eta+S\eta+\sigma\beta\bar\eta$ , acting from $W^{1,2}$ to $L^2$ . Then:

if $Z^-=\emptyset$ , then for all sufficiently large $\sigma$ , $D_\sigma$ is surjective and $\dim\ker D_\sigma=\#Z^+$ ;
if $Z^+=\emptyset$ , then for all sufficiently large $\sigma$ , $D_\sigma$ is injective and $\dim\operatorname{coker}D_\sigma=\#Z^-$ .

In either case $\operatorname{ind}D_\sigma=\#Z^+-\#Z^-$ for all sufficiently large $\sigma$ .

Formalization Note $\mathbb{C}=\mathbb{R}^2$ via $(x,y)\mapsto x+iy$ , and $\eta\mapsto\beta\bar\eta$ is the matrix antilinearMat β, so $D_\sigma$ is $D_{S_\sigma}$ with $S_\sigma=S+\sigma\cdot$ antilinearMat ∘ β. Points of the cylinder are pairs $(s,t)$ and $\zeta+z$ means $(\zeta_s+\operatorname{Re}z,\zeta_t+\operatorname{Im}z)$ ; $\beta$ is $1$ -periodic in $t$ , the zeros are listed in $\mathbb{R}\times[0,1)$ , and every zero of $\beta$ is a $t$ -translate by an integer of a listed one. Wendl's § 5.5 asks, near each zero, for a holomorphic chart onto the unit disc in which $d\mathrm{vol}$ is standard, the operator is $\bar\partial$ and $\beta$ is $z$ or $\bar z$ ; here the chart is a translation of the coordinates $(s,t)$ , the trivialization is the global one, and the area form is $ds\,dt$ . Replacing the unit disc by a disc of radius $r$ rescales $\beta$ in the chart by $r^2$ , which only reparametrizes $\sigma$ , and kernels and cokernels do not depend on the area form. The exponent is $p=2$ (Wendl, Assumption 5.7). The conclusions are stated with crRange 2 … = ⊤, crKernel 2 … = ⊥ and finrank of crKernel 2 … and of LpCyl 1 2 ⧸ crRange 2 …, together with their finite-dimensionality.

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, Proposition 5.27 (p. 102), with the assumptions of § 5.5 (p. 94), on the cylinder with the
trivial line bundle and `p = 2`: let `D_S` (`n = 1`) be asymptotic to nondegenerate loops `S±` of
symmetric matrices, and let `β : ℝ × S¹ → ℂ` be smooth with bounded derivative, with `|β|` and `1/|β|`
bounded for large `|s|`, whose zeros (mod `t ↦ t + 1`) are the finite sets `Z⁺` (positive zeros) and
`Z⁻` (negative zeros), such that on a disc of radius `r` around each zero `ζ` the operator is `∂̄`
(`S = 0`) and `β(ζ + z) = z` for `ζ ∈ Z⁺`, `β(ζ + z) = z̄` for `ζ ∈ Z⁻`. Put
`D_σ η = D_S η + σ β η̄`. If `Z⁻ = ∅`, then for all large `σ`, `D_σ : W^{1,2} → L²` is surjective with
`dim ker D_σ = #Z⁺`; if `Z⁺ = ∅`, then for all large `σ`, `D_σ` is injective with
`dim coker D_σ = #Z⁻`. -/
theorem large_antilinear_perturbation_index (Splus Sminus : ℝ → Mat 1) (hSplus : IsSymLoop Splus)
    (hSminus : IsSymLoop Sminus) (hplus : IsNondegenerate Splus) (hminus : IsNondegenerate Sminus)
    (S : ℝ × ℝ → Mat 1) (hS : IsAsymptoticTo S Splus Sminus)
    (β : ℝ × ℝ → ℂ) (hβ : ContDiff ℝ ∞ β) (hβper : ∀ s t, β (s, t + 1) = β (s, t))
    (hβC1 : ∃ C : ℝ, ∀ x, ‖fderiv ℝ β x‖ ≤ C)
    (hβends : ∃ (R c : ℝ), 0 < c ∧ ∀ s t, R ≤ |s| → c ≤ ‖β (s, t)‖ ∧ ‖β (s, t)‖ ≤ 1 / c)
    (Zplus Zminus : Finset (ℝ × ℝ)) (hZ : ∀ ζ ∈ Zplus ∪ Zminus, 0 ≤ ζ.2 ∧ ζ.2 < 1)
    (hdisj : Disjoint Zplus Zminus)
    (hzero : ∀ x : ℝ × ℝ, β x = 0 ↔ ∃ ζ ∈ Zplus ∪ Zminus, ∃ m : ℤ, x = (ζ.1, ζ.2 + m))
    (r : ℝ) (hr : 0 < r)
    (hplusZ : ∀ ζ ∈ Zplus, ∀ z : ℂ, ‖z‖ < r →
      β (ζ.1 + z.re, ζ.2 + z.im) = z ∧ S (ζ.1 + z.re, ζ.2 + z.im) = 0)
    (hminusZ : ∀ ζ ∈ Zminus, ∀ z : ℂ, ‖z‖ < r →
      β (ζ.1 + z.re, ζ.2 + z.im) = (starRingEnd ℂ) z ∧ S (ζ.1 + z.re, ζ.2 + z.im) = 0) :
    (Zminus = ∅ → ∃ σ₀ : ℝ, ∀ σ ≥ σ₀,
      crRange 2 (fun x => S x + σ • antilinearMat (β x)) = ⊤ ∧
      FiniteDimensional ℝ (crKernel 2 (fun x => S x + σ • antilinearMat (β x))) ∧
      Module.finrank ℝ (crKernel 2 (fun x => S x + σ • antilinearMat (β x))) = Zplus.card) ∧
    (Zplus = ∅ → ∃ σ₀ : ℝ, ∀ σ ≥ σ₀,
      crKernel 2 (fun x => S x + σ • antilinearMat (β x)) = ⊥ ∧
      FiniteDimensional ℝ (LpCyl 1 2 ⧸ crRange 2 (fun x => S x + σ • antilinearMat (β x))) ∧
      Module.finrank ℝ (LpCyl 1 2 ⧸ crRange 2 (fun x => S x + σ • antilinearMat (β x))) =
        Zminus.card) := by
  sorry

end CauchyRiemannIndex

Source

C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Lecture 5, Proposition 5.27, p. 102, with the assumptions of § 5.5, p. 94 (cylinder, trivial line bundle, p = 2)

Read-back

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

Read-back: `CauchyRiemannIndex.large_antilinear_perturbation_index`

Setting. $n=1$ , $p=2$ ; loops $S^\pm:\mathbb R\to\mathbb R^{2\times2}$ ; $S:\mathbb R\times\mathbb R\to\mathbb R^{2\times2}$ ; $\beta:\mathbb R\times\mathbb R\to\mathbb C$ ; finite sets $Z^+,Z^-\subset\mathbb R\times\mathbb R$ ; $r\in\mathbb R$ .

Hypotheses. $S^\pm$ continuous 1-periodic symmetric loops, nondegenerate; $S$ continuous, $t$ -periodic, asymptotic to $S^\pm$ (entrywise, uniformly in $t$ ). $\beta$ is $C^\infty$ , 1-periodic in $t$ , $\sup_x\|d\beta(x)\|<\infty$ , and $\exists R,\,c>0$ with $c\le|\beta(s,t)|\le 1/c$ for $|s|\ge R$ . Every $\zeta\in Z^+\cup Z^-$ has $\zeta_2\in[0,1)$ ; $Z^+\cap Z^-=\emptyset$ ; $\beta(x)=0\iff x=(\zeta_1,\zeta_2+m)$ for some $\zeta\in Z^+\cup Z^-$ , $m\in\mathbb Z$ . For some $r>0$ and all $|z|<r$ (writing $z=a+ib\mapsto(\zeta_1+a,\zeta_2+b)$ ): $\beta(\zeta+z)=z$ , $S(\zeta+z)=0$ for $\zeta\in Z^+$ ; $\beta(\zeta+z)=\bar z$ , $S(\zeta+z)=0$ for $\zeta\in Z^-$ .

Definitions used. crKernel, crRange (real spans of $\ker$ / image of $D=\partial_s+J_0\partial_t+(\cdot)$ on $W^{1,2}\to L^2$ of $\mathbb R\times S^1$ ), antilinearMat $\beta=\begin{pmatrix}\operatorname{Re}\beta&\operatorname{Im}\beta\\\operatorname{Im}\beta&-\operatorname{Re}\beta\end{pmatrix}$ . Check: for $z=x+iy$ , $\beta\bar z=(ax+by)+i(bx-ay)$ ( $\beta=a+ib$ ), which is exactly that matrix applied to $(x,y)$ ; $J_0=$ Matrix.J $=\begin{pmatrix}0&-1\\1&0\end{pmatrix}$ is multiplication by $i$ . So with $D_\sigma:=$ coefficient $S+\sigma\,$ antilinearMat $(\beta)$ ,

D_\sigma\eta=\partial_s\eta+i\partial_t\eta+S\eta+\sigma\beta\bar\eta=2\bar\partial\eta+S\eta+\sigma\beta\bar\eta\quad(w=s+it).

Conclusion. (i) If $Z^-=\emptyset$ : $\exists\sigma_0\ \forall\sigma\ge\sigma_0$ , $D_\sigma$ is onto $L^2$ , $\ker D_\sigma$ is finite-dimensional and $\dim_{\mathbb R}\ker D_\sigma=\#Z^+$ . (ii) If $Z^+=\emptyset$ : $\exists\sigma_0\ \forall\sigma\ge\sigma_0$ , $\ker D_\sigma=0$ , $\operatorname{coker}D_\sigma$ is finite-dimensional and $\dim_{\mathbb R}\operatorname{coker}D_\sigma=\#Z^-$ .

Remarks.

Local model check. Near $\zeta\in Z^+$ ( $S=0$ , $\beta=z$ ): $2\bar\partial\eta+\sigma z\bar\eta=0$ ; $\eta=e^{-\sigma|z|^2/2}$ gives $2\bar\partial\eta=-\sigma z\eta$ , so it solves the equation exactly for real $\eta$ -values ( $i e^{-\sigma|z|^2/2}$ does not): one real Gaussian per positive zero, matching real finrank $=\#Z^+$ . Near $\zeta\in Z^-$ ( $\beta=\bar z$ ): the $L^2$ -real adjoint of $\eta\mapsto\beta\bar\eta$ is itself and of $2\bar\partial$ is $-2\partial$ ; $-2\partial\xi+\sigma\bar z\bar\xi=0$ is solved by $\xi=i\,e^{-\sigma|z|^2/2}$ : one real cokernel Gaussian per negative zero. Orientation: $z=(s-\zeta_1)+i(t-\zeta_2)$ is the coordinate in which $\partial_s+J_0\partial_t=2\bar\partial$ , so " $\beta=z$ " is a positive (degree $+1$ ) zero. Signs and real dimensions consistent.
Consistency with the index: signed zero count $\#Z^+-\#Z^-=\mathrm{wind}\,\beta(+\infty,\cdot)-\mathrm{wind}\,\beta(-\infty,\cdot)$ (boundary of $[a,b]\times S^1$ for $ds\wedge dt$ is $\{b\}\times S^1-\{a\}\times S^1$ , $t$ increasing), matching index_eq_winding_of_antilinear_deformation.
The Lean hypotheses do not require $\beta$ to converge as $s\to\pm\infty$ (only $c\le|\beta|\le1/c$ and $\|d\beta\|$ bounded there). This is weaker than an "asymptotic to $\beta^\pm$ " assumption, but the conclusion still follows from the coercive estimate above, which uses exactly these bounds (plus boundedness of $S$ , implied by IsAsymptoticTo). No Fredholm assumption on $D_\sigma$ is needed since the conclusion states finite-dimensionality explicitly.
Normal form vs periodicity. If $r>1/2$ then $z=ia$ and $z=i(a-1)$ with $1-r<a<r$ both lie in the disc and give $\beta(\zeta_1,\zeta_2+a)=ia\ne i(a-1)=\beta(\zeta_1,\zeta_2+a-1)$ , contradicting $t$ -periodicity; so the hypotheses force $r\le1/2$ . Two discs (around $\zeta\ne\zeta'$ , or around $\zeta$ and an integer translate) cannot meet: at a common point $w$ , $w-\zeta=\beta(w)=w-\zeta'$ (or $\overline{w-\zeta}=\overline{w-\zeta'}$ for two negative zeros, again forcing $\zeta=\zeta'$ ). For one positive and one negative zero a single common point is possible, but the overlap of two open discs is open, and on it $\beta$ would be both $w\mapsto w-\zeta$ and $w\mapsto\overline{w-\zeta'}$ , i.e. $\partial\beta=1$ and $\partial\beta=0$ at once, impossible. Hence the hypotheses force the discs to be pairwise disjoint mod 1. These are consequences, not contradictions: $r$ is a hypothesis parameter, and a small $r$ is always available for a genuine example.

Soundness checks.

Junk/coercions: finrank used only alongside an explicit FiniteDimensional, so no junk 0; Zplus.card is ℕ, compared in ℕ. σ • antilinearMat (β x) is real scalar on Mat 1; S x + … pointwise. starRingEnd ℂ z is $\bar z$ . ‖fderiv ℝ β x‖ is the operator norm. Quantifier order: $\exists\sigma_0\,\forall\sigma\ge\sigma_0$ inside each implication, after all data are fixed; correct. Binder scope of ∀ z, ‖z‖ < r → β … ∧ S … = 0 covers both conjuncts as intended. hZ normalizes representatives to $t\in[0,1)$ , so card counts zeros mod 1 without duplicates.
Satisfiable, not vacuous: $Z^+=\{(s_0,0)\}$ , $Z^-=\emptyset$ : take $\beta_0(s,t)=\big(a(s)e^{2\pi it}-(1-a(s))\big)/\pi$ with smooth monotone $a$ , $a\to0$ at $-\infty$ , $a\to1$ at $+\infty$ , $a(s_0)=1/2$ , $a'(s_0)=\pi/2$ : its only zeros are $(s_0,m)$ and its Jacobian there is the identity, so $\beta_0(\zeta+z)=z+O(|z|^2)$ . Put $\beta=\chi z+(1-\chi)\beta_0$ with a cutoff $\chi(|z|)$ equal to 1 on $|z|<r$ and 0 on $|z|>2r$ (extended periodically): for small $r$ the two terms differ by $O(|z|^2)\ll|z|$ on the annulus, so no new zeros, and $\beta(\zeta+z)=z$ exactly on the disc; $|\beta|\to1$ at both ends, $d\beta$ bounded, smooth, periodic. Take $S=\chi_{\text{ends}}(s)\cdot S^\pm$ with $S^\pm=\pm\varepsilon I$ ( $0<\varepsilon<\pi$ , nondegenerate) and $\chi_{\text{ends}}=0$ on $|s|\le|s_0|+1$ , so $S=0$ on the disc. All hypotheses hold; conclusion (i) predicts a one-dimensional real kernel (the Gaussian) and surjectivity: consistent with index $=1=\mathrm{wind}(+)-\mathrm{wind}(-)$ . (Here $D_S$ itself has index $\mu(\varepsilon I)-\mu(-\varepsilon I)=2$ ; no contradiction, since $\sigma\beta\bar\eta$ does not decay at the ends, so $D_\sigma$ has different asymptotic operators than $D_S$ .) True (Wendl Prop. 5.27, under hypotheses at least as strong as needed for its proof).

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

Kernel and cokernel of Cauchy–Riemann operators with a large antilinear zeroth-order term

Read-back: CauchyRiemannIndex.large_antilinear_perturbation_index

Read-back: `CauchyRiemannIndex.large_antilinear_perturbation_index`