Prove2Me

Gradient bounds for curves whose dλd\lambda-energy lies below every period

Proved
FiniteEnergyPlane.exists_gradNorm_le_of_dlambdaEnergy_le

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

contact-geometrypseudoholomorphic-curvessymplectic-geometry

Let S=H−1(1)S=H^{-1}(1) be a strictly star-shaped level. Let Uk⊂CU_k\subset\mathbb{C} be open, increasing, with ⋃kUk=C∖{0}\bigcup_k U_k=\mathbb{C}\setminus\{0\}, and let vkv_k be finite-energy J~\tilde J-holomorphic curves on UkU_k with Hofer energy at most CC and dλd\lambda-energy at most ee, where ee is smaller than the period of every periodic Reeb orbit of period at most CC. Then on every compact K⊂C∖{0}K\subset\mathbb{C}\setminus\{0\} the R\mathbb{R}-invariant gradient norm of vkv_k is bounded by a constant MM for all large kk.

Preamble
import Definitions.Def_FiniteEnergyPlane_Setting
Formal statement
namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- Gradient bounds for curves with small `dλ`-energy. Let `U_k` be open, increasing, with
`⋃ U_k = ℂ \ {0}`, and let `v_k` be finite-energy `J̃`-holomorphic curves on `U_k` with Hofer energy
at most `C` and `dλ`-energy at most `e`, where `e` is smaller than every period at most `C` of a
periodic Reeb orbit. Then for every compact `K ⊆ ℂ \ {0}` the `ℝ`-invariant norm `gradNorm` of `v_k`
is bounded on `K` by a constant `M` for all large `k`. -/
theorem exists_gradNorm_le_of_dlambdaEnergy_le {n : ℕ} (H : V n → ℝ) (hH : IsStrictlyStarShapedLevel H)
    (J : V n → V n →L[ℝ] V n) (hJ : IsCompatibleXiStructure H J)
    (U : ℕ → Set ℂ) (hUo : ∀ k, IsOpen (U k))
    (hUm : Monotone U) (hUu : ⋃ k, U k = {z : ℂ | z ≠ 0}) (v : ℕ → ℂ → V n)
    (hv : ∀ k, IsFiniteEnergyCurve H J (U k) (v k)) (C e : ℝ)
    (hE : ∀ k, energy H (U k) (v k) ≤ ENNReal.ofReal C)
    (hd : ∀ k, dlambdaEnergy H (U k) (v k) ≤ ENNReal.ofReal e)
    (he₁ : ∀ Q : ReebOrbit H, Q.T ≤ C → e < Q.T) (K : Set ℂ) (hK : IsCompact K)
    (hK0 : K ⊆ {z : ℂ | z ≠ 0}) :
    ∃ M : ℝ, ∀ᶠ k in atTop, ∀ z ∈ K, gradNorm H (v k) z ≤ M := 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