Actions of circles are bounded by the Hofer energy on the punctured plane

Proved

FiniteEnergyPlane.ofReal_loopAction_ccwLoop_le_energy

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

contact-geometrypseudoholomorphic-curvessymplectic-geometry

Let $u$ be a finite-energy $\tilde J$ -holomorphic curve on $\mathbb{C}\setminus\{0\}$ with $a(u(z))\to-\infty$ as $z\to0$ . Then for every $\rho>0$ the action of the counterclockwise loop $t\mapsto\mathrm{proj}(u(\rho e^{2\pi it}))$ is at most the Hofer energy of $u$ on $\mathbb{C}\setminus\{0\}$ .

Preamble

import Definitions.Def_FiniteEnergyPlane_Setting

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- Actions are bounded by the Hofer energy. Let `u` be a finite-energy `J̃`-holomorphic curve on
`ℂ \ {0}` with `a(u(z)) → -∞` as `z → 0`. Then for every `ρ > 0` the action of the counterclockwise
circle of radius `ρ` is at most the Hofer energy of `u` on `ℂ \ {0}`. -/
theorem ofReal_loopAction_ccwLoop_le_energy {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 {z | z ≠ 0} u)
    (hneg : Tendsto (fun z => aCoord H (u z)) (𝓝[≠] 0) atBot) (ρ : ℝ) (hρ : 0 < ρ) :
    ENNReal.ofReal (loopAction H u (ccwLoop ρ)) ≤ energy H {z | z ≠ 0} u := by
  sorry

end FiniteEnergyPlane

Source

U. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. Amer. Math. Soc. 364 (2012), 1859-1931, Lemma 4.11; H. Hofer, K. Wysocki, E. Zehnder, Finite energy cylinders of small area, Ergodic Theory Dynam. Systems 22 (2002), 1451-1486, Theorem 1.1

View graph