Action of a finite-energy plane on any circle equals the $d\lambda$ -energy of its disk

Proved

FiniteEnergyPlane.loopAction_add_ccwLoop_eq_dlambdaEnergy

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

pseudoholomorphic-curvessymplectization

Let $u$ be a finite-energy $\tilde J$ -holomorphic plane in the symplectization of a strictly star-shaped level $S\subset\mathbb{R}^{2n+2}$ . For every $z_0\in\mathbb{C}$ and $\rho>0$ ,

\int_{\partial B_\rho(z_0)}u^*\lambda=\int_{B_\rho(z_0)}u^*d\lambda.

This extends the published identity for disks centered at the origin to arbitrary centers.

Formalization Note The left side is loopAction H u (fun t => z₀ + ccwLoop ρ t), the right side is (dlambdaEnergy H (ball z₀ ρ) u).toReal.

Preamble

import Definitions.Def_FiniteEnergyPlane_Setting

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- For a finite-energy `J̃`-holomorphic plane `u`, the action of `u` along the counterclockwise circle
of radius `ρ` about any center `z₀` equals the `dλ`-energy of `u` on the disk of radius `ρ` about `z₀`. -/
theorem loopAction_add_ccwLoop_eq_dlambdaEnergy {n : ℕ} (H : V n → ℝ)
    (hH : IsStrictlyStarShapedLevel H) (J : V n → V n →L[ℝ] V n) (hJ : IsCompatibleXiStructure H J)
    (u : ℂ → V n) (hu : IsFiniteEnergyCurve H J Set.univ u) (z₀ : ℂ) (ρ : ℝ) (hρ : 0 < ρ) :
    loopAction H u (fun t => z₀ + ccwLoop ρ t) = (dlambdaEnergy H (ball z₀ ρ) u).toReal := by
  sorry

end FiniteEnergyPlane

Source

Auxiliary to U. Hryniewicz, Trans. AMS 364 (2012), arXiv:0812.4076, Section 4

View graph

Action of a finite-energy plane on any circle equals the dλd\lambdadλ-energy of its disk

Action of a finite-energy plane on any circle equals the $d\lambda$ -energy of its disk