At a removable puncture the loop actions tend to zero

Proved

FiniteEnergyPlane.tendsto_loopAction_of_isRemovablePuncture

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

contact-geometrypseudoholomorphic-curvessymplectic-geometry

Let $S=H^{-1}(1)$ be a strictly star-shaped level and let the puncture $0$ of $u$ on the punctured unit disc be removable. Then the actions of the clockwise loops $t\mapsto\mathrm{proj}(u(\rho e^{-2\pi it}))$ tend to $0$ as $\rho\to0^+$ .

Preamble

import Definitions.Def_FiniteEnergyPlane_Setting

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- At a removable puncture `0` of `u` on the punctured unit disc, the actions of the clockwise
circles of radius `ρ` tend to `0` as `ρ → 0⁺`. -/
theorem tendsto_loopAction_of_isRemovablePuncture {n : ℕ} (H : V n → ℝ) (hH : IsStrictlyStarShapedLevel H)
    (J : V n → V n →L[ℝ] V n) (hJ : IsCompatibleXiStructure H J) (u : ℂ → V n)
    (hrem : IsRemovablePuncture H J u 0 1) :
    Tendsto (fun ρ => loopAction H u (cwLoop 0 ρ)) (𝓝[>] 0) (𝓝 0) := 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