Compactness of the restriction from W^{1,p} to L^p of a finite cylinder

Proved

CauchyRiemannIndex.compact_restriction

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

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

Let $1<p<\infty$ and $R\in\mathbb{R}$ . Every sequence of smooth maps on $\mathbb{R}\times S^1$ that vanish for large $|s|$ and are bounded in $W^{1,p}$ has a subsequence that is Cauchy in $L^p([-R,R]\times S^1)$ .

Formalization Note $p$ is in ℝ≥0∞. The sequence consists of test sections $u_k$ with w1pNorm p (u k) ≤ 1; the conclusion gives a strictly increasing $\varphi:\mathbb{N}\to\mathbb{N}$ such that $\|u_{\varphi(i)}-u_{\varphi(j)}\|_{L^p([-R,R]\times[0,1))}\to0$ , written with $\varepsilon\in$ ℝ≥0∞.

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, p. 74 (the compact inclusion `W^{1,p}(Σ_R) ↪ L^p(Σ_R)` used after Lemma 4.13), on
`Σ_R = [-R, R] × S¹`: for `1 < p < ∞`, every sequence of test sections bounded in `W^{1,p}`
has a subsequence that is Cauchy in `L^p([-R, R] × S¹)`. -/
theorem compact_restriction (n : ℕ) (p : ℝ≥0∞) (hp : 1 < p) (hp' : p ≠ ⊤) (R : ℝ)
    (u : ℕ → ℝ × ℝ → Vec n) (hu : ∀ k, IsTestSection (u k)) (hb : ∀ k, w1pNorm p (u k) ≤ 1) :
    ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ ε : ℝ≥0∞, 0 < ε → ∃ N, ∀ i ≥ N, ∀ j ≥ N,
      eLpNorm (u (φ i) - u (φ j)) 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, p. 74 (the compact inclusion used after Lemma 4.13)

Read-back

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

Read-back: `CauchyRiemannIndex.compact_restriction`

Setting. $n$ ; $p\in\mathbb R_{\ge0}^\infty$ ; $R\in\mathbb R$ ; a sequence $u_k$ of maps $\mathbb R^2\to\mathbb R^{2n}$ .

Hypotheses. $1<p<\infty$ . Each $u_k$ is a test section (smooth, 1-periodic in $t$ , compact $s$ -support). $\|u_k\|_{W^{1,p}(\mathbb R\times S^1)}\le1$ for all $k$ , using w1pNorm, the sum of the three $L^p$ norms on the strip.

Definitions used. w1pNorm. eLpNorm w.r.t. $\lambda$ on $[-R,R]\times[0,1)$ .

Conclusion.

\exists\varphi:\mathbb N\to\mathbb N\text{ strictly increasing}:\ \forall\varepsilon>0\ \exists N\ \forall i,j\ge N:\ \|u_{\varphi(i)}-u_{\varphi(j)}\|_{L^p([-R,R]\times S^1)}<\varepsilon.

That is, there is a subsequence that is Cauchy in $L^p(\Sigma_R)$ .

Degenerate cases. For $R<0$ the set is empty and the statement is trivial. $\varepsilon=\top$ is allowed, and is then trivial.

Remarks. This is the Rellich–Kondrachov compactness $W^{1,p}(\Sigma_R)\hookrightarrow L^p(\Sigma_R)$ , stated sequentially for smooth sections. Here $\Sigma_R=[-R,R]\times S^1$ is compact with a Lipschitz boundary. $1<p$ is more than needed ( $p\ge1$ suffices).

Soundness checks.

$u_{\varphi(i)}-u_{\varphi(j)}$ is the pointwise difference of functions. Each norm is finite. $\varepsilon:\mathbb R_{\ge0}^\infty$ with $0<\varepsilon$ is the correct Cauchy formulation. Quantifier order: $\varphi$ first, then $\forall\varepsilon\,\exists N$ , which is genuine Cauchyness, uniform in $i,j\ge N$ .
Not vacuous. It is true by Rellich on $[-R,R]\times S^1$ (e.g. via Fréchet–Kolmogorov: the $W^{1,p}$ bound gives uniform $L^p$ -equicontinuity of translates).

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

Compactness of the restriction from W^{1,p} to L^p of a finite cylinder

Read-back: CauchyRiemannIndex.compact_restriction

Read-back: `CauchyRiemannIndex.compact_restriction`