The Reeb field of a star-shaped level is Lipschitz on the level

Proved

FiniteEnergyPlane.exists_lipschitzOnWith_reeb

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

contact-geometryreeb-dynamicssymplectic-geometry

Let $S=H^{-1}(1)\subset\mathbb{R}^{2n+2}$ be a strictly star-shaped level with Reeb field $R$ . Then there is $K\ge 0$ such that $\|R(x)-R(y)\|\le K\|x-y\|$ for all $x,y\in S$ .

Preamble

import Definitions.Def_FiniteEnergyPlane_Setting

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- The Reeb field of a strictly star-shaped level `S` is Lipschitz on `S`. -/
theorem exists_lipschitzOnWith_reeb {n : ℕ} (H : V n → ℝ) (hH : IsStrictlyStarShapedLevel H) :
    ∃ K : NNReal, LipschitzOnWith K (reeb H) (energySurface H) := by
  sorry

end FiniteEnergyPlane

Source

U. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. Amer. Math. Soc. 364 (2012), 1859-1931, § 4.4

View graph