Motivation

Fast finite-energy planes are the pseudoholomorphic planes in the symplectization of a contact $3$-manifold whose asymptotic winding is as small as possible; their projections are immersions transverse to the Reeb flow. They are the pages of the open book decompositions that give disk-like global surfaces of section for dynamically convex Reeb flows on $S^3$ (H. Hofer, K. Wysocki, E. Zehnder, Ann. of Math. 148, 1998). To build such a family one needs to know that sequences of fast planes do not degenerate. U. Hryniewicz proved this compactness under conditions on the periodic orbits of bounded period: nondegeneracy and Conley–Zehnder index at least $3$ (Fast finite-energy planes in symplectizations and applications, Theorem 2.2, arXiv:0812.4076). In his characterization of the orbits that bound disk-like global surfaces of section, this is Theorem 3.10 (arXiv:1105.2077).

This mission formalizes that compactness theorem for the symplectization of a strictly star-shaped hypersurface $S\subset\mathbb{R}^4$, following Hryniewicz 2012, §§ 2 and 4, and H. Hofer, K. Wysocki, E. Zehnder, Finite energy cylinders of small area (Ergodic Theory Dynam. Systems 22, 2002). It is the tenth mission in a series on symplectic field theory, and builds on the published definitions and results of the previous missions: finite-energy curves and their punctures, asymptotic operators, and the winding numbers $\mathrm{wind}_\pi$, $\mathrm{wind}_\infty$.

Setting

All objects are those of FiniteEnergyPlane_Setting, FiniteEnergyPlane_Asymptotics and FiniteEnergyPlane_Winding with $n=1$: a strictly star-shaped level $S=H^{-1}(1)\subset\mathbb{R}^4$ with Reeb field $R$ and contact planes $\xi$, a compatible complex structure $J$ on $\xi$, and finite-energy $\tilde J$-holomorphic curves in $\mathbb{R}\times S\cong\mathbb{R}^4\setminus\{0\}$, $y=e^{2a}x$.

• The sets $\Theta$ and $\Theta_L$ (Hryniewicz (7), (9)). For a periodic orbit $P$, a compact $K\subset\mathbb{R}^4\setminus\{0\}$ and $\gamma>0$, $\Theta(K,P)$ is the set of fast planes asymptotic to $P$ at $\infty$ with $u(0)\in K$ and $d\lambda$-energy $\gamma$ outside the closed unit disk. $\Theta_L(K,P)$ adds the lower bound $a\ge-L$.
• Orbit hypotheses. Every periodic orbit of period at most $T_P$ is nondegenerate and has Conley–Zehnder index at least $3$, where the index is the one of the HryniewiczCriterion setting. The number $\gamma$ is smaller than every such period and every gap between two distinct such periods.
• Compactness means sequential compactness in $C^\infty_{loc}(\mathbb{C},\mathbb{R}^4)$.

Formalization targets

Goal: compactness of fast planes (Hryniewicz 2012, Theorem 2.2 (2); Hryniewicz 2014, Theorem 3.10)

Under the orbit hypotheses, if $K$ does not meet the cylinder $\mathbb{R}\times x(\mathbb{R})$ over $P=(x,T_P)$, then $\Theta(K,P)$ is sequentially compact in $C^\infty_{loc}$. The orbit hypotheses have the form used by exists_transverse_disk_open_book_of_approx in the HryniewiczCriterion mission.

Milestones

1. Orbit families (Hryniewicz 2012 (6)). Under nondegeneracy, the periodic orbits of period at most $T$ form finitely many families, with a uniform $C^0$ gap between distinct families.
2. Small-area cylinders (Hryniewicz 2012 Lemma 4.11; Hofer–Wysocki–Zehnder 2002 Theorem 1.1). Long finite-energy cylinders with small $d\lambda$-area and loop action bounded below are $C^m$-close to periodic orbits away from their inner end.
3. Blow-up points (Corollaries 4.8–4.10). Sequences in $\Theta(K,P)$ have subsequences whose gradients blow up at most at finitely many points of the closed unit disk.
4. Negative punctures (Lemma 4.13). A negative nondegenerate puncture at a nondegenerate orbit with $\mu_{CZ}\ge3$ has $\mathrm{wind}_\infty\ge2$.
5. Index below three (Lemma 4.15). A punctured sphere with one positive puncture of $\mathrm{wind}_\infty\le1$ and at least one negative puncture has a negative end at an orbit with $\mu_{CZ}<3$.
6. Escape to $+\infty$ (Lemma 4.16). Planes with small $d\lambda$-area outside shrinking disks, loop action and $a$ bounded below have $a\to+\infty$ on compact subsets of $\mathbb{C}\setminus\{0\}$.
7. Winding on a circle. On a circle enclosing all punctures, the winding of $\pi\partial_sw$ equals $\mathrm{wind}_\infty(u,\infty)$ minus the indices of the zeros of $\pi\,du$ outside the circle.
8. Limits of fast planes (Lemma 4.17). After shifting, a subsequence converges on $\mathbb{C}\setminus\Gamma$; either $\inf a\to-\infty$ and $K$ meets $\mathbb{R}\times x(\mathbb{R})$, or the limit is a plane of $\Theta(K,P)$.
9. Compactness of $\Theta_L$ (Theorem 2.2 (1)). Every $\Theta_L(K,P)$ is sequentially compact.

