The elliptic estimate on cylindrical ends with nondegenerate asymptotics

Proved

CauchyRiemannIndex.asymptotic_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)$ . If $A^+=-J_0\partial_t-S^+$ is nondegenerate, there are $R$ and $c$ such that

\|\eta\|_{W^{1,p}}\le c\,\|D_S\eta\|_{L^p}

for every smooth $\eta$ that vanishes for $s\le R$ . Likewise, if $A^-$ is nondegenerate, there are $R$ and $c$ such that the same estimate holds for every $\eta$ that vanishes for $s\ge-R$ .

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

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 4.9 (p. 71), case `k = 1`: let `D_S` be asymptotic to loops `S±` of
symmetric matrices and `1 < p < ∞`. If `S⁺` is nondegenerate, there are `R` and `c` with
`‖η‖_{W^{1,p}} ≤ c ‖D_S η‖_{L^p}` for every test section `η` vanishing for `s ≤ R`; likewise at
the negative end when `S⁻` is nondegenerate, for `η` vanishing for `s ≥ -R`. -/
theorem asymptotic_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) :
    (IsNondegenerate Splus → ∃ (R : ℝ) (c : ℝ≥0), ∀ u : ℝ × ℝ → Vec n, IsTestSection u →
      (∀ s t, s ≤ R → u (s, t) = 0) → w1pNorm p u ≤ c * eLpNorm (crOp S u) p cylMeasure) ∧
    (IsNondegenerate Sminus → ∃ (R : ℝ) (c : ℝ≥0), ∀ u : ℝ × ℝ → Vec n, IsTestSection u →
      (∀ s t, -R ≤ s → u (s, t) = 0) → w1pNorm p u ≤ c * eLpNorm (crOp S u) p cylMeasure) := by
  sorry

end CauchyRiemannIndex

Source

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

Read-back

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

Read-back: `CauchyRiemannIndex.asymptotic_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⁻: $S$ is continuous and $t$ -periodic, and $S(s,\cdot)\to S^\pm$ uniformly as $s\to\pm\infty$ .

Definitions used. w1pNorm, crOp and IsTestSection as in the Setting. IsNondegenerate: $\det(1-\Psi(1))\ne0$ for the fundamental solution of $J_0S^\pm$ .

Conclusion. A conjunction of two implications.

(+) If $S^+$ is nondegenerate, then

\exists R\in\mathbb R,\ c\ge0\ \forall u\text{ test},\ \big(u=0\text{ on }\{s\le R\}\big)\Rightarrow \|u\|_{W^{1,p}}\le c\,\|D_Su\|_{L^p}.

(−) If $S^-$ is nondegenerate, the same holds with $u=0$ on $\{s\ge -R\}$ .

Degenerate cases. $R$ is existential and can be taken large, so this concerns sections supported far out in one end. For $n=0$ it is trivial.

Remarks.

There is no $\|u\|_{L^p}$ term on the right, which is the correct, stronger form.
Each half uses only the nondegeneracy of its own end.
The IsSymLoop hypothesis on the other end is unused but harmless.

Soundness checks.

Quantifier order is $\exists R\,c$ before $\forall u$ , giving a uniform constant. All norms are finite because $u$ is smooth with compact support. There is no ℝ≥0∞ junk. The implications are scoped inside each conjunct, as intended.
Not vacuous: nondegenerate symmetric loops exist. It is true: for $u$ supported in $\{s>R\}$ , $\|u\|\le c_0\|D_{S^+}u\|\le c_0\|D_Su\|+c_0\sup_{s\ge R}|S-S^+|\,\|u\|_p$ , by the translation-invariant isomorphism. One then absorbs the last term for $R$ large. Without nondegeneracy this fails, which is why the implication is needed.

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 elliptic estimate on cylindrical ends with nondegenerate asymptotics

Read-back: CauchyRiemannIndex.asymptotic_estimate

Read-back: `CauchyRiemannIndex.asymptotic_estimate`