A nonzero point is determined by its symplectization coordinates

Proved

FiniteEnergyPlane.eq_of_aCoord_eq_of_proj_eq

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

pseudoholomorphic-curvessymplectic-geometry

Let $H$ be a strictly star-shaped level function on $V_n$ . If $x, y \in V_n \setminus \{0\}$ satisfy $a_H(x) = a_H(y)$ and $\mathrm{proj}_H(x) = \mathrm{proj}_H(y)$ , then $x = y$ .

Role. Injectivity of the coordinates $(a_H, \mathrm{proj}_H)$ on $V_n \setminus \{0\}$ .

Preamble

import Definitions.Def_FiniteEnergyPlane_Setting

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- A nonzero point of `V n` is determined by its symplectization coordinates `aCoord H`, `proj H`. -/
theorem eq_of_aCoord_eq_of_proj_eq {n : ℕ} (H : V n → ℝ) (hH : IsStrictlyStarShapedLevel H)
    {x y : V n} (hx : x ≠ 0) (hy : y ≠ 0) (ha : aCoord H x = aCoord H y)
    (hp : proj H x = proj H y) : x = y := by
  sorry

end FiniteEnergyPlane

Source

Elementary lemma in the setting of U. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. AMS 364 (2012), arXiv:0812.4076

View graph