Radial scaling in symplectization coordinates

Proved

FiniteEnergyPlane.proj_aCoord_exp_smul

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$ , and let $y \in V_n$ , $y \neq 0$ . For every $c \in \mathbb{R}$ ,

\mathrm{proj}_H(e^{2c} y) = \mathrm{proj}_H(y), \qquad a_H(e^{2c} y) = a_H(y) + c,

where $a_H$ is aCoord H.

Role. In the identification $V_n \setminus \{0\} \cong \mathbb{R} \times S$ , this says that scaling by $e^{2c}$ is the translation by $c$ in the $\mathbb{R}$ -direction.

Preamble

import Definitions.Def_FiniteEnergyPlane_Setting

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- For `y ≠ 0`, scaling by `e^{2c}` fixes `proj H y` and adds `c` to `aCoord H y`. -/
theorem proj_aCoord_exp_smul {n : ℕ} (H : V n → ℝ) (hH : IsStrictlyStarShapedLevel H)
    (c : ℝ) (y : V n) (hy : y ≠ 0) :
    proj H (Real.exp (2 * c) • y) = proj H y ∧ aCoord H (Real.exp (2 * c) • y) = aCoord H y + c := 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