Definition module FiniteEnergyPlane_Fredholm (Def_FiniteEnergyPlane_Fredholm.lean)

The module contains three definitions, in the namespace FiniteEnergyPlane. They assume nothing about $H$, $J$, $P$, $K$ or $\gamma$: strict star-shapedness and compatibility (described in the setting below) are not part of these definitions, so the junk-value conventions below apply for arbitrary $H,J$.

1. Embedded plane (IsEmbeddedPlane). For any $n$ and any $u:\mathbb C\to V_n=\mathbb R^{2(n+1)}$: $u$ is an embedded plane if

• $u$ is injective on all of $\mathbb C$, and
• for every $z\in\mathbb C$ the real Fréchet derivative $Du(z):\mathbb C\to V_n$ is injective as a real-linear map.

The derivative is $0$ by convention at points where $u$ is not differentiable, and $0$ is not injective, so the second clause entails real differentiability at every point of $\mathbb C$. No properness, closedness of the image, or homeomorphism-onto-image condition is included, and no smoothness beyond this.

2. Shift (shiftA). For any $n$, any $c\in\mathbb R$ and any $u:\mathbb C\to V_n$, the map $\mathrm{shiftA}_c(u):\mathbb C\to V_n$ is

$$\mathrm{shiftA}_c(u)(z)=e^{2c}\,u(z),$$

pointwise scalar multiplication of the values by $e^{2c}$.

3. Set of embedded fast planes (embeddedFastPlaneSet). For $H:V_1\to\mathbb R$, $J:V_1\to\mathrm{End}_{\mathbb R}(V_1)$, a Reeb orbit $P$ of $H$, a subset $K\subseteq V_1$ and $\gamma\in\mathbb R$, this is the set of all $u:\mathbb C\to V_1$ such that

