Prove2Me

The dλd\lambda-energy of a plane with a nondegenerate end equals the period

Proved
FiniteEnergyPlane.dlambdaEnergy_univ_eq_of_isNondegenerateEnd

by Mazecto · Nov 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

contact-geometrypseudoholomorphic-curvessymplectic-geometry

Let S=H−1(1)S = H^{-1}(1) be a strictly star-shaped level with contact form λ\lambda, and let u~\tilde u be a finite-energy J~\tilde J-holomorphic plane with a nondegenerate end at ∞\infty, in the sense of Hryniewicz's Definition 2.9 with sign +1+1, asymptotic to the periodic Reeb orbit P=(x,T)P = (x, T). Then

∫Cu∗dλ=T.\int_{\mathbb{C}} u^* d\lambda = T.

This identifies the total dλd\lambda-energy of every plane in the sets Θ(K,P)\Theta(K, P) of fast finite-energy planes, and it is used in the compactness analysis of those sets.

Formalization Note: the integral is dlambdaEnergy H Set.univ u, valued in [0,∞][0, \infty]. The dimension is general.

Preamble
import Definitions.Def_FiniteEnergyPlane_Asymptotics
Formal statement
namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- The total `dλ`-energy of a finite-energy `J̃`-holomorphic plane with a nondegenerate end at `∞`
(Hryniewicz, Definition 2.9, sign `+1`) asymptotic to the periodic Reeb orbit `P` is the period of
`P`. -/
theorem dlambdaEnergy_univ_eq_of_isNondegenerateEnd {n : ℕ} (H : V n → ℝ)
    (hH : IsStrictlyStarShapedLevel H) (J : V n → V n →L[ℝ] V n)
    (hJ : IsCompatibleXiStructure H J) (u : ℂ → V n) (hu : IsFiniteEnergyCurve H J Set.univ u)
    (P : ReebOrbit H) (hnd : IsNondegenerateEnd H u cylInf P 1) :
    dlambdaEnergy H Set.univ u = ENNReal.ofReal P.T := by
  sorry

end FiniteEnergyPlane
Source
U. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. Amer. Math. Soc. 364 (2012), 1859-1931, proof of Corollary 4.9

View graph