Prove2Me

The global-frame coordinates of ξ\xi depend continuously on the base point and the vector

Proved
FiniteEnergyPlane.continuousAt_xiCoordC_prod

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

reeb-dynamicssymplectic-geometrywinding-numbers

Let S=H−1(1)⊂R4S=H^{-1}(1)\subset\mathbb{R}^4 be a strictly star-shaped level, and let Ξx:R4→C\Xi_x:\mathbb{R}^4\to\mathbb{C} be the coordinate map of Hryniewicz's global frame Z1(x),Z2(x)Z_1(x),Z_2(x) of ξ\xi, i.e. Ξx(v)=ω0(v,Z2(x))+i ω0(Z1(x),v)\Xi_x(v)=\omega_0(v,Z_2(x))+i\,\omega_0(Z_1(x),v). Then the map

R4×R4→C,(x,v)↦Ξx(v)\mathbb{R}^4\times\mathbb{R}^4\to\mathbb{C},\qquad (x,v)\mapsto \Xi_x(v)

is jointly continuous at every point (x,v)(x,v) with x∈Sx\in S.

This lets the global-frame coordinates of a ξ\xi-valued section be compared along nearby base points, uniformly on compact sets such as the image of a periodic Reeb orbit.

Formalization Note R4\mathbb{R}^4 is V 1, and Ξx(v)\Xi_x(v) is xiCoordC H x v. The hypothesis x∈Sx\in S is H x = 1. Continuity is ContinuousAt on the product V 1 × V 1 at (x, v).

Preamble
import Definitions.Def_FiniteEnergyPlane_Winding
Formal statement
namespace FiniteEnergyPlane

open Topology

/-- Let `S = H⁻¹(1)` be a strictly star-shaped level. The global-frame coordinate map
`(x, v) ↦ xiCoordC H x v` is jointly continuous at every point `(x, v)` with `x ∈ S`. -/
theorem continuousAt_xiCoordC_prod (H : V 1 → ℝ) (hH : IsStrictlyStarShapedLevel H) {x v : V 1}
    (hx : H x = 1) : ContinuousAt (fun p : V 1 × V 1 => xiCoordC H p.1 p.2) (x, v) := by
  sorry

end FiniteEnergyPlane
Source
U. Hryniewicz, J. Symplectic Geom. 12 (2014), arXiv:1105.2077, Section 2.2.4 (the global frame of ξ\xi on a star-shaped level)

View graph