Monotonicity: pseudoholomorphic maps through the center of a small ball have energy at least $c\,r^2$

Proved

FiniteEnergyPlane.energy_ge_of_mapsTo_ball

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

finite-energypseudoholomorphic-curvesreeb-dynamicssymplectic-geometrysymplectization

Let $E$ be a finite-dimensional real normed space, $J$ a smooth almost complex structure on an open set $O\subseteq E$ , and $K\subseteq O$ compact. There are $r_0>0$ and $c>0$ with the following property. Let $p\in K$ , $0<r\le r_0$ , let $U\subseteq\mathbb{C}$ be open and let $u$ be $C^\infty$ and $J$ -holomorphic on $U$ , with $u(U)\subseteq B_r(p)$ , $u:U\to B_r(p)$ proper, and $p\in u(U)$ . Then

\int_U\|Du(z)\|^2\,dz\ \ge\ c\,r^2.

Formalization Note $B_r(p)$ is the open ball of the norm of $E$ and $\|Du(z)\|$ is the operator norm of the real derivative $\mathbb{C}\to E$ . Properness is: $U\cap u^{-1}(L)$ is compact for every compact $L\subseteq B_r(p)$ . Zinger states the lower bound for a compact Riemann surface with boundary whose boundary avoids a metric ball of a $J$ -compatible metric, with an explicit constant; here the constant $c$ is unspecified.

Preamble

import Definitions.Def_FiniteEnergyPlane_Setting

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- Monotonicity lemma: Zinger, *Notes on J-holomorphic maps*, Proposition 3.12 (local form);
Gromov 1985; quoted in Wendl, p. 152. Let `J` be a smooth almost complex structure on an open set
`O ⊆ E` and `K ⊆ O` compact. There are `r₀ > 0` and `c > 0` such that for every `p ∈ K` and
`0 < r ≤ r₀`, every smooth `J`-holomorphic map `u` on an open set `U ⊆ ℂ` that maps `U` properly
into the ball `B_r(p)` and passes through `p` has Dirichlet energy `∫_U ‖Du‖² ≥ c r²`.
(Zinger: a compact Riemann surface with boundary whose boundary image avoids a metric ball
`B_ρ(x)` of a `J`-compatible metric `g`, energy `E_g`, and the explicit bound
`ord_x u · ρ² / (1 + C(x) ρ)⁴`. Here: an open `U ⊆ ℂ` with a proper map into a norm ball of `E`,
the operator-norm Dirichlet energy, and an unspecified constant `c`.) -/
theorem energy_ge_of_mapsTo_ball {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (J : E → E →L[ℝ] E) (O : Set E)
    (hJ : JHolomorphic.IsAlmostComplexOn J O) (K : Set E) (hK : IsCompact K) (hKO : K ⊆ O) :
    ∃ r₀ : ℝ, 0 < r₀ ∧ ∃ c : ℝ, 0 < c ∧ ∀ p ∈ K, ∀ r : ℝ, 0 < r → r ≤ r₀ →
      ∀ U : Set ℂ, IsOpen U → ∀ u : ℂ → E, ContDiffOn ℝ ∞ u U →
        JHolomorphic.IsJHolomorphicOn J U u → Set.MapsTo u U (ball p r) →
        (∀ L : Set E, IsCompact L → L ⊆ ball p r → IsCompact (U ∩ u ⁻¹' L)) → p ∈ u '' U →
        ENNReal.ofReal (c * r ^ 2) ≤ ∫⁻ z in U, ENNReal.ofReal (‖fderiv ℝ u z‖ ^ 2) := by
  sorry

end FiniteEnergyPlane

Source

A. Zinger, Notes on J-holomorphic maps, arXiv:1706.00331, Proposition 3.12; C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, p. 152

Read-back

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

Read-back: `FiniteEnergyPlane.energy_ge_of_mapsTo_ball`

Data. Let $E$ be a finite-dimensional real normed vector space (any norm; the norm is not assumed to come from an inner product). Let $J : E \to \mathcal L(E)$ assign to each point $x \in E$ a continuous $\mathbb R$ -linear map $J_x : E \to E$ , and let $O \subseteq E$ . The hypothesis on $(J, O)$ ("almost complex on $O$ ") is:

$O$ is open,
$x \mapsto J_x$ is $C^\infty$ on $O$ (as a map into the normed space of operators),
$J_x \circ J_x = -\mathrm{id}_E$ for every $x \in O$ .

Nothing is assumed about $J_x$ for $x \notin O$ . Let $K \subseteq E$ be compact with $K \subseteq O$ .

Conclusion. There exist constants $r_0 > 0$ and $c > 0$ (depending only on $E$ with its norm, $J$ , $O$ , $K$ ) such that the following holds for every point $p \in K$ , every radius $r$ with $0 < r \le r_0$ , every open set $U \subseteq \mathbb C$ and every map $u : \mathbb C \to E$ satisfying all of:

$u$ is $C^\infty$ on $U$ (as a map of the real vector space $\mathbb C \cong \mathbb R^2$ );
$u$ is $J$ -holomorphic on $U$ : for every $z \in U$ , $u$ is real-differentiable at $z$ and

\partial_s u(z) + J_{u(z)}\,\partial_t u(z) = 0,

where $\partial_s u(z) = Du(z)\cdot 1$ and $\partial_t u(z) = Du(z)\cdot i$ (here $J$ is evaluated at $u(z)$ , whether or not $u(z) \in O$ ); 3. $u(U) \subseteq B(p, r)$ , the open ball of radius $r$ about $p$ in the norm of $E$ ; 4. for every compact $L \subseteq E$ with $L \subseteq B(p,r)$ , the set $U \cap u^{-1}(L)$ is compact; 5. $p \in u(U)$ , i.e. $p = u(z)$ for some $z \in U$ ;

then

c\,r^2 \;\le\; \int_U \|Du(z)\|^2 \, dz ,

where the integral is the Lebesgue integral over $U$ with respect to Lebesgue (area) measure on $\mathbb C$ , taken in $[0, \infty]$ (so the inequality also holds trivially if the right side is $+\infty$ ), and $\|Du(z)\|$ is the operator norm of the real derivative $Du(z) : \mathbb C \to E$ , with $\mathbb C$ normed by the modulus and $E$ by its given norm. (The derivative is taken in the ordinary sense on $\mathbb C$ ; at points of $U$ it exists by hypothesis 2.)

Remarks on edge cases. The ball $B(p,r)$ is not required to lie in $O$ ; only $p \in K \subseteq O$ . If $O$ (hence $K$ ) is empty, the condition on all $p \in K$ is vacuous and the statement reduces to the existence of some positive $r_0, c$ . If $E$ has odd positive dimension, $J_x^2 = -\mathrm{id}$ is impossible, so $O$ and $K$ must be empty and the statement is vacuous in the same way. If $E = \{0\}$ , the condition $J_x^2 = -\mathrm{id}$ holds trivially; in that case hypotheses 3–5 force $U$ to be a nonempty open set with $U = U \cap u^{-1}(\{p\})$ compact, which cannot occur, so the conclusion is vacuous for every $U$ , $u$ . Hypotheses 4 and 5 together exclude $U = \emptyset$ .

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

Monotonicity: pseudoholomorphic maps through the center of a small ball have energy at least c r2c\,r^2cr2

Read-back: FiniteEnergyPlane.energy_ge_of_mapsTo_ball

Monotonicity: pseudoholomorphic maps through the center of a small ball have energy at least $c\,r^2$

Read-back: `FiniteEnergyPlane.energy_ge_of_mapsTo_ball`