Continuity of the symplectization coordinates of a map

Proved

FiniteEnergyPlane.continuous_aCoord_proj_comp

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 $u : \mathbb{C} \to V_n$ be continuous with $u(z) \neq 0$ for all $z$ . Then $z \mapsto a_H(u(z))$ and $z \mapsto \mathrm{proj}_H(u(z))$ are continuous.

Role. Basic regularity used whenever a plane is read in the coordinates of the symplectization.

Preamble

import Definitions.Def_FiniteEnergyPlane_Setting

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- The symplectization coordinates of a continuous map avoiding `0` are continuous. -/
theorem continuous_aCoord_proj_comp {n : ℕ} (H : V n → ℝ) (hH : IsStrictlyStarShapedLevel H)
    (u : ℂ → V n) (hu0 : ∀ z, u z ≠ 0) (huc : Continuous u) :
    Continuous (fun z => aCoord H (u z)) ∧ Continuous (fun z => proj H (u z)) := 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