A finite-energy curve near infinity, read on a punctured disc via $z\mapsto z^{-1}$

Proved

FiniteEnergyPlane.isFiniteEnergyCurve_comp_inv_exterior

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

finite-energypseudoholomorphic-curvessymplectization

Let $S=H^{-1}(1)\subset\mathbb{R}^{2n+2}$ be a strictly star-shaped level, let $J$ be a compatible complex structure on $\xi$ and $\tilde J$ the induced almost complex structure on $\mathbb{R}^{2n+2}\setminus\{0\}\cong\mathbb{R}\times S$ . Let $R\in\mathbb{R}$ , and let $u$ be a finite-energy $\tilde J$ -holomorphic curve on the exterior region $\{z\in\mathbb{C}: |z|>R\}$ (smooth, avoiding $0$ , $\tilde J$ -holomorphic, with finite Hofer energy). Let $\rho>0$ with $R\rho\le 1$ . Then $v(z)=u(z^{-1})$ is a finite-energy $\tilde J$ -holomorphic curve on the punctured disc $B(0,\rho)\setminus\{0\}$ , and for every $z\neq 0$ with $|z^{-1}|>R$ ,

v^*d\lambda\ \text{density at } z \;=\; |z|^{-4}\cdot\big(u^*d\lambda\ \text{density at } z^{-1}\big),

where the $d\lambda$ -density of $u$ at $z$ is $\omega_0(\partial_s w,\partial_t w)$ with $w=\mathrm{pr}\circ u$ .

This lets statements about finite-energy curves near the puncture $0$ of a punctured disc be applied to a curve near its puncture at $\infty$ . It extends the case of planes ( $u$ defined on all of $\mathbb{C}$ , unit disc) to curves defined only outside a disc.

Formalization Note $\mathbb{R}^{2n+2}$ is V n, $\tilde J$ is Jtilde H J, $\mathrm{pr}$ is proj H; "finite-energy curve on $U$ " is IsFiniteEnergyCurve H J U, and the $d\lambda$ -density is dlambdaDensity H. $R$ may be zero or negative, in which case the exterior region is $\mathbb{C}$ (for $R<0$ ) or $\mathbb{C}\setminus\{0\}$ (for $R=0$ ).

Preamble

import Definitions.Def_FiniteEnergyPlane_Setting

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- A finite-energy `J̃`-holomorphic curve on the exterior region `{|z| > R}`, read in the
coordinate `z ↦ z⁻¹`, is a finite-energy `J̃`-holomorphic curve on the punctured disc
`B(0, ρ) \ {0}` whenever `ρ > 0` and `R ρ ≤ 1`, and its `dλ`-density at `z` is `|z|⁻⁴` times the
density of `u` at `z⁻¹`. This is the domain version of `isFiniteEnergyCurve_comp_inv`, which treats
planes (`U = ℂ`). -/
theorem isFiniteEnergyCurve_comp_inv_exterior {n : ℕ} (H : V n → ℝ)
    (hH : IsStrictlyStarShapedLevel H) (J : V n → V n →L[ℝ] V n) (hJ : IsCompatibleXiStructure H J)
    (R ρ : ℝ) (hρ : 0 < ρ) (hRρ : R * ρ ≤ 1) (u : ℂ → V n)
    (hu : IsFiniteEnergyCurve H J {z | R < ‖z‖} u) :
    IsFiniteEnergyCurve H J (ball 0 ρ \ {0}) (fun z => u z⁻¹) ∧
      ∀ z : ℂ, z ≠ 0 → R < ‖z⁻¹‖ →
        dlambdaDensity H (fun z => u z⁻¹) z = (‖z‖ ^ 4)⁻¹ * dlambdaDensity H u z⁻¹ := by
  sorry

end FiniteEnergyPlane

Source

H. Hofer, K. Wysocki, E. Zehnder; U. Hryniewicz, J. Symplectic Geom. 12 (2014), arXiv:1105.2077, Section 2.2 (punctures at infinity; standard change of coordinates)

View graph

A finite-energy curve near infinity, read on a punctured disc via z↦z−1z\mapsto z^{-1}z↦z−1

A finite-energy curve near infinity, read on a punctured disc via $z\mapsto z^{-1}$