A J-holomorphic plane with bounded angular derivative has finite Hofer energy

Proved

FiniteEnergyPlane.energy_univ_lt_top_of_norm_fderiv_mul_I_le

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

pseudoholomorphic-curvessymplectic-geometry

Let $S = H^{-1}(1)$ be a strictly star-shaped level in $V_n$ and $J$ a compatible complex structure on $\xi$ . Let $u : \mathbb{C} \to V_n$ be smooth, avoid $0$ and be $\tilde J$ -holomorphic, and suppose the projection $w = \mathrm{proj} \circ u$ to $S$ has bounded angular derivative: $\|Dw(z)(iz)\| \leq K$ for all $z$ . Then the Hofer energy of $u$ on $\mathbb{C}$ is finite.

A criterion for finite energy in terms of the derivative in the circle direction only.

Preamble

import Definitions.Def_FiniteEnergyPlane_Asymptotics

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- A smooth `J̃`-holomorphic plane avoiding `0` whose projection to `S` has bounded angular
derivative, `‖D(proj ∘ u)(z)(i z)‖ ≤ K` for all `z`, has finite Hofer energy. -/
theorem energy_univ_lt_top_of_norm_fderiv_mul_I_le {n : ℕ} (H : V n → ℝ)
    (hH : IsStrictlyStarShapedLevel H) (J : V n → V n →L[ℝ] V n)
    (hJ : IsCompatibleXiStructure H J) (u : ℂ → V n) (hu : ContDiff ℝ ∞ u) (hu0 : ∀ z, u z ≠ 0)
    (hhol : JHolomorphic.IsJHolomorphicOn (Jtilde H J) Set.univ u) (K : ℝ)
    (hK : ∀ z, ‖fderiv ℝ (fun z => proj H (u z)) z (z * Complex.I)‖ ≤ K) :
    energy H Set.univ u < ⊤ := by
  sorry

end FiniteEnergyPlane

Source

H. Hofer, Invent. Math. 114 (1993), § 3; U. Hryniewicz, Trans. AMS 364 (2012), § 6

View graph