Nonnegativity of the energy densities of finite-energy curves

Proved

FiniteEnergyPlane.energyDensity_nonneg

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

finite-energypseudoholomorphic-curvesreeb-dynamicssymplectic-geometrysymplectization

Let $S=H^{-1}(1)$ be a strictly star-shaped level, $J$ a smooth $d\lambda_0$ -compatible complex structure on $\xi$ , $U\subseteq\mathbb{C}$ open and $u$ a finite-energy $\tilde J$ -holomorphic curve on $U$ . Then:

for every $\varphi\in\Sigma$ , the integrand of $u^*d(\varphi(a)\lambda_0)$ is $\ge0$ at every point of $U$ ;
the integrand $\omega_0(\partial_sw,\partial_tw)$ of $u^*d\lambda_0$ is $\ge0$ on $U$ ;
$\int_Uu^*d\lambda_0\le E(u)$ ;
if $U$ is connected and $E(u)=0$ , then $u$ is constant on $U$ .

Formalization Note Connectedness is IsPreconnected U. Both energies are lower integrals in ℝ≥0∞.

Preamble

import Definitions.Def_FiniteEnergyPlane_Setting

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- Hryniewicz 2014, § 2.2.1 and (17); Hofer 1993, (42). For a finite-energy `J̃`-holomorphic
curve on an open set `U ⊆ ℂ`, the integrand of `u*d(φ(a) λ)` is nonnegative for every admissible
`φ`, so is the integrand of `u*dλ`, and the `dλ`-energy is at most the Hofer energy. If `U` is
preconnected and the Hofer energy vanishes, `u` is constant on `U`. -/
theorem energyDensity_nonneg {n : ℕ} (H : V n → ℝ) (hH : IsStrictlyStarShapedLevel H)
    (J : V n → V n →L[ℝ] V n) (hJ : IsCompatibleXiStructure H J) (U : Set ℂ) (hU : IsOpen U)
    (u : ℂ → V n) (hu : IsFiniteEnergyCurve H J U u) :
    (∀ φ : ℝ → ℝ, Admissible φ → ∀ z ∈ U, 0 ≤ energyDensity H φ u z) ∧
      (∀ z ∈ U, 0 ≤ dlambdaDensity H u z) ∧ dlambdaEnergy H U u ≤ energy H U u ∧
      (IsPreconnected U → energy H U u = 0 → ∃ c : V n, ∀ z ∈ U, u z = c) := 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.1 and (17), p. 12; H. Hofer, Pseudoholomorphic curves in symplectizations with applications to the Weinstein conjecture in dimension three, Invent. Math. 114 (1993), 515–563, (42), p. 535

Read-back

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

Read-back: `FiniteEnergyPlane.energyDensity_nonneg`

Ambient space. Fix a natural number $n$ (including $n = 0$ ) and let $V = \mathbb{R}^{2(n+1)}$ , coordinates indexed $k = 0, \dots, 2n+1$ . The code uses:

$j_0 : V \to V$ , $(j_0 v)_k = -v_{k+1}$ for even $k$ , $(j_0 v)_k = v_{k-1}$ for odd $k$ ;
$\langle u, v\rangle = \sum_k u_k v_k$ , $\omega_0(u, v) = \langle j_0 u, v\rangle$ , and $\lambda_x(v) = \tfrac12\,\omega_0(x, v)$ ;
for $H : V \to \mathbb{R}$ : $DH(x)$ is the Fréchet derivative (equal to $0$ where $H$ is not differentiable), $\nabla H(x)_k = DH(x)(e_k)$ , $X_H(x) = j_0 \nabla H(x)$ , $S = \{H = 1\}$ , and $R(x) = (\lambda_x(X_H(x)))^{-1} X_H(x)$ with $0^{-1} = 0$ ;
$\xi_x$ -membership: $v$ "lies in $\xi$ at $x$ " means $\lambda_x(v) = 0$ and $DH(x)(v) = 0$ .

Radial coordinates. For $y \in V$ , let $\rho(y)$ be: some (chosen) $r > 0$ with $H(r y) = 1$ if such an $r$ exists, and $\rho(y) = 1$ otherwise. Put $\pi(y) = \rho(y)\, y$ and $a(y) = -\tfrac12 \log \rho(y)$ (real logarithm).

Hypotheses.

