A strictly star-shaped level is compact

Proved

FiniteEnergyPlane.isCompact_energySurface

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. Then $S$ is compact.

Preamble

import Definitions.Def_FiniteEnergyPlane_Setting

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- A strictly star-shaped level `S = H⁻¹(1)` is compact. -/
theorem isCompact_energySurface {n : ℕ} (H : V n → ℝ) (hH : IsStrictlyStarShapedLevel H) :
    IsCompact (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