The symplectization structure $\tilde J$ is a smooth almost complex structure invariant under radial scaling

Proved

FiniteEnergyPlane.jtilde_isAlmostComplexOn

by Mazecto · 1 vote · Oct 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

finite-energypseudoholomorphic-curvesreeb-dynamicssymplectic-geometrysymplectization

Let $S=H^{-1}(1)\subset\mathbb{R}^{2n+2}$ be a strictly star-shaped level and $J$ a smooth $d\lambda_0$ -compatible complex structure on $\xi$ . Then $\tilde J$ is a $C^\infty$ almost complex structure on $V\setminus\{0\}$ , the maps $\mathrm{proj}$ and $a$ are $C^\infty$ on $V\setminus\{0\}$ , every $y\neq0$ satisfies $H(\mathrm{proj}(y))=1$ and $y=e^{2a(y)}\mathrm{proj}(y)$ , and $\tilde J(cy)=\tilde J(y)$ for $y\neq0$ and $c>0$ .

Formalization Note The first claim is JHolomorphic.IsAlmostComplexOn (Jtilde H J) {y | y ≠ 0} (smoothness on the open set and $\tilde J(y)^2=-1$ there). Smoothness of proj H and aCoord H is ContDiffOn ℝ ∞ on {y | y ≠ 0}.

Preamble

import Definitions.Def_FiniteEnergyPlane_Setting

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- The symplectization structure (Hryniewicz 2014, § 2.2; Hofer 1993, § 3). On `V n \ {0}` the
map `J̃` is a smooth almost complex structure, and it is invariant under the radial scaling
`y ↦ c y`, `c > 0` (the `ℝ`-action on `ℝ × S`). The radial projection to `S` and the coordinate
`a` are smooth on `V n \ {0}`, and `y = e^{2a(y)} proj(y)` with `proj(y) ∈ S`. -/
theorem jtilde_isAlmostComplexOn {n : ℕ} (H : V n → ℝ) (hH : IsStrictlyStarShapedLevel H)
    (J : V n → V n →L[ℝ] V n) (hJ : IsCompatibleXiStructure H J) :
    JHolomorphic.IsAlmostComplexOn (Jtilde H J) {y | y ≠ 0} ∧
      ContDiffOn ℝ ∞ (proj H) {y | y ≠ 0} ∧ ContDiffOn ℝ ∞ (aCoord H) {y | y ≠ 0} ∧
      (∀ y : V n, y ≠ 0 → H (proj H y) = 1 ∧ y = Real.exp (2 * aCoord H y) • proj H y) ∧
      ∀ y : V n, y ≠ 0 → ∀ c : ℝ, 0 < c → Jtilde H J (c • y) = Jtilde H J y := by
  sorry

end FiniteEnergyPlane

Source

U. Hryniewicz, Systems of global surfaces of section for dynamically convex Reeb flows on the 3-sphere, J. Symplectic Geom. 12 (2014), arXiv:1105.2077, Section 2.2; H. Hofer, Pseudoholomorphic curves in symplectizations with applications to the Weinstein conjecture in dimension three, Invent. Math. 114 (1993), 515–563, Section 3

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Read-back: `FiniteEnergyPlane.jtilde_isAlmostComplexOn`

Setting. Fix a natural number $n \ge 0$ (implicit) and let $V = \mathbb{R}^{2(n+1)}$ , with coordinates indexed $0, 1, \dots, 2n+1$ (so $\dim V \ge 2$ ). On $V$ the following fixed structures are used:

$j_0 : V \to V$ is the linear map with $(j_0 v)_k = -v_{k+1}$ for $k$ even and $(j_0 v)_k = v_{k-1}$ for $k$ odd; on each coordinate pair $(v_{2i}, v_{2i+1})$ it acts as $(a, b) \mapsto (-b, a)$ .
$\langle u, v \rangle = \sum_k u_k v_k$ is the Euclidean dot product, and $\omega_0(u, v) = \langle j_0 u, v \rangle = \sum_i \big(u_{2i} v_{2i+1} - u_{2i+1} v_{2i}\big)$ .
$\lambda_x(v) = \tfrac12 \omega_0(x, v)$ for $x, v \in V$ .
For $H : V \to \mathbb{R}$ , $dH_x$ denotes the Fréchet derivative of $H$ at $x$ (by convention the zero map if $H$ is not differentiable at $x$ ); $\nabla H(x)$ is the vector with components $dH_x(e_k)$ ; $X_H(x) = j_0 \nabla H(x)$ ; and $R(x) = \lambda_x(X_H(x))^{-1} \, X_H(x)$ (with the convention $0^{-1} = 0$ , so $R(x) = 0$ if $\lambda_x(X_H(x)) = 0$ ).
$\xi_x = \{ v \in V : \lambda_x(v) = 0 \text{ and } dH_x(v) = 0 \}$ , and $S = \{x : H(x) = 1\}$ .

