A puncture of zero charge is removable
ProvedFiniteEnergyPlane.isRemovablePuncture_of_tendsto_loopAction_zerofinite-energypseudoholomorphic-curvesreeb-dynamicssymplectic-geometry
Let be a strictly star-shaped level with contact form and -compatible complex structure on , and let be a finite-energy -holomorphic curve on the punctured unit disc. Write for the action of the clockwise loop , and call for the gradient bound near the puncture, where (-invariant). Assume the gradient bound near the puncture and as . Then the puncture is removable: agrees on with a smooth -holomorphic map . (With zero charge the shifted cylinders converge to constants, so stays bounded near , maps a punctured neighbourhood of into a compact subset of with finite Euclidean energy, and the removable singularity theorem applies.)
Preamble
import Definitions.Def_FiniteEnergyPlane_Setting
Formal statement
namespace FiniteEnergyPlane
open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real
/-- (c) Zero charge: under the gradient bound, if the loop actions tend to `0` then the puncture
is removable. -/
theorem isRemovablePuncture_of_tendsto_loopAction_zero {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 (ball 0 1 \ {0}) u)
(hG : ∃ r : ℝ, 0 < r ∧ ∃ C : ℝ, ∀ z : ℂ, z ≠ 0 → ‖z‖ < r → ‖z‖ * gradNorm H u z ≤ C)
(hQ : Tendsto (fun ρ => loopAction H u (cwLoop 0 ρ)) (𝓝[>] 0) (𝓝 0)) :
IsRemovablePuncture H J u 0 1 := by
sorry
end FiniteEnergyPlaneSource
H. Hofer, Pseudoholomorphic curves in symplectizations with applications to the Weinstein conjecture in dimension three, Invent. Math. 114 (1993), 515-563, Section 3 (removability when the charge vanishes); C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Theorem 9.8 and its proof, pp. 157-160