• $u$ is a fast plane for $H,J$ (defined below; this contains its own existential prime orbit $P'$, which is not tied to $P$ by this clause);
• $u$ has a nondegenerate end at $\infty$ asymptotic to the given $P$ (defined below, $\varepsilon=1$; $P$ is not assumed prime);
• $u(0)\in K$;
• $E_{d\lambda}(\{z:|z|>1\},u)=\mathrm{ofReal}(\gamma)$ in $[0,\infty]$, where $\mathrm{ofReal}(\gamma)=\gamma$ for $\gamma\ge0$ and $\mathrm{ofReal}(\gamma)=0$ for $\gamma<0$ (so for every $\gamma\le0$ this clause says the $d\lambda$-energy on $\{|z|>1\}$ equals $0$);
• $u$ is an embedded plane in the sense of item 1.

(The first four clauses are the imported set fastPlaneSet.) If $K=\varnothing$ the set is empty.

Setting and notation (unfolded from the imported definitions)

Space. $V_n=\mathbb R^{2(n+1)}$ (functions $\{0,\dots,2n+1\}\to\mathbb R$); the material below applies to item 3 and uses $V_1=\mathbb R^4$, with coordinates $y=(y_0,y_1,y_2,y_3)$; items 1 and 2 hold for any $V_n$, which also carries the sup norm. The norm on $V_1$ is the sup norm $\|y\|=\max_k|y_k|$; on $\mathbb C$ the norm is the modulus, so $B(z_0,\varepsilon)=\{z\in\mathbb C:|z-z_0|<\varepsilon\}$ is a Euclidean open disc. On $\mathbb C\times\mathbb C$ the norm is $\max(|z|,|\tau|)$. "Smooth" ($C^\infty$) means infinitely real-differentiable (not analytic).

Linear structure. $j_0(y)=(-y_1,\,y_0,\,-y_3,\,y_2)$; $\omega_0(u,v)=\langle j_0u,v\rangle=u_0v_1-u_1v_0+u_2v_3-u_3v_2$; the Liouville form $\lambda_x(v)=\tfrac12\,\omega_0(x,v)$.

Hamiltonian data. For $H:V_1\to\mathbb R$: $\nabla H(x)_k=dH_x(e_k)$; $X_H(x)=j_0\nabla H(x)$; the Reeb field $R(x)=\lambda_x(X_H(x))^{-1}\,X_H(x)$, with the convention $0^{-1}=0$ (so $R(x)=0$ when $\lambda_x(X_H(x))=0$). The energy surface is $\{H=1\}$.

Hypothesis "$H$ is a strictly star-shaped level" ($hH$): $H$ is $C^\infty$ on all of $V_1$; for every $u\ne0$ there is a unique $r>0$ with $H(ru)=1$; and $dH_x(x)>0$ for every $x$ with $H(x)=1$.

Contact plane. $v\in\xi_x$ means $\lambda_x(v)=0$ and $dH_x(v)=0$.

Hypothesis "$J$ is a compatible $\xi$-structure" ($hJ$): $J:V_1\to\mathrm{End}_{\mathbb R}(V_1)$ is $C^\infty$, and for every $x$ with $H(x)=1$ and all $v,w\in\xi_x$: $J(x)v\in\xi_x$, $J(x)J(x)v=-v$, $v\ne0\Rightarrow\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_x$, nor for $x\notin\{H=1\}$, beyond smoothness.

Radial coordinates. $\sigma(y)$ ("scaleToS") is a chosen $r>0$ with $H(ry)=1$ if such an $r$ exists, and the junk value $1$ otherwise (e.g. at $y=0$ when $H(0)\ne1$). Then $\mathrm{proj}(y)=\sigma(y)\,y$ and $a(y)=-\tfrac12\log\sigma(y)$.

Almost complex structure $\tilde J$ on $V_1$. For $y\in V_1$ put $x=\mathrm{proj}(y)$, $r=\sigma(y)$, and the real-linear functionals and map

$$\alpha(h)=\frac{r}{2\,dH_x(x)}\,dH_x(h),\qquad \beta(h)=r\,\lambda_x(h),\qquad w(h)=h-\alpha(h)\,2y-\beta(h)\,r^{-1}R(x).$$

Then

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

(Division by $0$ again yields $0$.)

Partial derivatives. For $f:\mathbb C\to F$ (real vector space), $\partial_sf(z)=Df(z)(1)$, $\partial_tf(z)=Df(z)(i)$, where $Df(z)$ is the real Fréchet derivative (equal to $0$ by convention where $f$ is not differentiable).

$\tilde J$-holomorphic on $U$: for each $z\in U$, $u$ is real-differentiable at $z$ and $\partial_su(z)+\tilde J(u(z))\,\partial_tu(z)=0$.

Energy. An admissible $\varphi:\mathbb R\to\mathbb R$ is $C^\infty$, monotone non-decreasing, with $0\le\varphi\le1$. With $a_u=a\circ u$ and $w_u=\mathrm{proj}\circ u$, the energy density is

$$e_\varphi(z)=\varphi'(a_u)\big(\partial_sa_u\,\lambda_{w_u}(\partial_tw_u)-\partial_ta_u\,\lambda_{w_u}(\partial_sw_u)\big)+\varphi(a_u)\,\omega_0(\partial_sw_u,\partial_tw_u)$$

(evaluated at $z$), and

$$E(U,u)=\sup_{\varphi\text{ admissible}}\int_U \max\big(e_\varphi(z),0\big)\,dz\in[0,\infty],$$

i.e. only the positive part of the density is integrated (Lebesgue measure on $\mathbb C$). The $d\lambda$-density is $\omega_0(\partial_sw_u,\partial_tw_u)$ and the $d\lambda$-energy is $E_{d\lambda}(U,u)=\int_U\max\big(\omega_0(\partial_sw_u,\partial_tw_u),0\big)\,dz\in[0,\infty]$.

Finite-energy curve on $U$ ($U\subseteq\mathbb C$): $u:\mathbb C\to V_1$ is $C^\infty$ on $U$, $u(z)\ne0$ for all $z\in U$, $u$ is $\tilde J$-holomorphic on $U$, and $E(U,u)<\infty$. (Nothing is required of $u$ outside $U$.)

Reeb orbit. A Reeb orbit $P$ of $H$ consists of $x_P:\mathbb R\to V_1$ and $T_P>0$ with $H(x_P(\tau))=1$, $x_P'(\tau)=R(x_P(\tau))$ for all $\tau$, and $x_P(\tau+T_P)=x_P(\tau)$ for all $\tau$ ($T_P$ is a period, not necessarily the minimal one). $P$ is prime if $x_P(\tau)\ne x_P(0)$ for all $0<\tau<T_P$.

Nondegenerate end at $\infty$ asymptotic to $P$ (with sign $\varepsilon=1$ and the chart $c_\infty(s,t)=e^{2\pi s}e^{2\pi i t}$): there exist $d,c\in\mathbb R$ and $b>0$ such that, uniformly in $t\in\mathbb R$ (i.e. for every $\delta>0$ there is $s_0$ with the bound for all $s\ge s_0$ and all $t\in\mathbb R$),

$$\big|a(u(c_\infty(s,t)))-T_Ps-d\big|\to0,\qquad e^{bs}\,\big\|\mathrm{proj}(u(c_\infty(s,t)))-x_P(T_Pt+c)\big\|\to0\quad(s\to\infty).$$

Loop winding. $f:\mathbb R\to\mathbb C$ has winding $k\in\mathbb Z$ if $f$ is continuous, $1$-periodic, nowhere zero, and there is a continuous $\theta:\mathbb R\to\mathbb R$ with $f(t)=|f(t)|e^{i\theta(t)}$ for all $t$ and $\theta(1)-\theta(0)=2\pi k$.

Zero index. $f:\mathbb C\to\mathbb C$ has a zero of index $k$ at $z_0$ if $f(z_0)=0$ and there is $r>0$ such that $f(z)\ne0$ for all $z$ in the closed disc $\overline B(z_0,r)$ with $z\ne z_0$, and for every $\rho\in(0,r)$ the loop $t\mapsto f(z_0+\rho e^{2\pi it})$ has winding $k$.

$\xi$-coordinates. For $x\in\mathbb R^4$ let $Q_1(x)=(-x_2,x_3,x_0,-x_1)$, $Q_2(x)=(x_3,x_2,-x_1,-x_0)$, $|x|$ the Euclidean norm, $\hat Q(x)=Q(x)-\dfrac{dH_x(Q(x))}{dH_x(x)}\,x$, $e_1(x)=|x|^{-1}\hat Q_2(x)$, $e_2(x)=|x|^{-1}\hat Q_1(x)$. Then $\xi\mathrm{coord}_x(v)=\omega_0(v,e_2(x))+i\,\omega_0(e_1(x),v)\in\mathbb C$. The $\xi$-projection is $\pi_\xi(x,v)=v-\lambda_x(v)\,R(x)$.

$\pi\,\partial_s$ map. With $w_u=\mathrm{proj}\circ u$: $\pi\partial_s u(z)=\xi\mathrm{coord}_{w_u(z)}\big(\pi_\xi(w_u(z),\partial_sw_u(z))\big)\in\mathbb C$.

$\mathrm{wind}_\pi(u)=0$ (with no punctures). The set $Z=\{z\in\mathbb C:\pi\partial_su(z)=0\}$ is finite, and there are integers $\mathrm{idx}(z)$, $z\in Z$, such that $\pi\partial_su$ has a zero of index $\mathrm{idx}(z)$ at each $z\in Z$ and $\sum_{z\in Z}\mathrm{idx}(z)=0$. (This is a condition on finiteness, isolation-with-index and the index sum; it does not by itself say $Z=\varnothing$.)

Fast plane. $u:\mathbb C\to V_1$ is a fast plane (for $H,J$) if: (i) $u$ is a finite-energy curve on all of $\mathbb C$; (ii) there exists a prime Reeb orbit $P'$ such that $u$ has a nondegenerate end at $\infty$ asymptotic to $P'$ (as above, $\varepsilon=1$); (iii) $\mathrm{wind}_\pi(u)=0$ in the sense just described.