Exponential decay of solutions of linear Cauchy–Riemann equations on a half-cylinder

Proved

FiniteEnergyPlane.halfCyl_exp_decay

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$ , and $S_\infty$ a $C^\infty$ $1$ -periodic loop of symmetric matrices with $S\to S_\infty$ in $C^\infty$ and $-J_0\partial_t-S_\infty$ nondegenerate. If $\zeta$ is a solution of $\partial_s\zeta+J_0\partial_t\zeta+S\zeta=0$ on the half-cylinder with $\zeta\to0$ uniformly, then there are $\delta>0$ and $C$ with $\|\zeta(s,t)\|\le Ce^{-\delta s}$ for all $s\ge1$ and $t$ .

Formalization Note $\zeta$ satisfies IsHalfCylSolution S ζ ( $C^\infty$ on $(0,\infty)\times\mathbb{R}$ ). Smoothness of $S$ and $S_\infty$ is entrywise.

Preamble

import Definitions.Def_FiniteEnergyPlane_Asymptotics

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- Exponential decay for linear Cauchy–Riemann equations on a half-cylinder: if `S(s, t) → S∞(t)`
in `C^∞`, the asymptotic operator `-J₀ ∂ₜ - S∞` is nondegenerate, and the solution `ζ` of
`∂ₛζ + J₀ ∂ₜζ + S ζ = 0` tends to `0` uniformly, then `ζ` decays exponentially. -/
theorem halfCyl_exp_decay {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))
    (hSas : IsCInftyAsymptoticTo S Sinf) (hnd : CauchyRiemannIndex.IsNondegenerate Sinf)
    (ζ : ℝ × ℝ → CauchyRiemannIndex.Vec n) (hζ : IsHalfCylSolution S ζ)
    (hζ0 : TendstoZeroUnif ζ) :
    ∃ δ > 0, ∃ C : ℝ, ∀ s ≥ 1, ∀ t : ℝ, ‖ζ (s, t)‖ ≤ C * Real.exp (-(δ * s)) := 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.6.6

Read-back

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

Read-back: `FiniteEnergyPlane.halfCyl_exp_decay`

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$ .
$S$ is $C^\infty$ -asymptotic to $S_\infty$ : for every pair of indices $(i,j)$ , the function $f_{ij}(s,t) = S(s,t)_{ij} - S_\infty(t)_{ij}$ (i) is $C^\infty$ on $(s_0,\infty) \times \mathbb R$ for some $s_0$ , and (ii) for every $m \ge 0$ and every $\varepsilon > 0$ there is $s_1$ with $\|D^m f_{ij}(s,t)\| \le \varepsilon$ for all $s \ge s_1$ and all $t$ .
$S_\infty$ is nondegenerate: every $\Psi : \mathbb R \to \mathrm{Mat}$ with $\Psi(0) = I$ and $\Psi'(t) = J_0 S_\infty(t)\Psi(t)$ for all $t$ satisfies $\det(I - \Psi(1)) \neq 0$ .
$\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 \to 0$ uniformly: for every $\varepsilon > 0$ there is $s_0$ with $\|\zeta(s,t)\| \le \varepsilon$ for all $s \ge s_0$ and all $t$ .

Conclusion. There exist $\delta > 0$ and a real number $C$ such that

\|\zeta(s,t)\| \le C\, e^{-\delta s} \quad \text{for all } s \ge 1 \text{ and all } t \in \mathbb R.

Only the norm of $\zeta$ itself is bounded (no derivatives), and only on $s \ge 1$ . For $n = 0$ , $E$ is the zero space, $\zeta \equiv 0$ , and the conclusion is immediate.

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

Exponential decay of solutions of linear Cauchy–Riemann equations on a half-cylinder

Read-back: FiniteEnergyPlane.halfCyl_exp_decay

Read-back: `FiniteEnergyPlane.halfCyl_exp_decay`