Global regularity of weak L^p solutions of Cauchy–Riemann equations on the cylinder

Proved

CauchyRiemannIndex.memW1p_of_weak_solution

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 $\eta\in L^p$ and $f\in L^p$ satisfy $D_S\eta=f$ weakly, that is,

\int_{\mathbb{R}\times S^1}\langle D_S^*\varphi,\eta\rangle=\int_{\mathbb{R}\times S^1}\langle\varphi,f\rangle\quad\text{for every test section }\varphi,\qquad D_S^*\varphi=-\partial_s\varphi+J_0\partial_t\varphi+S^{\mathsf T}\varphi,

then $\eta\in W^{1,p}$ and $D_S\eta=f$ .

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. The conclusion is ∃ w ∈ W1p p n, w.1 = η ∧ crApply S w =ᵐ f: $\eta$ is the first component of an element of $W^{1,p}$ on which $D_S$ equals $f$ almost everywhere. Integrals are over the strip $\mathbb{R}\times[0,1)$ ; $D_S^*$ is the formal adjoint of $D_S$ for the real $L^2$ pairing.

Preamble

import Definitions.Def_CauchyRiemannIndex_Setting
import Mathlib.Analysis.Calculus.ContDiff.Basic
import Mathlib.MeasureTheory.Integral.Bochner.Basic

Formal statement

namespace CauchyRiemannIndex

open MeasureTheory Matrix Filter Topology
open scoped ENNReal NNReal ContDiff RealInnerProductSpace

/-- Wendl, Proposition 4.6 (p. 70), case `k = 1`: let `D_S` be asymptotic to loops `S±` of
symmetric matrices and `1 < p < ∞`. If `η ∈ L^p` satisfies `D_S η = f` weakly for some
`f ∈ L^p`, i.e. `∫ ⟨D_S^* φ, η⟩ = ∫ ⟨φ, f⟩` for every test section `φ`, where
`D_S^* φ = -∂ₛφ + J₀ ∂ₜφ + S(s, t)ᵀ φ` is the formal adjoint, then `η ∈ W^{1,p}` and
`D_S η = f`. -/
theorem memW1p_of_weak_solution (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) (η f : LpCyl n p)
    (hweak : ∀ φ : ℝ × ℝ → Vec n, IsTestSection φ →
      ∫ x, inner ℝ (-partialS φ x + Matrix.toEuclideanLin (J₀ n) (partialT φ x) +
          Matrix.toEuclideanLin (S x)ᵀ (φ x)) (η x) ∂cylMeasure =
        ∫ x, inner ℝ (φ x) (f x) ∂cylMeasure) :
    ∃ w ∈ W1p p n, w.1 = η ∧ crApply S w =ᵐ[cylMeasure] (f : ℝ × ℝ → Vec n) := 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.6, p. 70 (case k = 1)

Read-back

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

Read-back: `CauchyRiemannIndex.memW1p_of_weak_solution`

Setting. $n$ ; $p\in[1,\infty]$ ; loops $S^\pm$ ; a coefficient $S:\mathbb R^2\to\mathrm{Mat}_{2n}$ ; $\eta,f\in L^p(\mathbb R\times S^1,\mathbb R^{2n})$ .

Hypotheses.

$1<p<\infty$ .
$S^\pm$ are symmetric loops.
IsAsymptoticTo S S⁺ S⁻: $S$ is continuous and $t$ -periodic, with uniform entrywise limits $S^\pm$ .
(weak equation) For every test section $\varphi$ (smooth, 1-periodic in $t$ , compact $s$ -support):

\int_{\mathbb R\times[0,1)}\big\langle-\partial_s\varphi+J_0\partial_t\varphi+S^T\varphi,\ \eta\big\rangle\,ds\,dt=\int_{\mathbb R\times[0,1)}\langle\varphi,f\rangle\,ds\,dt.

Definitions used. W1p and crApply are as in the Setting. The formal $L^2$ adjoint of $D_S=\partial_s+J_0\partial_t+S$ is $-\partial_s+J_0\partial_t+S^T$ , because $(J_0\partial_t)^*=-\partial_t J_0^T=J_0\partial_t$ (using $J_0^T=-J_0$ and periodic integration by parts in $t$ ). So the hypothesis says exactly that $D_S\eta=f$ in the sense of distributions on the cylinder.

Conclusion.

\exists w\in W^{1,p}:\ w_1=\eta\ \text{ in }L^p\quad\text{and}\quad w_2+J_0w_3+Sw_1=f\ \text{ a.e.}

That is, $\eta\in W^{1,p}$ and $D_S\eta=f$ , because $w_2,w_3$ are forced to be $\partial_s\eta,\partial_t\eta$ .

Degenerate cases. For $\varphi=0$ the identity is trivial. For $n=0$ the statement is trivial.

Remarks. Nondegeneracy of $S^\pm$ is not assumed, and it is not needed: this is interior elliptic regularity with constants uniform in the base point, since $S$ is bounded, and summed over unit pieces. The limits $S^\pm$ enter only to make $S$ bounded.

Soundness checks.

Bochner integrals: the left integrand is $\langle\psi,\eta\rangle$ $⟨ ψ, η ⟩$ with $\psi=D_S^*\varphi$ $ψ = D_{S}^{*} φ$ . $\psi$ $ψ$ is continuous and bounded on the strip, with support in $[-R,R]\times[0,1)$ $[- R, R] \times [0, 1)$ , so $\psi\in L^{p'}$ $ψ \in L^{p^{'}}$ and the integrand is integrable. Likewise for $\langle\varphi,f\rangle$ $⟨ φ, f ⟩$ . Both integrals are genuine, with no junk $0$ $0$ .
- Notation: ∫ x, r ∂μ parses its body at precedence 60, so the = (prec 50) is not swallowed. Each side is a separate integral.
- toEuclideanLin (S x)ᵀ (φ x) applies $S(x)^T$ ( $ᵀ$ is postfix max-precedence) to $\varphi(x)$ .
- -partialS φ x is $-(\partial_s\varphi(x))$ .
- Test functions are periodic, so they are exactly $C_c^\infty$ of the cylinder, and no boundary terms arise at $t=0,1$ .
Not vacuous: e.g. $\eta$ a test section with $f=D_S\eta$ . The statement is true, by $L^p$ elliptic regularity for $1<p<\infty$ .

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

Global regularity of weak L^p solutions of Cauchy–Riemann equations on the cylinder

Read-back: CauchyRiemannIndex.memW1p_of_weak_solution

Read-back: `CauchyRiemannIndex.memW1p_of_weak_solution`