Translation-invariant Cauchy–Riemann operators with nondegenerate asymptotics are isomorphisms

Proved

CauchyRiemannIndex.translationInvariant_bijective

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

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

Let $1<p<\infty$ and let $S_\infty$ be a continuous loop of symmetric matrices whose asymptotic operator $-J_0\partial_t-S_\infty(t)$ is nondegenerate. Then

\partial_s+J_0\partial_t+S_\infty(t):W^{1,p}(\mathbb{R}\times S^1,\mathbb{R}^{2n})\to L^p(\mathbb{R}\times S^1,\mathbb{R}^{2n})

is an isomorphism.

Formalization Note The operator is $D_S$ with $S(s,t)=S_\infty(t)$ . The conclusion is crKernel p S = ⊥ ∧ crRange p S = ⊤, i.e. bijectivity, which for a bounded operator between Banach spaces is the same as being an isomorphism. $p$ is in ℝ≥0∞ with Fact (1 ≤ p), $1<p$ , $p\ne\infty$ .

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.11 (p. 71), case `k = 1`: for `1 < p < ∞` and a nondegenerate loop `S∞`
of symmetric matrices, the translation-invariant operator
`∂ₛ + J₀ ∂ₜ + S∞(t) : W^{1,p}(ℝ × S¹, ℝ²ⁿ) → L^p(ℝ × S¹, ℝ²ⁿ)` is an isomorphism: it is
injective and onto. -/
theorem translationInvariant_bijective (n : ℕ) (p : ℝ≥0∞) [Fact (1 ≤ p)] (hp : 1 < p)
    (hp' : p ≠ ⊤) (Sinf : ℝ → Mat n) (hS : IsSymLoop Sinf) (hnd : IsNondegenerate Sinf) :
    crKernel p (fun x : ℝ × ℝ => Sinf x.2) = ⊥ ∧ crRange p (fun x : ℝ × ℝ => Sinf x.2) = ⊤ := 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.11, p. 71 (case k = 1)

Read-back

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

Read-back: `CauchyRiemannIndex.translationInvariant_bijective`

Setting. $n\in\mathbb N$ , $p\in[1,\infty]$ (Fact (1 ≤ p)), a loop $S_\infty:\mathbb R\to\mathrm{Mat}_{2n}(\mathbb R)$ .

Hypotheses.

$1<p$ and $p\ne\infty$ .
IsSymLoop S∞: $S_\infty$ is continuous, 1-periodic and symmetric.
IsNondegenerate S∞: $\det(1-\Psi(1))\ne0$ for the fundamental solution $\Psi'=J_0S_\infty\Psi$ , $\Psi(0)=I$ .

Definitions used. The operator is $D(u)=\partial_su+J_0\partial_tu+S_\infty(t)u$ , i.e. the coefficient is $S(s,t)=S_\infty(t)$ . It is applied to $W^{1,p}(\mathbb R\times S^1,\mathbb R^{2n})=\overline{\mathrm{span}}\{(u,\partial_su,\partial_tu):u\in C_c^\infty\}$ , embedded in $(L^p)^3$ . crKernel and crRange are the kernel (in triples) and the range (in $L^p$ ) of $D$ . See the Setting read-back.

Conclusion.

\ker\big(D:W^{1,p}\to L^p\big)=\{0\}\quad\text{and}\quad D(W^{1,p})=L^p(\mathbb R\times S^1,\mathbb R^{2n}).

That is, $\partial_s+J_0\partial_t+S_\infty$ is bijective $W^{1,p}\to L^p$ . Bounded invertibility then follows by the open mapping theorem.

Degenerate cases. For $n=0$ all spaces are $0$ and the statement is trivial. $S_\infty$ is bounded, so $D$ maps $W^{1,p}$ into $L^p$ .

Remarks. Nondegeneracy cannot be dropped. If $\Psi(1)\eta_0=\eta_0$ , then $(s,t)\mapsto\Psi(t)\eta_0$ is $s$ -independent. It is not in $L^p$ , but cut-offs of it show that the range is not closed, so surjectivity fails. Nondegeneracy is therefore a genuine hypothesis.

Soundness checks.

⊥ is the zero submodule of Triple, and ⊤ is all of LpCyl n p. The equalities are of submodules, so there are no coercion issues. $S(x)=S_\infty(x.2)$ correctly takes $t=x.2$ . There are no quantifier-order issues.
Not vacuous: e.g. $S_\infty=\varepsilon I$ with $\varepsilon\notin2\pi\mathbb Z$ is nondegenerate. The statement is the standard isomorphism theorem for translation-invariant CR operators with nondegenerate asymptotics, $1<p<\infty$ . It 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

Translation-invariant Cauchy–Riemann operators with nondegenerate asymptotics are isomorphisms

Read-back: CauchyRiemannIndex.translationInvariant_bijective

Read-back: `CauchyRiemannIndex.translationInvariant_bijective`