$H : V \to \mathbb{R}$ is a strictly star-shaped level: $H$ is $C^\infty$ ; for each $u \neq 0$ there is exactly one $r > 0$ with $H(r u) = 1$ ; and $DH(x)(x) > 0$ whenever $H(x) = 1$ .
$J : V \to \mathcal{L}(V, V)$ (continuous linear maps) is a compatible $\xi$ -structure: $J$ is $C^\infty$ , and for every $x \in S$ and all $v, w$ lying in $\xi$ at $x$ : $J(x)v$ lies in $\xi$ at $x$ ; $J(x)J(x)v = -v$ ; if $v \neq 0$ then $\omega_0(v, J(x)v) > 0$ ; and $\omega_0(J(x)v, J(x)w) = \omega_0(v, w)$ . Nothing is required of $J(x)$ off $\xi$ , or for $x \notin S$ .
$U \subseteq \mathbb{C}$ is open.
$u : \mathbb{C} \to V$ is a finite-energy curve on $U$ (defined below).

Extended structure $\tilde J$ . For $y \in V$ let $x = \pi(y)$ , $r = \rho(y)$ , and define linear functionals $\alpha(v) = \dfrac{r}{2\,DH(x)(x)}\, DH(x)(v)$ and $\beta(v) = r\,\lambda_x(v)$ , and $w(v) = v - 2\alpha(v)\, y - \beta(v)\, r^{-1} R(x)$ . Then

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

Derivatives of maps from $\mathbb{C}$ . For $f : \mathbb{C} \to F$ (real vector space), $\partial_s f(z) = Df(z)(1)$ and $\partial_t f(z) = Df(z)(i)$ , with $Df(z)$ the real Fréchet derivative (taken to be $0$ where $f$ is not differentiable).

Finite-energy curve. $u$ is a finite-energy curve on $U$ iff: $u$ is $C^\infty$ on $U$ ; $u(z) \neq 0$ for all $z \in U$ ; for every $z \in U$ , $u$ is (real-)differentiable at $z$ and $\partial_s u(z) + \tilde J(u(z))\, \partial_t u(z) = 0$ ; and $E(u; U) < \infty$ (energy defined below).

Densities and energies. Write $a(z) = a(u(z))$ and $w(z) = \pi(u(z))$ as functions of $z \in \mathbb{C}$ . A function $\varphi : \mathbb{R} \to \mathbb{R}$ is admissible if it is $C^\infty$ , monotone nondecreasing, and $0 \le \varphi(s) \le 1$ for all $s$ . For such $\varphi$ , the energy density is

e_\varphi(z) = \varphi'(a(z))\Big(\partial_s a(z)\,\lambda_{w(z)}(\partial_t w(z)) - \partial_t a(z)\,\lambda_{w(z)}(\partial_s w(z))\Big) + \varphi(a(z))\,\omega_0\big(\partial_s w(z), \partial_t w(z)\big),

and the $d\lambda$ -density is $e_{d\lambda}(z) = \omega_0(\partial_s w(z), \partial_t w(z))$ . With Lebesgue measure on $\mathbb{C}$ and $\max(\cdot,0)$ denoting truncation at $0$ (values in $[0, \infty]$ ):

E(u; U) = \sup_{\varphi \text{ admissible}} \int_U \max\big(e_\varphi(z), 0\big)\, dz, \qquad E_{d\lambda}(u; U) = \int_U \max\big(e_{d\lambda}(z), 0\big)\, dz.

Conclusion. All four of the following hold:

for every admissible $\varphi$ and every $z \in U$ , $\;0 \le e_\varphi(z)$ ;
for every $z \in U$ , $\;0 \le e_{d\lambda}(z)$ ;
$E_{d\lambda}(u; U) \le E(u; U)$ (as elements of $[0, \infty]$ );
if $U$ is preconnected and $E(u; U) = 0$ , then there is $c \in V$ with $u(z) = c$ for all $z \in U$ .

Edge cases. $U = \varnothing$ is allowed (it is open and preconnected; all four parts are then immediate). The integrals in the energies use truncated positive parts, so negative density values would not be counted. Part 4 assumes preconnectedness only of $U$ , and asks for constancy of $u$ itself (not of $\pi \circ u$ or $a \circ u$ ).

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

Nonnegativity of the energy densities of finite-energy curves

Read-back: FiniteEnergyPlane.energyDensity_nonneg

Read-back: `FiniteEnergyPlane.energyDensity_nonneg`