Asymptotic formula for linear Cauchy–Riemann equations on a half-cylinder

Proved

FiniteEnergyPlane.halfCyl_asymptotic_formula

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

asymptotic-operatorpseudoholomorphic-curvesreeb-dynamicssymplectic-geometrysymplectization

Let $S:\mathbb{R}^2\to\mathbb{R}^{2n\times2n}$ be $C^\infty$ and $1$ -periodic in $t$ , $S_\infty$ a $C^\infty$ $1$ -periodic loop of symmetric matrices, and $d>0$ with $S-S_\infty$ decaying like $e^{-ds}$ in $C^\infty$ . Let $\zeta$ be a solution of $\partial_s\zeta+J_0\partial_t\zeta+S\zeta=0$ on the half-cylinder, not identically zero on $(0,\infty)\times\mathbb{R}$ , with $\|\zeta(s,t)\|\le Ce^{\delta_0s}$ for $s>0$ . Then there are an eigenvalue $\mu\le\delta_0$ of $-J_0\partial_t-S_\infty$ and an eigenfunction $e$ for $\mu$ such that $e^{-\mu s}\zeta(s,t)-e(t)\to0$ in $C^\infty$ .

Formalization Note The eigenfunction is IsLoopEigen Sinf μ e; the convergence is TendstoZeroCInfty of fun p => Real.exp (-(μ * p.1)) • ζ p - e p.2.

Preamble

