The kernel and the index of a Cauchy–Riemann operator do not depend on p

Proved

CauchyRiemannIndex.index_independent_of_p

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 for every $p_2\in(1,\infty)$ the kernels of $D_S$ on $W^{1,p}$ and on $W^{1,p_2}$ have the same dimension, and the Fredholm indices of $D_S:W^{1,p}\to L^p$ and $D_S:W^{1,p_2}\to L^{p_2}$ are equal.

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$ . The index is crIndex, an integer.

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), second part, case `k = 1`, on the cylinder: if `D_S` is asymptotic
to nondegenerate loops `S±` of symmetric matrices, the kernel dimension and the Fredholm index of
`D_S : W^{1,p} → L^p` do not depend on `p ∈ (1, ∞)`. -/
theorem index_independent_of_p (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)
    (p₂ : ℝ≥0∞) [Fact (1 ≤ p₂)] (hp₂ : 1 < p₂) (hp₂' : p₂ ≠ ⊤) :
    Module.finrank ℝ (crKernel p S) = Module.finrank ℝ (crKernel p₂ S) ∧
      crIndex p S = crIndex 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 (second statement, case k = 1)

Read-back

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

Read-back: `CauchyRiemannIndex.index_independent_of_p`

Setting. As in isFredholm: $n$ , loops $S^\pm$ , coefficient $S$ , and two exponents $p,p_2\in[1,\infty]$ (each with a Fact (1 ≤ ·) instance).

Hypotheses. $1<p<\infty$ , $1<p_2<\infty$ ; $S^\pm$ continuous 1-periodic symmetric loops; $S$ continuous, $t$ -periodic, uniformly asymptotic to $S^\pm$ as $s\to\pm\infty$ ; $S^\pm$ nondegenerate ( $\det(I-\Psi^\pm(1))\ne0$ for the fundamental solution $\Psi'=J_0S^\pm\Psi$ , $\Psi(0)=I$ ).

Definitions used. crKernel p S = $\ker(D_S:W^{1,p}\to L^p)\subseteq L^p\times L^p\times L^p$ (triples $(u,\partial_su,\partial_tu)$ on the strip $\mathbb R\times[0,1)$ ). crIndex p S $=\operatorname{finrank}_{\mathbb R}\ker-\operatorname{finrank}_{\mathbb R}(L^p/\operatorname{range})\in\mathbb Z$ . $D_S=\partial_s+J_0\partial_t+S$ . (See isFredholm.md for the unfolding of $W^{1,p}$ .)

Conclusion.

\dim_{\mathbb R}\ker D_S^{(p)}=\dim_{\mathbb R}\ker D_S^{(p_2)}\quad\text{and}\quad \operatorname{ind}D_S^{(p)}=\operatorname{ind}D_S^{(p_2)} ,

where $D_S^{(q)}:W^{1,q}\to L^q$ .

Degenerate cases. $p=p_2$ : trivial. $n=0$ : both sides $0$ .

Remarks. Module.finrank is $0$ on infinite-dimensional spaces, so the statement is only meaningful because the operators are Fredholm under these hypotheses (isFredholm); with Fredholmness, finrank equals the true dimension and crIndex is the true index. The kernels live in different ambient spaces; only their dimensions are compared, which is the intended content (Wendl Thm 4.3, second part).

Soundness checks.

Junk values: finrank-0 junk only arises off the Fredholm regime, which the hypotheses exclude; ℤ-casts in crIndex are applied before subtraction (no ℕ truncation). Quantifiers: all data universally quantified; $p_2$ arbitrary in $(1,\infty)$ .
Not vacuous (hypotheses satisfiable, see isFredholm.md). In the test case $n=1$ , $S=c(s)I$ , $c\to\pm\varepsilon$ : kernel $=\{e^{-\int_0^s c}v\}$ is in $W^{1,q}$ for every $q$ , dimension 2 for all $q$ ; cokernel $0$ for all $q$ . Consistent. True by elliptic regularity (kernel elements are smooth and exponentially decaying) plus the same for the formal adjoint.

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

The kernel and the index of a Cauchy–Riemann operator do not depend on p

Read-back: CauchyRiemannIndex.index_independent_of_p

Read-back: `CauchyRiemannIndex.index_independent_of_p`