Hypotheses. The statement takes:

a function $H : V \to \mathbb{R}$ such that (i) $H$ is $C^\infty$ ; (ii) for every $u \ne 0$ there is exactly one $r \in \mathbb{R}$ with $r > 0$ and $H(r u) = 1$ ; (iii) for every $x$ with $H(x) = 1$ , $dH_x(x) > 0$ ;
a map $J : V \to \mathcal{L}(V, V)$ (continuous linear endomorphisms of $V$ ) such that $J$ is $C^\infty$ as a map into $\mathcal{L}(V,V)$ , and for every $x \in S$ and all $v, w \in \xi_x$ : $J(x) v \in \xi_x$ ; $J(x)J(x) v = -v$ ; if $v \ne 0$ then $\omega_0(v, J(x) v) > 0$ ; and $\omega_0(J(x) v, J(x) w) = \omega_0(v, w)$ . No condition is placed on $J(x)$ outside $\xi_x$ , nor on $J(x)$ for $x \notin S$ , beyond global smoothness of $J$ .

Auxiliary maps. For $y \in V$ , $s(y)$ is defined as: if some $r > 0$ satisfies $H(r y) = 1$ , then $s(y)$ is a (choice-function-selected) such $r$ ; otherwise $s(y) = 1$ . (For $y \ne 0$ , hypothesis (ii) makes $s(y)$ the unique such $r$ .) Then

\pi(y) = s(y)\, y, \qquad a(y) = -\tfrac12 \log s(y),

where $\log$ is the real logarithm (with the conventions $\log 0 = 0$ and $\log t = \log|t|$ for $t<0$ ). The endomorphism $\tilde J(y) \in \mathcal{L}(V,V)$ is defined, with $x = \pi(y)$ and $r = s(y)$ , by

\alpha(v) = \frac{r}{2\, dH_x(x)}\, dH_x(v), \qquad \beta(v) = r\, \lambda_x(v),

(the fraction is $0$ if $dH_x(x) = 0$ ),

w(v) = v - \alpha(v)\,(2y) - \beta(v)\, r^{-1} R(x),

\tilde J(y)\, v = \alpha(v)\, r^{-1} R(x) - \beta(v)\,(2y) + J(x)\big(w(v)\big).

Conclusion. Under these hypotheses, all five of the following hold:

$\tilde J$ is an almost complex structure on $V \setminus \{0\}$ , meaning: the set $\{y : y \ne 0\}$ is open; $\tilde J$ is $C^\infty$ on that set as a map into $\mathcal{L}(V,V)$ ; and for every $y \ne 0$ , $\tilde J(y) \circ \tilde J(y) = -\mathrm{id}_V$ .
$\pi$ is $C^\infty$ on $\{y \ne 0\}$ .
$a$ is $C^\infty$ on $\{y \ne 0\}$ .
For every $y \ne 0$ : $H(\pi(y)) = 1$ and $y = e^{2 a(y)}\, \pi(y)$ .
For every $y \ne 0$ and every real $c > 0$ : $\tilde J(c y) = \tilde J(y)$ .

Here " $C^\infty$ " means smooth of all finite orders (not real-analytic). Nothing is asserted at $y = 0$ .

Human review

Endorsed by Shuze Chen · Oct 21, 2026
Confirmed by the moderator at approval.
Endorsed by Mazecto · Oct 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

The symplectization structure J~\tilde JJ~ is a smooth almost complex structure invariant under radial scaling

Read-back: FiniteEnergyPlane.jtilde_isAlmostComplexOn

The symplectization structure $\tilde J$ is a smooth almost complex structure invariant under radial scaling

Read-back: `FiniteEnergyPlane.jtilde_isAlmostComplexOn`