Significance

The results. Compactness of fast planes is the analytic core of the existence of disk-like global surfaces of section: together with the Fredholm theory of fast planes it turns a single fast plane into an $S^1$-family of pages of an open book decomposition of $S^3$. It is used, for the planes asymptotic to a fixed unknotted orbit with self-linking number $-1$, in Hryniewicz's characterization of the binding orbits of such open books (Hryniewicz 2014, § 3). Milestones 2 and 5 are general facts about finite-energy curves in symplectizations and are used again in the analysis of families of fast planes and of the Bishop family.

Formalizing them. All results are classical and proved in the cited sources. Lemma 4.11 of Hryniewicz 2012 is stated there with references only; Theorem 1.1 of Hofer–Wysocki–Zehnder 2002 establishes a version of it. None of these results has been formalized in Lean or another interactive theorem prover, as far as a literature search shows; Mathlib has no pseudoholomorphic curves.

Difficulty

The theorem is a compactness statement for solutions of a nonlinear elliptic equation in a non-compact target, so it needs all the analysis of the previous missions: bounds on derivatives from energy, convergence in $C^\infty_{loc}$, and the asymptotic description of punctures. The limit must again be a fast plane with the same asymptotic orbit and the same normalizations, and the only input about the dynamics is the hypothesis on the orbits of bounded period. The statements mix three normalizations (the point $u(0)\in K$, the $d\lambda$-energy outside the unit disk, and the $\mathbb{R}$-shift of the target) with winding numbers measured in a global frame. Lemma 4.11 is not available in the literature in exactly the form stated by Hryniewicz.

Formalization scope

• Namespace FiniteEnergyPlane; the definition module FiniteEnergyPlane_Compactness imports FiniteEnergyPlane_Winding (previous mission).
• Dimension three ($n=1$, $S\subset\mathbb{R}^4$) for the sets of fast planes and the winding statements. Milestones 1, 2 and 6 are stated for $S\subset\mathbb{R}^{2n+2}$.
• Compact sets in the symplectization are compact $K\subset\mathbb{R}^4$ with $0\notin K$; the cylinder over an orbit is the cone over its image.
• No total infima: statements about $\inf a$ are written with explicit quantifiers.
• Not included. Embeddedness of limits of embedded fast planes (Hryniewicz's sets $\Lambda$, $\Lambda_L$) needs intersection theory and is left to a later mission, as are the Fredholm theory of fast planes and the Bishop family.

Contributions welcome: general lemmas on $C^\infty_{loc}$ convergence of finite-energy curves and on finite sets of blow-up points.

Selected references

• U. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. Amer. Math. Soc. 364 (2012), 1859–1931, §§ 2 and 4. https://arxiv.org/abs/0812.4076
• U. Hryniewicz, Systems of global surfaces of section for dynamically convex Reeb flows on the 3-sphere, J. Symplectic Geom. 12 (2014), Theorem 3.10. https://arxiv.org/abs/1105.2077
• H. Hofer, K. Wysocki, E. Zehnder, Finite energy cylinders of small area, Ergodic Theory Dynam. Systems 22 (2002), 1451–1486, Theorem 1.1. https://doi.org/10.1017/S0143385702001013
• H. Hofer, K. Wysocki, E. Zehnder, The dynamics on three-dimensional strictly convex energy surfaces, Ann. of Math. 148 (1998), 197–289.
• H. Hofer, K. Wysocki, E. Zehnder, Properties of pseudoholomorphic curves in symplectisations II: Embedding controls and algebraic invariants, Geom. Funct. Anal. 5 (1995), 270–328.