import Definitions.Def_FiniteEnergyPlane_Asymptotics

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- Asymptotic formula for linear Cauchy–Riemann equations on a half-cylinder: if `S(s, t) - S∞(t)`
decays exponentially in `C^∞` and `ζ` is a solution of `∂ₛζ + J₀ ∂ₜζ + S ζ = 0`, not identically
zero, with `‖ζ(s, t)‖ ≤ C e^{δ₀ s}`, then there are an eigenvalue `μ ≤ δ₀` of `-J₀ ∂ₜ - S∞` and an
eigenfunction `e` with `e^{-μs} ζ(s, t) - e(t) → 0` in `C^∞`. -/
theorem halfCyl_asymptotic_formula {n : ℕ} (S : ℝ × ℝ → CauchyRiemannIndex.Mat n)
    (hS : ∀ i j, ContDiff ℝ ∞ (fun p : ℝ × ℝ => S p i j)) (hSper : ∀ s t : ℝ, S (s, t + 1) = S (s, t))
    (Sinf : ℝ → CauchyRiemannIndex.Mat n) (hSinf : CauchyRiemannIndex.IsSymLoop Sinf)
    (hSinf' : ∀ i j, ContDiff ℝ ∞ (fun t => Sinf t i j))
    (d : ℝ) (hd : 0 < d) (hSas : IsExpAsymptoticTo S Sinf d)
    (ζ : ℝ × ℝ → CauchyRiemannIndex.Vec n) (hζ : IsHalfCylSolution S ζ)
    (hne : ∃ p : ℝ × ℝ, 0 < p.1 ∧ ζ p ≠ 0)
    (C δ₀ : ℝ) (hgrowth : ∀ s > 0, ∀ t : ℝ, ‖ζ (s, t)‖ ≤ C * Real.exp (δ₀ * s)) :
    ∃ μ : ℝ, μ ≤ δ₀ ∧ ∃ e : ℝ → CauchyRiemannIndex.Vec n, IsLoopEigen Sinf μ e ∧
      TendstoZeroCInfty (fun p : ℝ × ℝ => Real.exp (-(μ * p.1)) • ζ p - e p.2) := by
  sorry

end FiniteEnergyPlane

Source

C. Wendl, Lectures on Symplectic Field Theory, lecture notes, Humboldt-Universität zu Berlin (2026 version); earlier version arXiv:1612.01009, Theorem 4.8.2, formula (4.26); R. Siefring, Relative asymptotic behavior of pseudoholomorphic half-cylinders, Comm. Pure Appl. Math. 61 (2008), arXiv:math/0702356, Appendix A

Read-back

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

Read-back: `FiniteEnergyPlane.halfCyl_asymptotic_formula`

Setting. Fix $n \in \mathbb N$ (including $n = 0$ ). $E = \mathbb R^{2n}$ with coordinates $(a_1,\dots,a_n,b_1,\dots,b_n)$ , the Euclidean inner product and the Euclidean norm $\|\cdot\|$ . $\mathrm{Mat}$ denotes real $2n \times 2n$ matrices indexed the same way, acting on $E$ by matrix multiplication; $J_0 = \begin{pmatrix} 0 & -I \\ I & 0\end{pmatrix}$ , so $J_0(a,b) = (-b,a)$ . Points of $\mathbb R^2$ are written $(s,t)$ , and $\mathbb R^2$ carries the sup norm. For a map $f$ on $\mathbb R^2$ , $D^m f$ is its $m$ -th Fréchet derivative (zero at points where $f$ is not $m$ times differentiable), $D^0 f = f$ , measured in operator norm. Partial derivatives are $\partial_s u = Du\,(1,0)$ and $\partial_t u = Du\,(0,1)$ .

Hypotheses.

$S : \mathbb R^2 \to \mathrm{Mat}$ ; every entry $(s,t) \mapsto S(s,t)_{ij}$ is $C^\infty$ on $\mathbb R^2$ ; and $S(s, t+1) = S(s,t)$ for all $s, t$ .
$S_\infty : \mathbb R \to \mathrm{Mat}$ is a symmetric loop (continuous, $1$ -periodic, each $S_\infty(t)$ symmetric), and every entry $t \mapsto S_\infty(t)_{ij}$ is $C^\infty$ .
$d > 0$ , and $S$ is exponentially asymptotic to $S_\infty$ with rate $d$ : for every pair $(i,j)$ , the function $f_{ij}(s,t) = S(s,t)_{ij} - S_\infty(t)_{ij}$ is $C^\infty$ on $(s_0,\infty) \times \mathbb R$ for some $s_0$ , and for every $m \ge 0$ there are real $C_m, s_m$ with $\|D^m f_{ij}(s,t)\| \le C_m e^{-d s}$ for all $s \ge s_m$ and all $t$ .
$\zeta : \mathbb R^2 \to E$ is a half-cylinder solution for $S$ : $\zeta$ is $C^\infty$ on $(0,\infty) \times \mathbb R$ ; $\zeta(s,t+1) = \zeta(s,t)$ for all real $s, t$ (including $s \le 0$ ); and for all $s > 0$ and all $t$ ,

\partial_s \zeta(s,t) + J_0\, \partial_t \zeta(s,t) + S(s,t)\, \zeta(s,t) = 0.

$\zeta(s,t) \neq 0$ for at least one point with $s > 0$ .
$C$ and $\delta_0$ are real numbers (no sign constraints) with

\|\zeta(s,t)\| \le C\, e^{\delta_0 s} \quad \text{for all } s > 0,\ t \in \mathbb R.

No nondegeneracy condition on $S_\infty$ is assumed.

Conclusion. There exist a real number $\mu$ with $\mu \le \delta_0$ and a map $e : \mathbb R \to E$ such that:

$e$ is an eigenvector of $S_\infty$ with eigenvalue $\mu$ : $e$ is $C^\infty$ , $1$ -periodic, $e(t) \neq 0$ for some $t$ , and for all $t$

-J_0\, e'(t) - S_\infty(t)\, e(t) = \mu\, e(t);

the function $g(s,t) = e^{-\mu s}\, \zeta(s,t) - e(t)$ tends to $0$ in $C^\infty$ : $g$ is $C^\infty$ on $(s_0', \infty) \times \mathbb R$ for some $s_0'$ , and for every $m \ge 0$ and every $\varepsilon > 0$ there is $s_1$ with $\|D^m g(s,t)\| \le \varepsilon$ for all $s \ge s_1$ and all $t$ .

The bound $\mu \le \delta_0$ is non-strict. For $n = 0$ , $E$ is the zero space, so the hypothesis that $\zeta$ is somewhere nonzero cannot hold and the statement is vacuous; similarly, if $C \le 0$ the growth bound forces $\zeta = 0$ on $s > 0$ , contradicting that hypothesis.

Human review

Endorsed by Shuze Chen · Oct 21, 2026
Confirmed by the moderator at approval.
Endorsed by Mazecto · Oct 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Asymptotic formula for linear Cauchy–Riemann equations on a half-cylinder

Read-back: FiniteEnergyPlane.halfCyl_asymptotic_formula

Read-back: `FiniteEnergyPlane.halfCyl_asymptotic_formula`