Corrected Poincaré–Treshchev persistence under almost-periodic perturbations

Let $n,m$ be positive natural numbers and put $d=n+m$. Let $g\subset\mathbb Z^d$ be a primitive rank-$m$ subgroup equipped with a matrix $K_0=(K_1,K_2)\in\operatorname{Mat}_{d\times d}(\mathbb Z)$ of determinant $1$, whose last $m$ columns generate $g$ and whose first $n$ columns form the complementary block. Let $G\subset\mathbb R^d$ be bounded and closed, let $N:\mathbb R^d\to\mathbb R$ be real analytic on a neighborhood of $G$, and let $\omega=(\omega_j)_{j\in\mathbb Z}$ be a real external frequency vector.

Let $\mathcal S$ be a covering spatial structure of finite subsets of $\mathbb Z$, with exponent $\varrho>2$ and shell weight

$$[A]=1+\sum_{j\in A}\log^{\varrho}(1+|j|).$$

For a finitely supported integer mode $k$, call it admissible when $\operatorname{supp}k\subset A$ for some $A\in\mathcal S$, and let $[[k]]$ be the minimum $[A]$ among such shells. Let $\Delta:[0,\infty)\to[1,\infty)$ be nondecreasing, satisfy $\Delta(0)=1$, have $\log\Delta(t)/t$ nonincreasing on $(0,\infty)$ and tending to $0$ at infinity, and satisfy $\int_0^\infty\log\Delta(t)t^{-2}\,dt<\infty$. Assume that a constant $\gamma>0$ gives

$$\left|\sum_{j\in\mathbb Z}k_j\omega_j\right| \ge\frac{\gamma}{\Delta([[k]])\Delta(\sum_j|k_j|)}$$

for every nonzero admissible mode $k$.

Let $P(\theta,x,y,\epsilon)$ be the real perturbation specified by shell-indexed Fourier coefficients $P_{A,k,\widetilde k,\ell}(y,\epsilon)$, where $A\in\mathcal S$, $k$ is an admissible external mode, $\widetilde k\in\mathbb Z^n$, and $\ell\in\mathbb Z^m$. Assume the coefficients are holomorphic on one complex neighborhood of $G\times[-1,1]$, obey the reality symmetry, define the actual Fourier sum, and admit nonnegative bounds $B_A$ and positive widths $r,s$ such that

$$|P_{A,k,\widetilde k,\ell}(y,\epsilon)| e^{r(|k|_1+|\widetilde k|_1+|\ell|_1)}\le B_A, \qquad \sum_A B_Ae^{s[A]}<\infty.$$

Define the internal frequency $\nabla N(y)$ by the Fréchet derivative of $N$, and set

$$O(g,G)=\{y\in G:K_2^{\mathsf T}\nabla N(y)=0\}, \qquad \Omega(y)=K_1^{\mathsf T}\nabla N(y).$$

In the adapted angles $(\psi,\phi)=K_0^{\mathsf T}x$, let $h_0(\phi,y)$ be the zero external and zero $\psi$ Fourier coefficient of $P$ at $\epsilon=0$. Write

$$O_0=\left\{y\in O(g,G):\exists\phi\in\mathbb T^m, \ \nabla_\phi h_0(\phi,y)=0, \ \det D_\phi^2h_0(\phi,y)\ne0\right\}, \qquad \Omega_0=\Omega(O_0).$$

Assume $O_0$ is nonempty. Assume there is $\xi_*>0$ such that, for every $0<\xi\le\xi_*$, the sets

$$\Omega_\xi=\{\eta\in\Omega_0:\xi\le\operatorname{dist}(\eta,\partial\Omega_0)\}, \qquad O_\xi=\{y\in O_0:\Omega(y)\in\Omega_\xi\}$$

have the following properties: $O_\xi$ is measurable and compact; $\Omega_\xi$ has positive $n$-dimensional Lebesgue measure; $D(\nabla N)(y)$ is injective for every $y\in O_\xi$; $\Omega:O_\xi\to\Omega_\xi$ is an analytic bijection with analytic inverse and a constant $c_\xi>0$ satisfying $c_\xi|y-y'|\le|\Omega(y)-\Omega(y')|$; and every critical point $\phi$ of $h_0(\cdot,y)$ for $y\in O_\xi$ has nonzero Hessian determinant.

