The local elliptic estimate for Cauchy–Riemann operators on a finite cylinder

Proved

CauchyRiemannIndex.local_estimate

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

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

Let $1<p<\infty$ , $R\in\mathbb{R}$ , and let $S:\mathbb{R}\times S^1\to\mathbb{R}^{2n\times2n}$ be continuous. There is a constant $c$ such that

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

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

Formalization Note $p$ is in ℝ≥0∞. $S$ is continuous and $1$ -periodic in $t$ . 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.8 (p. 71), case `k = 1`, on the compact piece `[-R, R] × S¹` of the
cylinder: for `1 < p < ∞` and a continuous `t`-periodic `S` there is `c` with
`‖η‖_{W^{1,p}} ≤ c ‖D_S η‖_{L^p} + c ‖η‖_{L^p}` for every smooth `η`, `1`-periodic in `t`,
that vanishes for `|s| ≥ R`. -/
theorem local_estimate (n : ℕ) (p : ℝ≥0∞) (hp : 1 < p) (hp' : p ≠ ⊤) (R : ℝ)
    (S : ℝ × ℝ → Mat n) (hS : Continuous S) (hper : ∀ s t, S (s, t + 1) = S (s, t)) :
    ∃ 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 + c * eLpNorm 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.8, p. 71 (case k = 1, Σ₀ = [-R, R] × S¹)

Read-back

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

Read-back: `CauchyRiemannIndex.local_estimate`

Setting. $n$ ; $p\in\mathbb R_{\ge0}^\infty$ ; $R\in\mathbb R$ ; a coefficient $S:\mathbb R^2\to\mathrm{Mat}_{2n}$ .

Hypotheses. $1<p$ , $p\ne\infty$ , $S$ continuous, $S(s,t+1)=S(s,t)$ .

Definitions used.

w1pNorm p u $=\|u\|_{L^p}+\|\partial_su\|_{L^p}+\|\partial_tu\|_{L^p}$ on the strip $\mathbb R\times[0,1)$ .
crOp S u $=\partial_su+J_0\partial_tu+Su$ .
IsTestSection: smooth, 1-periodic in $t$ , with compact $s$ -support.

Conclusion.

\exists c\in[0,\infty)\ \forall u\text{ test section with }u(s,t)=0\text{ for }|s|\ge R:\quad \|u\|_{W^{1,p}}\le c\,\|D_Su\|_{L^p}+c\,\|u\|_{L^p}.

The constant $c$ depends on $n,p,R,S$ only.

Degenerate cases. For $R\le0$ only $u=0$ qualifies, and the bound is trivial. For $n=0$ it is trivial.

Remarks. Only the values of $S$ on the compact set $[-R,R]\times[0,1]$ matter. There, $S$ is bounded and uniformly continuous. [Fact (1 ≤ p)] is not needed here, since there are no Lp spaces, only eLpNorm.

Soundness checks.

All quantities are ℝ≥0∞. Since $u$ is smooth with compact support on the strip, every norm is finite, so the inequality is not trivialised by $\top$ . $c:\mathbb R_{\ge0}$ is finite. fderiv is applied to smooth $u$ only. Quantifier order: $c$ is chosen before $u$ , so the bound is uniform over all $u$ supported in $|s|<R$ .
Not vacuous. It is true: this is the local Calderón–Zygmund estimate for $\partial_s+J_0\partial_t$ on $[-R,R]\times S^1$ , with the zeroth-order term $Su$ absorbed into $c\|u\|_p$ .

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 local elliptic estimate for Cauchy–Riemann operators on a finite cylinder

Read-back: CauchyRiemannIndex.local_estimate

Read-back: `CauchyRiemannIndex.local_estimate`