Finite-stage KAM exclusions and persistence on the common survivor

Open

KAMMainCorrected.finiteStagePersistenceData

by Wenqian · Sep 6, 2026 · Mathlib c5ea003 (Lean v4.30.0)

almost-periodic-functionsinvariant-torikam-theorymeasure-theorysmall-divisors

Let $M$ satisfy the corrected persistence hypotheses, and fix $0<\xi\le\xi_*$ . Write $T=O_\xi$ , $U=\Omega_\xi$ , and $\Omega(y)=K_1^{\mathsf T}\nabla N(y)$ for the physical trim, its reduced-frequency domain, and the frequency chart.

There exist $\varepsilon_*>0$ , a rate $c:\mathbb R\to\mathbb R$ , a bound $b:\mathbb R\to[0,\infty]$ , and closed decreasing frequency sets $K_{\varepsilon,j}\subseteq\mathbb R^n$ for $j\in\mathbb N$ , such that $c(\varepsilon)\ge0$ for $0<\varepsilon\le\varepsilon_*$ and

c(\varepsilon)\longrightarrow0,\qquad b(\varepsilon)\longrightarrow0, \qquad \operatorname{vol}_n(U\setminus K_{\varepsilon,j})\le b(\varepsilon) \quad(0<\varepsilon\le\varepsilon_*,\ j\in\mathbb N).

Both limits are as $\varepsilon\downarrow0$ . For every such $\varepsilon$ , every $y\in T$ with $\Omega(y)\in\bigcap_jK_{\varepsilon,j}$ , and every associated nondegenerate averaged critical point $\phi$ , there exists an embedded torus satisfying the corrected target's full suspended invariance, shell analyticity, local symplectic conjugacy, and uniform $c(\varepsilon)$ -closeness requirements, including the external $\ell^1$ actions.

This intermediate statement keeps the finite-stage exclusion estimate uniform in the iteration index. It does not assume nonemptiness or an excluded-volume estimate for the infinite intersection. The KAM construction must use a common survivor for the mixed-frequency divisor and both normal-matrix determinant divisors.

Formalization Note This is an interface-level consequence to be proved from the corrected hypotheses using the source's iteration and finite-stage estimates, not a verbatim separately numbered theorem of the paper. The suspended torus predicates are exactly those already fixed by the parent theorem.

Preamble

import Definitions.Def_frame_2026_kam_interfaces
noncomputable section
open Filter MeasureTheory Set
open scoped Topology
open KAMInterfaces

Formal statement

theorem KAMMainCorrected.finiteStagePersistenceData {n m : ℕ} (M : Model n m)
    (hypotheses : CorrectedHypotheses M)
    (ξ : ℝ) (hξ : 0 < ξ) (hξtrim : ξ ≤ hypotheses.trimRadius) :
    ∃ epsilonStar : ℝ, 0 < epsilonStar ∧
    ∃ closenessRate : ℝ → ℝ,
      (∀ epsilon, 0 < epsilon → epsilon ≤ epsilonStar →
        0 ≤ closenessRate epsilon) ∧
      Tendsto closenessRate (𝓝[>] 0) (𝓝 0) ∧
    ∃ excludedBound : ℝ → ENNReal,
      Tendsto excludedBound (𝓝[>] 0) (𝓝 0) ∧
    ∃ stages : ℝ → ℕ → Set (Point n),
      ∀ epsilon, 0 < epsilon → epsilon ≤ epsilonStar →
        (∀ j, IsClosed (stages epsilon j)) ∧
        Antitone (stages epsilon) ∧
        (∀ j, volume
          (trimmedReducedFrequencyDomain M ξ \ stages epsilon j) ≤
            excludedBound epsilon) ∧
        ∀ y ∈ trimmedNondegenerateResonantSet M ξ,
          (∀ j, reducedFrequency M.frame
            (internalFrequency M.integrableHamiltonian) y ∈ stages epsilon j) →
          ∀ phi, IsAssociatedNondegenerateCritical M.perturbation phi y →
            ∃ embedding : TorusPoint n → SuspendedPhase (n + m),
              Topology.IsEmbedding embedding ∧
              IsRealAnalyticAlmostPeriodicSuspendedEmbedding
                M.spatialStructure embedding ∧
              IsSymplecticallyConjugateSuspendedEmbedding M y phi embedding ∧
              IsSuspendedHamiltonianInvariantTorus M epsilon y embedding ∧
              SuspendedCloseToUnperturbed
                M closenessRate epsilon y phi embedding := by sorry

Source

Yuan Zhang, Wen Si, Jianguo Si, Poincaré–Treshchev Mechanism in Integrable Hamiltonian Systems Under Almost-Periodic Perturbations, DCDS 52 (2026), 32–69, https://doi.org/10.3934/dcds.2026043. Intermediate formulation of Lemma 5.1, equations (48)–(54), Section 5.2, and Section 6 equations (55)–(60) and their summation (journal pp. 57–64; author manuscript pp. 26–33), under the corrected hypotheses of KAMMainCorrected.poincareTreshchevPersistence. The common retained sets include the three divisor families of Section 4.6. Author-uploaded full text: https://www.researchgate.net/publication/401352098_Poincare-Treshchev_mechanism_in_integrable_Hamiltonian_systems_under_almost-periodic_perturbations . Environment port of kptm's theorem 773a95d0-9bda-404e-9f6c-489b7470bc8d and accepted reduction 18ba15af-c2bb-45c5-842b-db46ed62d5d8, preserving the exact finite-stage statement and the mission's original Lean 4.30.0 interface.

View graph