For the suspended Hamiltonian on $(\mathbb T^{\mathbb Z}\times\ell^1(\mathbb Z;\mathbb R))\times(\mathbb T^d\times\mathbb R^d)$,

$$\mathcal H_\epsilon(\theta,J,x,y)= \sum_{j\in\mathbb Z}\omega_jJ_j+N(y)+\epsilon P(\theta,x,y,\epsilon),$$

the following holds. For every $0<\xi\le\xi_*$ there exist $\epsilon_0\in(0,1]$, a function $c:(0,\epsilon_0]\to[0,\infty)$ with $c(\epsilon)\to0$ as $\epsilon\downarrow0$, and sets $\Lambda_\epsilon\subset\mathbb R^d$ such that, for every $0<\epsilon\le\epsilon_0$:

1. $\Lambda_\epsilon$ is closed, measurable, nonempty, and contained in $O_\xi$.

2. The excluded reduced-frequency volume tends to zero:

$$\operatorname{vol}_n\bigl(\Omega(O_\xi\setminus\Lambda_\epsilon)\bigr) \longrightarrow0\qquad(\epsilon\downarrow0).$$

3. For every $y\in\Lambda_\epsilon$ and every $\phi\in\mathbb T^m$ satisfying $\nabla_\phi h_0(\phi,y)=0$ and $\det D_\phi^2h_0(\phi,y)\ne0$, there is a topological embedding

$$\iota:\mathbb T^{\mathbb Z}\times\mathbb T^n \longrightarrow (\mathbb T^{\mathbb Z}\times\ell^1)\times (\mathbb T^d\times\mathbb R^d).$$

Every coordinate of $\iota$ has an actual shell-indexed analytic almost-periodic Fourier expansion, and its external-action component has one uniformly controlled weighted-$\ell^1$-valued expansion. The map $\iota$ is the image of the standard embedding

$$\iota_0(\theta,\psi)= \bigl((\theta,0),(K_0^{-\mathsf T}(\psi,\phi),y)\bigr)$$

under a local homeomorphism between open suspended-phase neighborhoods that fixes $\theta$, is differentiable in all canonical cylinder directions, and preserves $\sum_jd\theta_j\wedge dJ_j+\sum_i dx_i\wedge dy_i$ on those directions.

Along the rigid translation with frequency $(\omega,\Omega(y))$, every coordinate solves the actual canonical Hamilton equation:

$$\frac d{dt}\iota\bigl(q+t(\omega,\Omega(y))\bigr) =X_{\mathcal H_\epsilon}\!\left( \iota\bigl(q+t(\omega,\Omega(y))\bigr)\right).$$

The external pairing is convergent and the external action velocity belongs to $\ell^1$ along this torus. Finally, for every torus point, every external and internal angle coordinate is within $c(\epsilon)$ of $\iota_0$, the $\ell^1$ norm of the external action is at most $c(\epsilon)$, and every internal action coordinate is within $c(\epsilon)$ of $y$.

This is a corrected formal version of Theorem 2.7: the full twist and reduced-frequency diffeomorphism are explicit hypotheses rather than consequences hidden in the notation.

Formalization Note The parameter sets called “Cantor sets” in the paper are required here to be closed, measurable, nonempty, and asymptotically full in reduced-frequency volume; perfectness and total disconnectedness are not asserted. External-angle tangent directions are finitely supported, while external-action tangent directions range over all of $\ell^1$.

import Definitions.Def_frame_2026_kam_interfaces

noncomputable section

namespace KAMMainCorrected

open Filter MeasureTheory Set
open scoped Topology
open KAMInterfaces

variable {n m : ℕ}

theorem poincareTreshchevPersistence (M : Model n m) :
    PoincareTreshchevPersistenceProblem M := by sorry

end KAMMainCorrected