The asymptotic operator is symmetric

Proved

FiniteEnergyPlane.asympOp_symm

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

asymptotic-operatorpseudoholomorphic-curvesreeb-dynamicssymplectic-geometrysymplectization

Let $S=H^{-1}(1)$ be a strictly star-shaped level, $J$ a smooth $d\lambda_0$ -compatible complex structure on $\xi$ , $P=(x,T)$ a periodic Reeb orbit, and $\eta,\zeta$ two $\xi$ -loops along $P$ . Then $A_P\eta$ is a $\xi$ -loop along $P$ , and

\int_0^1\omega_0\big(A_P\eta(t),J(x(Tt))\zeta(t)\big)\,dt=\int_0^1\omega_0\big(\eta(t),J(x(Tt))A_P\zeta(t)\big)\,dt.

Formalization Note $A_P$ is asympOp J P, acting pointwise on functions ℝ → V n; the integrals are interval integrals over $[0,1]$ .

Preamble

import Definitions.Def_FiniteEnergyPlane_Asymptotics

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- Hryniewicz, Definition 2.5: the asymptotic operator `A_P` maps `ξ`-loops to `ξ`-loops and is
symmetric for the `L²` pairing `⟨η, ζ⟩ = ∫₀¹ ω₀(η(t), J(x(Tt)) ζ(t)) dt`. -/
theorem asympOp_symm {n : ℕ} (H : V n → ℝ) (hH : IsStrictlyStarShapedLevel H)
    (J : V n → V n →L[ℝ] V n) (hJ : IsCompatibleXiStructure H J) (P : ReebOrbit H)
    (η ζ : ℝ → V n) (hη : IsXiLoop P η) (hζ : IsXiLoop P ζ) :
    IsXiLoop P (asympOp J P η) ∧
      ∫ t in (0 : ℝ)..1, omega0 (asympOp J P η t) (J (P.x (P.T * t)) (ζ t)) =
        ∫ t in (0 : ℝ)..1, omega0 (η t) (J (P.x (P.T * t)) (asympOp J P ζ t)) := by
  sorry

end FiniteEnergyPlane

Source

U. Hryniewicz, Systems of global surfaces of section for dynamically convex Reeb flows on the 3-sphere, J. Symplectic Geom. 12 (2014), arXiv:1105.2077, Definition 2.5 and Remark 2.6

Read-back

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

Read-back: `FiniteEnergyPlane.asympOp_symm`

Setting. Fix $n \in \mathbb N$ (including $n = 0$ ) and let $V = \mathbb R^{2n+2}$ with coordinates $v_0, \dots, v_{2n+1}$ . Write $(j_0 v)_{2i} = -v_{2i+1}$ , $(j_0 v)_{2i+1} = v_{2i}$ , $\langle u, v\rangle = \sum_k u_k v_k$ , and

\omega_0(u, v) = \langle j_0 u, v\rangle = \sum_i \bigl(u_{2i} v_{2i+1} - u_{2i+1} v_{2i}\bigr), \qquad \lambda_x(v) = \tfrac12\, \omega_0(x, v).

For $H : V \to \mathbb R$ , $dH_x$ is the Fréchet derivative at $x$ (the zero map where $H$ is not differentiable), $\nabla H(x) = (dH_x(e_k))_k$ , $X_H = j_0 \nabla H$ , and the Reeb field is $R(x) = \lambda_x(X_H(x))^{-1} X_H(x)$ with $0^{-1} = 0$ ; $DR(x)$ is its Fréchet derivative (zero where $R$ is not differentiable). For $x \in V$ , $\xi_x = \{v : \lambda_x(v) = 0,\ dH_x(v) = 0\}$ .

Hypotheses.

$H$ is strictly star-shaped: $H$ is $C^\infty$ ; for every $u \neq 0$ there is exactly one $r > 0$ with $H(r u) = 1$ ; and $dH_x(x) > 0$ whenever $H(x) = 1$ .
$J$ assigns to each $x \in V$ a linear map $J_x : V \to V$ , and $J$ is compatible with $\xi$ : $x \mapsto J_x$ is $C^\infty$ , and for every $x$ with $H(x) = 1$ and all $v, w \in \xi_x$ :

J_x v \in \xi_x, \quad J_x J_x v = -v, \quad v \neq 0 \Rightarrow \omega_0(v, J_x v) > 0, \quad \omega_0(J_x v, J_x w) = \omega_0(v, w).

$P$ is a Reeb orbit of $H$ : $x_P : \mathbb R \to V$ and $T_P > 0$ with $H(x_P(\tau)) = 1$ , $x_P'(\tau) = R(x_P(\tau))$ and $x_P(\tau + T_P) = x_P(\tau)$ for all $\tau$ .
$\eta, \zeta : \mathbb R \to V$ are $\xi$ -loops along $P$ : each is $C^\infty$ , $1$ -periodic, and takes the value at $t$ in $\xi_{x_P(T_P t)}$ for every $t$ .

Write $J_t = J_{x_P(T_P t)}$ , and define the asymptotic operator on any $\gamma : \mathbb R \to V$ by

(A\gamma)(t) = J_t\Bigl( -\gamma'(t) + T_P\, DR\bigl(x_P(T_P t)\bigr)\, \gamma(t) \Bigr).

Conclusion. Both of the following hold.

$A\eta$ is again a $\xi$ -loop along $P$ : it is $C^\infty$ , $1$ -periodic, and $(A\eta)(t) \in \xi_{x_P(T_P t)}$ for every $t$ .
The following two integrals over $[0,1]$ are equal:

\int_0^1 \omega_0\bigl( (A\eta)(t),\, J_t\, \zeta(t) \bigr)\, dt = \int_0^1 \omega_0\bigl( \eta(t),\, J_t\, (A\zeta)(t) \bigr)\, dt.

The integrals are oriented integrals from $0$ to $1$ (with the convention that a non-integrable integrand gives the value $0$ ). Statement 1 is asserted only for $\eta$ ; the corresponding statement for $\zeta$ is not part of the conclusion.

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

The asymptotic operator is symmetric

Read-back: FiniteEnergyPlane.asympOp_symm

Read-back: `FiniteEnergyPlane.asympOp_symm`