The global estimate for Cauchy–Riemann operators on the cylinder modulo a finite piece

Proved

CauchyRiemannIndex.global_estimate

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 there are $R$ and $c$ such that

\|\eta\|_{W^{1,p}}\le c\,\|D_S\eta\|_{L^p}+c\,\|\eta\|_{L^p([-R,R]\times S^1)}

for every smooth $\eta$ on $\mathbb{R}\times S^1$ that vanishes for large $|s|$ .

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 estimate is stated for test sections $u$ (smooth, $1$ -periodic in $t$ , zero for large $|s|$ ), with $\|u\|_{W^{1,p}}$ = w1pNorm p u $=\|u\|_p+\|\partial_su\|_p+\|\partial_tu\|_p$ in ℝ≥0∞ and $D_Su$ = crOp S u; the constant is in ℝ≥0 and is chosen before $u$ . $\|\eta\|_{L^p([-R,R]\times S^1)}$ is eLpNorm u p (cylMeasure.restrict (Icc (-R) R ×ˢ univ)).

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, Lemma 4.13 (p. 74), case `k = 1`: let `D_S` be asymptotic to nondegenerate loops `S±`
of symmetric matrices and `1 < p < ∞`. There are `R` and `c` with
`‖η‖_{W^{1,p}} ≤ c ‖D_S η‖_{L^p} + c ‖η‖_{L^p([-R, R] × S¹)}` for every test section `η`. -/
theorem global_estimate (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) :
    ∃ (R : ℝ) (c : ℝ≥0), ∀ u : ℝ × ℝ → Vec n, IsTestSection u →
      w1pNorm p u ≤ c * eLpNorm (crOp S u) p cylMeasure +
        c * eLpNorm u p (cylMeasure.restrict (Set.Icc (-R) R ×ˢ Set.univ)) := by
  sorry

end CauchyRiemannIndex

Source

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

Read-back

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

Read-back: `CauchyRiemannIndex.global_estimate`

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⁻. Both $S^+$ and $S^-$ are nondegenerate.

Definitions used. w1pNorm, crOp and IsTestSection as in the Setting. cylMeasure.restrict (Icc (-R) R ×ˢ univ) is Lebesgue measure on $[-R,R]\times[0,1)$ , i.e. $\Sigma_R=[-R,R]\times S^1$ .

Conclusion.

\exists R\in\mathbb R,\ c\ge0\ \forall u\text{ test section}:\quad \|u\|_{W^{1,p}(\mathbb R\times S^1)}\le c\,\|D_Su\|_{L^p(\mathbb R\times S^1)}+c\,\|u\|_{L^p([-R,R]\times S^1)}.

Degenerate cases. For $n=0$ it is trivial. $R$ is existential. A negative $R$ would give an empty set, but the statement then just asks for $\|u\|\le c\|D_Su\|$ (injectivity-type), so the prover will pick $R$ large.

Remarks. This is stated on test sections only, which suffices by density for $W^{1,p}$ . Both ends must be nondegenerate.

Soundness checks.

Restricting a restricted measure: cylMeasure.restrict A $=\lambda|_{(\mathbb R\times[0,1))\cap A}$ , as intended. All norms are finite. The quantifier order is $\exists R\,c$ before $\forall u$ , as intended. The + is between two ℝ≥0∞ terms, with no precedence issue (the * binds tighter).
Not vacuous. It is true: combine the local estimate on $[-R-1,R+1]$ with the two asymptotic estimates, using a partition of unity in $s$ . The cut-off derivative terms are bounded by $\|u\|_{L^p(\Sigma_{R+1})}$ after enlarging $R$ .

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 global estimate for Cauchy–Riemann operators on the cylinder modulo a finite piece

Read-back: CauchyRiemannIndex.global_estimate

Read-back: `CauchyRiemannIndex.global_estimate`