Gradient bound near a puncture of a finite-energy curve
ProvedFiniteEnergyPlane.exists_norm_mul_gradNorm_le_near_puncturefinite-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). Then there are and with for all . Otherwise there are with ; rescaling on and bubbling off near (Hofer's lemma) gives a nonconstant finite-energy plane whose -energy on each disc is bounded by the liminf of the -energies of on discs contained in . These tend to because , so , contradicting the positivity of the -energy of nonconstant finite-energy planes.
Preamble
import Definitions.Def_FiniteEnergyPlane_Setting
Formal statement
namespace FiniteEnergyPlane
open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real
/-- (b) Gradient bound near a puncture: `|z| · |∇u(z)| ≤ C` near `0` (bubbling off would produce a
nonconstant finite-energy plane whose positive `dλ`-energy is captured in arbitrarily small
punctured discs about `0`). -/
theorem exists_norm_mul_gradNorm_le_near_puncture {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) :
∃ r : ℝ, 0 < r ∧ ∃ C : ℝ, ∀ z : ℂ, z ≠ 0 → ‖z‖ < r → ‖z‖ * gradNorm H u z ≤ C := 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 (gradient bound near punctures, via bubbling off); 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