Coercive estimate, up to one direction per positive zero, for a Cauchy–Riemann operator with a large antilinear term

Proved

CauchyRiemannIndex.large_antilinear_coercive_estimate

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

analysiscauchy-riemann-operatorspde

Identify $\mathbb R^2$ with $\mathbb C$ and consider the cylinder $\mathbb R\times S^1$ , $S^1=\mathbb R/\mathbb Z$ , with coordinates $(s,t)$ . Let $\beta:\mathbb R\times\mathbb R\to\mathbb C$ be smooth and $1$ -periodic in $t$ , with bounded derivative, and assume there are $R,c>0$ with $c\le|\beta(s,t)|\le 1/c$ for $|s|\ge R$ . Let $Z^+,Z^-\subset\mathbb R\times[0,1)$ be disjoint finite sets such that the zeros of $\beta$ are exactly the points $(\zeta_1,\zeta_2+m)$ , $\zeta\in Z^+\cup Z^-$ , $m\in\mathbb Z$ , and let $r>0$ be such that for $|z|<r$

\beta(\zeta+z)=z\quad(\zeta\in Z^+),\qquad \beta(\zeta+z)=\bar z\quad(\zeta\in Z^-).

For $\sigma\in\mathbb R$ put

D_\sigma\eta=\partial_s\eta+i\,\partial_t\eta+\sigma\,\beta\,\bar\eta .

Then there are constants $A$ and $\sigma_0>0$ such that for every $\sigma\ge\sigma_0$ there exist smooth functions $\Phi_\zeta:\mathbb R\times\mathbb R\to\mathbb C$ ( $\zeta\in Z^+$ ), $1$ -periodic in $t$ and vanishing for large $|s|$ , with

\|\eta\|_{L^2}^2\;\le\;\frac{A}{\sigma}\,\|D_\sigma\eta\|_{L^2}^2+\sum_{\zeta\in Z^+}\langle\Phi_\zeta,\eta\rangle_{L^2}^2

for every smooth $\eta:\mathbb R\times\mathbb R\to\mathbb C$ that is $1$ -periodic in $t$ and vanishes for large $|s|$ . Here $L^2$ norms and real inner products $\langle u,v\rangle=\int\mathrm{Re}(u\bar v)$ are taken over $\mathbb R\times[0,1)$ .

This is a quantitative injectivity statement for $D_\sigma$ at large $\sigma$ : apart from at most $\#Z^+$ directions, $\|D_\sigma\eta\|$ dominates $\sqrt{\sigma}\,\|\eta\|$ . It is the analytic input for the bound $\dim\ker D_\sigma\le\#Z^+$ in Wendl's Lemma 5.22 and in the index computation of Proposition 5.27.

Formalization Note. Sections are maps ℝ × ℝ → Vec 1 (Vec 1 = ℝ²) satisfying IsTestSection; $D_\sigma$ is crOp (fun x => σ • antilinearMat (β x)), where antilinearMat β is the real matrix of $z\mapsto\beta\bar z$ ; integrals are over cylMeasure (Lebesgue measure on $\mathbb R\times[0,1)$ ). The functions $\Phi_\zeta$ are given as a family Φ : ℝ × ℝ → ℝ × ℝ → Vec 1 of which only the members with ζ ∈ Zplus are used.

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

/-- A coercive estimate for a Cauchy–Riemann operator with a large antilinear term (Wendl,
Lecture 5, setting of § 5.5). Let `β : ℝ × S¹ → ℂ` be smooth and `1`-periodic in `t`, with bounded
derivative and with `|β|` bounded below for large `|s|`; let its zeros (mod `t ↦ t + 1`) be the
finite sets `Z⁺` and `Z⁻`, with `β(ζ + z) = z` for `ζ ∈ Z⁺` and `β(ζ + z) = z̄` for `ζ ∈ Z⁻` on the
disc `|z| < r`. Then there are `A` and `σ₀ > 0` such that for every `σ ≥ σ₀` there are smooth
compactly supported sections `Φ_ζ` (`ζ ∈ Z⁺`) with
`‖η‖²_{L²} ≤ (A/σ) ‖∂ₛη + J₀∂ₜη + σ β η̄‖²_{L²} + Σ_{ζ ∈ Z⁺} ⟨Φ_ζ, η⟩²_{L²}`
for every test section `η` of the cylinder. -/
theorem large_antilinear_coercive_estimate (β : ℝ × ℝ → ℂ) (hβ : ContDiff ℝ ∞ β)
    (hβper : ∀ s t, β (s, t + 1) = β (s, t))
    (hβC1 : ∃ C : ℝ, ∀ x, ‖fderiv ℝ β x‖ ≤ C)
    (hβends : ∃ (R c : ℝ), 0 < c ∧ ∀ s t, R ≤ |s| → c ≤ ‖β (s, t)‖ ∧ ‖β (s, t)‖ ≤ 1 / c)
    (Zplus Zminus : Finset (ℝ × ℝ)) (hZ : ∀ ζ ∈ Zplus ∪ Zminus, 0 ≤ ζ.2 ∧ ζ.2 < 1)
    (hdisj : Disjoint Zplus Zminus)
    (hzero : ∀ x : ℝ × ℝ, β x = 0 ↔ ∃ ζ ∈ Zplus ∪ Zminus, ∃ m : ℤ, x = (ζ.1, ζ.2 + m))
    (r : ℝ) (hr : 0 < r)
    (hplusZ : ∀ ζ ∈ Zplus, ∀ z : ℂ, ‖z‖ < r → β (ζ.1 + z.re, ζ.2 + z.im) = z)
    (hminusZ : ∀ ζ ∈ Zminus, ∀ z : ℂ, ‖z‖ < r → β (ζ.1 + z.re, ζ.2 + z.im) = (starRingEnd ℂ) z) :
    ∃ A σ₀ : ℝ, 0 < σ₀ ∧ ∀ σ ≥ σ₀, ∃ Φ : ℝ × ℝ → ℝ × ℝ → Vec 1,
      (∀ ζ ∈ Zplus, IsTestSection (Φ ζ)) ∧
      ∀ η : ℝ × ℝ → Vec 1, IsTestSection η →
        ∫ x, ‖η x‖ ^ 2 ∂cylMeasure ≤
          A / σ * ∫ x, ‖crOp (fun x => σ • antilinearMat (β x)) η x‖ ^ 2 ∂cylMeasure +
            ∑ ζ ∈ Zplus, (∫ x, ⟪Φ ζ x, η x⟫ ∂cylMeasure) ^ 2 := by
  sorry

end CauchyRiemannIndex

Source

C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, Lecture 5, § 5.5 (setting of Lemma 5.22)

View graph