Shell-analytic suspended Hamiltonian interfaces for corrected resonant KAM persistence

import Mathlib

/-!
# Concrete interfaces for almost-periodic resonant KAM persistence

The perturbation is represented by its Fourier coefficients in the external
almost-periodic angles and in the adapted internal angles.  The averaged
Hamiltonian, its critical points and Hessian, the canonical Hamiltonian vector
field, analytic almost-periodic embeddings, and the standard symplectic form
are definitions, not model-supplied predicates.

We use the suspended Hamiltonian

`H ε θ J x y = ⟨ω,J⟩ + N y + ε P θ x y ε`

on the genuine `ℓ¹` external-action phase space.  Invariance is stated in all
external and internal canonical coordinates.
-/

noncomputable section

namespace KAMInterfaces

open Filter MeasureTheory Set
open scoped BigOperators Topology Gradient

abbrev Point (d : ℕ) := Fin d → ℝ
abbrev ComplexPoint (d : ℕ) := Fin d → ℂ
abbrev LatticePoint (d : ℕ) := Fin d → ℤ
abbrev PhaseAngle (m : ℕ) := Fin m → Real.Angle
abbrev ExternalAngle := ℤ → Real.Angle
abbrev ExternalAction := lp (fun _ : ℤ => ℝ) 1
abbrev ComplexExternalAction := lp (fun _ : ℤ => ℂ) 1
abbrev TorusPoint (n : ℕ) := ExternalAngle × PhaseAngle n
abbrev FiniteMode := ℤ →₀ ℤ
abbrev CanonicalPhase (d : ℕ) := PhaseAngle d × Point d
abbrev PhaseVector (d : ℕ) := Point d × Point d
abbrev SuspendedPhase (d : ℕ) :=
  (ExternalAngle × ExternalAction) × CanonicalPhase d
abbrev ExternalCylinderVector := ℤ →₀ ℝ
abbrev SuspendedCylinderVector (d : ℕ) :=
  (ExternalCylinderVector × ExternalAction) × PhaseVector d
abbrev SuspendedPhaseVector (d : ℕ) :=
  ((ℤ → ℝ) × ExternalAction) × PhaseVector d

/-- Coordinatewise complexification of a real `ℓ¹` external action. -/
noncomputable def complexifyExternalAction
    (J : ExternalAction) : ComplexExternalAction :=
  ⟨fun j => (J j : ℂ), by
    apply memℓp_gen
    simpa using (lp.memℓp J).summable_of_one.norm⟩

/-- The canonical inclusion of a real finite-dimensional point in its
complexification. -/
def complexifyPoint {d : ℕ} (x : Point d) : ComplexPoint d :=
  fun i => (x i : ℂ)

/-- A genuine complex neighborhood of a real parameter set. -/
def complexTube {d : ℕ} (G : Set (Point d)) (radius : ℝ) : Set (ComplexPoint d) :=
  {z | ∃ y ∈ G, dist z (complexifyPoint y) < radius}

/-- A complex neighborhood of the real perturbation interval `[-1,1]`. -/
def complexEpsilonTube (radius : ℝ) : Set ℂ :=
  {z | ∃ epsilon ∈ Set.Icc (-1 : ℝ) 1, dist z (epsilon : ℂ) < radius}

/-- The elementary Fourier mode supported at one external frequency. -/
def unitMode (j : ℤ) : FiniteMode :=
  Finsupp.single j 1

/-- Pairing of a finite-support external mode with a real frequency vector. -/
def modePairing (k : FiniteMode) (ω : ℤ → ℝ) : ℝ :=
  k.sum fun j coefficient => (coefficient : ℝ) * ω j

/-- The external Fourier length. -/
def modeL1 (k : FiniteMode) : ℕ :=
  k.sum fun _ coefficient => coefficient.natAbs

/-- Pairing of a finite-dimensional integer mode with lifted angles. -/
def latticePairing {d : ℕ} (k : LatticePoint d) (x : Point d) : ℝ :=
  ∑ j, (k j : ℝ) * x j

/-- The finite-dimensional Fourier length. -/
def latticeL1 {d : ℕ} (k : LatticePoint d) : ℕ :=
  ∑ j, (k j).natAbs

/-- The source's concrete weight of a finite spatial set. -/
def spatialSetWeight (spatialExponent : ℝ) (A : Finset ℤ) : ℝ :=
  1 + ∑ j ∈ A,
    Real.rpow (Real.log (1 + (j.natAbs : ℝ))) spatialExponent

/-- A source spatial structure, including a chosen witness for the printed
minimum `[[k]] = min{[A] : supp k ⊆ A ∈ S}`.  The witness is constrained to
be a genuine minimizer, so it cannot change the small-divisor condition. -/
structure SpatialStructure where
  sets : Set (Finset ℤ)
  spatialExponent : ℝ
  spatialExponent_gt_two : 2 < spatialExponent
  covers : ∀ j : ℤ, ∃ A, A ∈ sets ∧ j ∈ A
  union_mem_of_intersects :
    ∀ {A B}, A ∈ sets → B ∈ sets → (A ∩ B).Nonempty → A ∪ B ∈ sets
  supportEnvelope : FiniteMode → Finset ℤ
  supportEnvelope_mem :
    ∀ k, (∃ A, A ∈ sets ∧ k.support ⊆ A) → supportEnvelope k ∈ sets
  support_subset_envelope :
    ∀ k, (∃ A, A ∈ sets ∧ k.support ⊆ A) → k.support ⊆ supportEnvelope k
  supportEnvelope_minimal :
    ∀ k, (∃ A, A ∈ sets ∧ k.support ⊆ A) →
      ∀ A, A ∈ sets → k.support ⊆ A →
        spatialSetWeight spatialExponent (supportEnvelope k) ≤
          spatialSetWeight spatialExponent A

/-- The modes `ℤ^ℤ_S` occurring in the source: finite modes whose support is
contained in a member of the spatial structure. -/
def SpatialStructure.IsAdmissible (S : SpatialStructure) (k : FiniteMode) : Prop :=
  ∃ A, A ∈ S.sets ∧ k.support ⊆ A

/-- Every elementary external mode is admissible, because a spatial structure
covers every lattice site.  Thus the nonresonance quantifier cannot be empty. -/
theorem SpatialStructure.unitMode_admissible (S : SpatialStructure) (j : ℤ) :
    S.IsAdmissible (unitMode j) := by
  rcases S.covers j with ⟨A, hA, hj⟩
  refine ⟨A, hA, ?_⟩
  intro i hi
  have hji : i = j := by simpa [unitMode] using hi
  rw [hji]; exact hj

/-- The source weight `[[k]]`, evaluated at the constrained minimizing shell. -/
def modeSpatialWeight (S : SpatialStructure) (k : FiniteMode) : ℝ :=
  spatialSetWeight S.spatialExponent (S.supportEnvelope k)

/-- The source's individual-site weight `[j]`, obtained from the constrained
minimum shell containing the unit mode at `j`. -/
def siteSpatialWeight (S : SpatialStructure) (j : ℤ) : ℝ :=
  modeSpatialWeight S (unitMode j)

/-- Weighted external actions from the source phase norm
`sum_j |J_j| exp(w[j])`. -/
def HasWeightedExternalAction (S : SpatialStructure) (w : ℝ)
    (J : ExternalAction) : Prop :=
  Summable fun j : ℤ => ‖J j‖ * Real.exp (w * siteSpatialWeight S j)

/-- Weighted summability for a complex `ℓ¹` action coefficient. -/
def HasWeightedComplexExternalAction (S : SpatialStructure) (w : ℝ)
    (J : ComplexExternalAction) : Prop :=
  Summable fun j : ℤ => ‖J j‖ * Real.exp (w * siteSpatialWeight S j)

/-- The actual weighted `ℓ¹` norm of a complex action coefficient.  Every use
below is paired with `HasWeightedComplexExternalAction`, so the `tsum` fallback
is excluded. -/
noncomputable def weightedComplexExternalActionNorm (S : SpatialStructure)
    (w : ℝ) (J : ComplexExternalAction) : ℝ :=
  ∑' j : ℤ, ‖J j‖ * Real.exp (w * siteSpatialWeight S j)

/-- The character of the infinite product torus associated to a finite mode. -/
def externalCharacter (k : FiniteMode) (θ : ExternalAngle) : ℂ :=
  k.prod fun j coefficient => ((θ j).toCircle : ℂ) ^ coefficient

/-- The character of a finite torus associated to an integer lattice point. -/
def finiteCharacter {d : ℕ} (k : LatticePoint d) (x : PhaseAngle d) : ℂ :=
  ∏ j, ((x j).toCircle : ℂ) ^ k j

/-- A subgroup of a free abelian group is primitive (saturated). -/
def IsPrimitive {d : ℕ} (g : AddSubgroup (LatticePoint d)) : Prop :=
  ∀ (q : ℕ), q ≠ 0 → ∀ z, q • z ∈ g → z ∈ g

/-- A primitive rank-`m` resonance lattice with a chosen unimodular frame. -/
structure ResonanceFrame (n m : ℕ) where
  g : AddSubgroup (LatticePoint (n + m))
  K₀ : Matrix (Fin (n + m)) (Fin (n + m)) ℤ
  det_one : K₀.det = 1
  generated_by_resonant_columns :
    g = AddSubgroup.closure
      (Set.range fun j : Fin m =>
        fun i : Fin (n + m) => K₀ i (Fin.natAdd n j))

/-- The complementary columns of a resonance frame. -/
def ResonanceFrame.K₁ {n m : ℕ} (K : ResonanceFrame n m) :
    Matrix (Fin (n + m)) (Fin n) ℤ :=
  fun i j => K.K₀ i (Fin.castAdd m j)

/-- The resonant columns of a resonance frame. -/
def ResonanceFrame.K₂ {n m : ℕ} (K : ResonanceFrame n m) :
    Matrix (Fin (n + m)) (Fin m) ℤ :=
  fun i j => K.K₀ i (Fin.natAdd n j)

/-- Lifted adapted angle coordinates `(ψ, φ) = K₀ᵀ x`. -/
def ResonanceFrame.adaptedLift {n m : ℕ} (K : ResonanceFrame n m)
    (x : Point (n + m)) : Point n × Point m :=
  (fun j => ∑ i, (K.K₁ i j : ℝ) * x i,
   fun j => ∑ i, (K.K₂ i j : ℝ) * x i)

/-- Adapted torus coordinates `(ψ, φ) = K₀ᵀ x`. -/
def ResonanceFrame.adaptedAngles {n m : ℕ} (K : ResonanceFrame n m)
    (x : PhaseAngle (n + m)) : PhaseAngle n × PhaseAngle m :=
  (fun j => ∑ i, (K.K₁ i j) • x i,
   fun j => ∑ i, (K.K₂ i j) • x i)

/-- Recover the original torus angle from `(ψ, φ)`.  Since `det K₀ = 1`,
`adjugate K₀` is its integer inverse. -/
def ResonanceFrame.originalAngles {n m : ℕ} (K : ResonanceFrame n m)
    (ψ : PhaseAngle n) (φ : PhaseAngle m) : PhaseAngle (n + m) :=
  let q : PhaseAngle (n + m) := Fin.append ψ φ
  fun i => ∑ a, (K.K₀.adjugate a i) • q a

/-- `K₁ᵀ` applied to the internal frequency. -/
def reducedFrequency {n m : ℕ} (K : ResonanceFrame n m)
    (internalFrequency : Point (n + m) → Point (n + m)) :
    Point (n + m) → Point n :=
  fun y j => ∑ i, (K.K₁ i j : ℝ) * internalFrequency y i

/-- The internal resonant surface `K₂ᵀ ∇N(y)=0`. -/
def resonantSet {n m : ℕ} (K : ResonanceFrame n m)
    (G : Set (Point (n + m)))
    (internalFrequency : Point (n + m) → Point (n + m)) :
    Set (Point (n + m)) :=
  {y | y ∈ G ∧
    ∀ j : Fin m,
      ∑ i, (K.K₂ i j : ℝ) * internalFrequency y i = 0}

/-- An analytic bijection with analytic inverse and a uniform lower Lipschitz
bound on the source. -/
def IsAnalyticDiffeomorphismOn {d e : ℕ}
    (f : Point d → Point e) (source : Set (Point d))
    (target : Set (Point e)) : Prop :=
  AnalyticOnNhd ℝ f source ∧
    Set.BijOn f source target ∧
    ∃ inverse : Point e → Point d,
      AnalyticOnNhd ℝ inverse target ∧
      Set.MapsTo inverse target source ∧
      (∀ x ∈ source, inverse (f x) = x) ∧
      (∀ z ∈ target, f (inverse z) = z) ∧
      ∃ twist : ℝ, 0 < twist ∧
        ∀ x ∈ source, ∀ y ∈ source,
          twist * dist x y ≤ dist (f x) (f y)

/-- Approximation-function conditions used in the small-divisor estimates. -/
structure ApproximationFunction where
  toFun : ℝ → ℝ
  one_le : ∀ t, 0 ≤ t → 1 ≤ toFun t
  monotone : MonotoneOn toFun (Set.Ici 0)
  at_zero : toFun 0 = 1
  ratio_antitone :
    AntitoneOn (fun t => Real.log (toFun t) / t) (Set.Ioi 0)
  subexponential :
    Tendsto (fun t => Real.log (toFun t) / t) atTop (𝓝 0)
  brjuno_integrable :
    MeasureTheory.IntegrableOn
      (fun t => Real.log (toFun t) / t ^ 2) (Set.Ioi 0)

instance : CoeFun ApproximationFunction (fun _ => ℝ → ℝ) :=
  ⟨ApproximationFunction.toFun⟩

/-- The source nonresonance condition, quantified over exactly the nonzero
external modes admitted by the spatial structure. -/
def StronglyNonresonant (S : SpatialStructure) (ω : ℤ → ℝ) (γ : ℝ)
    (Δ : ApproximationFunction) : Prop :=
  0 < γ ∧
    ∀ k : FiniteMode, k ≠ 0 → S.IsAdmissible k →
      |modePairing k ω| ≥
        γ / (Δ (modeSpatialWeight S k) * Δ (modeL1 k : ℝ))

/-- A Fourier mode of the perturbation in `(θ, ψ, φ)`. -/
abbrev PerturbationMode (n m : ℕ) :=
  FiniteMode × LatticePoint n × LatticePoint m

/-- Shell-indexed Fourier data for a perturbation.  The first index is the
spatial shell `A ∈ S`; it is deliberately not collapsed to the minimum-weight
support of the total Fourier mode.  Coefficients are defined on complex
parameter variables so that the source's complex-neighborhood analyticity can
be stated literally. -/
structure FourierPerturbation (n m : ℕ) where
  coefficient :
    Finset ℤ → PerturbationMode n m → ComplexPoint (n + m) → ℂ → ℂ

/-- Total Fourier length of a perturbation mode. -/
def perturbationModeL1 {n m : ℕ} (mode : PerturbationMode n m) : ℕ :=
  modeL1 mode.1 + latticeL1 mode.2.1 + latticeL1 mode.2.2

/-- Evaluation of the perturbation on real lifts of the torus angles. -/
def FourierPerturbation.evaluateLifted {n m : ℕ}
    (P : FourierPerturbation n m) (θ : ℤ → ℝ)
    (ψ : Point n) (φ : Point m) (y : Point (n + m)) (ε : ℝ) : ℝ :=
  (∑' shellMode : Finset ℤ × PerturbationMode n m,
    P.coefficient shellMode.1 shellMode.2 (complexifyPoint y) (ε : ℂ) *
      Complex.exp (Complex.I *
        (modePairing shellMode.2.1 θ + latticePairing shellMode.2.2.1 ψ +
          latticePairing shellMode.2.2.2 φ))).re

/-- The source's shell Banach class for a real analytic almost-periodic
perturbation.  A single bound for each shell controls the angular Fourier norm
uniformly throughout one complex neighborhood, and the spatially weighted sum
of those shell bounds is finite.  Keeping the shell index prevents replacing
`sum_A ‖P_A‖ exp(m[A])` by the weaker minimum-envelope norm of a collapsed
coefficient. -/
def FourierPerturbation.IsRealAnalyticAlmostPeriodicOn {n m : ℕ}
    (P : FourierPerturbation n m) (S : SpatialStructure)
    (G : Set (Point (n + m))) : Prop :=
  ∃ angleWidth spatialWidth parameterWidth : ℝ,
    0 < angleWidth ∧ 0 < spatialWidth ∧ 0 < parameterWidth ∧
    ∃ shellBound : Finset ℤ → ℝ,
    (∀ A, 0 ≤ shellBound A) ∧
    (∀ A, A ∉ S.sets → shellBound A = 0) ∧
    Summable (fun A : Finset ℤ =>
      shellBound A * Real.exp (spatialWidth * spatialSetWeight S.spatialExponent A)) ∧
    (∀ A mode,
      ¬ (A ∈ S.sets ∧ mode.1.support ⊆ A) →
        ∀ y ε, P.coefficient A mode y ε = 0) ∧
    (∀ A mode,
      DifferentiableOn ℂ
        (fun z : ComplexPoint (n + m) × ℂ =>
          P.coefficient A mode z.1 z.2)
        (complexTube G parameterWidth ×ˢ complexEpsilonTube parameterWidth)) ∧
    (∀ A mode, ∀ y ∈ complexTube G parameterWidth,
      ∀ ε ∈ complexEpsilonTube parameterWidth,
        ‖P.coefficient A mode y ε‖ *
          Real.exp (angleWidth * (perturbationModeL1 mode : ℝ)) ≤ shellBound A) ∧
    (∀ A, ∀ y ∈ complexTube G parameterWidth,
      ∀ ε ∈ complexEpsilonTube parameterWidth,
        Summable (fun mode : PerturbationMode n m =>
          ‖P.coefficient A mode y ε‖)) ∧
    (∀ A mode, ∀ y ∈ G, ∀ ε ∈ Set.Icc (-1 : ℝ) 1,
      P.coefficient A (-mode.1, -mode.2.1, -mode.2.2)
          (complexifyPoint y) (ε : ℂ) =
        star (P.coefficient A mode (complexifyPoint y) (ε : ℂ))) ∧
    /- Requiring analyticity of the actual uniformly convergent sum records the
    source's analytic shell function and prevents `fderiv` fallback. -/
    (∀ theta : ℤ → ℝ,
      AnalyticOnNhd ℝ
        (fun z : (Point n × Point m) × (Point (n + m) × ℝ) =>
          P.evaluateLifted theta z.1.1 z.1.2 z.2.1 z.2.2)
        ((Set.univ ×ˢ Set.univ) ×ˢ (G ×ˢ Set.Icc (-1 : ℝ) 1))) ∧
    /- The zero fast/external Fourier coefficient used for `h_0` is likewise
    required to be the actual analytic averaged potential. -/
    AnalyticOnNhd ℝ
      (fun z : Point m × Point (n + m) =>
        (∑' shellMode : Finset ℤ × LatticePoint m,
          P.coefficient shellMode.1 (0, 0, shellMode.2)
              (complexifyPoint z.2) 0 *
            Complex.exp (Complex.I * latticePairing shellMode.2 z.1)).re)
      (Set.univ ×ˢ G)

/-- The averaged perturbation `h₀(φ,y)`: the zero external and zero fast-angle
Fourier coefficient, evaluated at `ε = 0`. -/
def averagedPotentialLift {n m : ℕ} (P : FourierPerturbation n m)
    (φ : Point m) (y : Point (n + m)) : ℝ :=
  (∑' shellMode : Finset ℤ × LatticePoint m,
    P.coefficient shellMode.1 (0, 0, shellMode.2) (complexifyPoint y) 0 *
      Complex.exp (Complex.I * latticePairing shellMode.2 φ)).re

/-- A torus angle represented by its standard real representative. -/
def phaseAngleLift {m : ℕ} (φ : PhaseAngle m) : Point m :=
  fun j => (φ j).toReal

/-- Coordinate gradient on `ℝᵈ`, using the actual Fréchet derivative and the
standard coordinate vectors.  This avoids importing an inner product whose
norm would conflict with the product norm on `Fin d → ℝ`. -/
def coordinateGradient {d : ℕ} (f : Point d → ℝ) (x : Point d) : Point d :=
  fun j => fderiv ℝ f x (Pi.single j 1)

/-- Criticality of the explicitly averaged Hamiltonian. -/
def IsAveragedCritical {n m : ℕ} (P : FourierPerturbation n m)
    (φ : PhaseAngle m) (y : Point (n + m)) : Prop :=
  coordinateGradient (fun u : Point m => averagedPotentialLift P u y)
    (phaseAngleLift φ) = 0

/-- The Hessian matrix of the explicitly averaged Hamiltonian. -/
def averagedCriticalHessian {n m : ℕ} (P : FourierPerturbation n m)
    (φ : PhaseAngle m) (y : Point (n + m)) : Matrix (Fin m) (Fin m) ℝ :=
  let D := fderiv ℝ
    (fun u : Point m =>
      coordinateGradient (fun v : Point m => averagedPotentialLift P v y) u)
    (phaseAngleLift φ)
  fun i j => D (Pi.single j 1) i

/-- The internal frequency is the actual Euclidean gradient of `N`. -/
def internalFrequency {d : ℕ} (N : Point d → ℝ) : Point d → Point d :=
  coordinateGradient N

/-- Concrete data for one almost-periodically perturbed integrable Hamiltonian. -/
structure Model (n m : ℕ) where
  frame : ResonanceFrame n m
  parameterRegion : Set (Point (n + m))
  integrableHamiltonian : Point (n + m) → ℝ
  externalFrequency : ℤ → ℝ
  perturbation : FourierPerturbation n m
  approximation : ApproximationFunction
  divisorConstant : ℝ
  spatialStructure : SpatialStructure

/-- The perturbation evaluated in the original physical angles. -/
def Model.perturbationValue {n m : ℕ} (M : Model n m)
    (θ : ExternalAngle) (x : PhaseAngle (n + m))
    (y : Point (n + m)) (ε : ℝ) : ℝ :=
  let adapted := M.frame.adaptedLift (fun i => (x i).toReal)
  M.perturbation.evaluateLifted (fun j => (θ j).toReal)
    adapted.1 adapted.2 y ε

/-- The literal non-autonomous Hamiltonian `N + ε P`. -/
def Model.hamiltonian {n m : ℕ} (M : Model n m) (ε : ℝ)
    (θ : ExternalAngle) (z : CanonicalPhase (n + m)) : ℝ :=
  M.integrableHamiltonian z.2 + ε * M.perturbationValue θ z.1 z.2 ε

/-- The same Hamiltonian on real lifts of all angle variables. -/
def Model.hamiltonianLifted {n m : ℕ} (M : Model n m) (ε : ℝ)
    (θ : ℤ → ℝ) (z : Point (n + m) × Point (n + m)) : ℝ :=
  let adapted := M.frame.adaptedLift z.1
  M.integrableHamiltonian z.2 +
    ε * M.perturbation.evaluateLifted θ adapted.1 adapted.2 z.2 ε

/-- The canonical Hamiltonian vector field `(∂H/∂y, -∂H/∂x)`, computed on
real lifts of the physical angle torus. -/
def Model.hamiltonianVectorField {n m : ℕ} (M : Model n m) (ε : ℝ)
    (θ : ExternalAngle) (z : CanonicalPhase (n + m)) : PhaseVector (n + m) :=
  let θLift : ℤ → ℝ := fun j => (θ j).toReal
  let xLift : Point (n + m) := fun j => (z.1 j).toReal
  (coordinateGradient
      (fun y => M.hamiltonianLifted ε θLift (xLift, y)) z.2,
    -coordinateGradient
      (fun x => M.hamiltonianLifted ε θLift (x, z.2)) xLift)

/-- An associated nondegenerate relative equilibrium is an actual critical
point of the averaged perturbation with nonzero Hessian determinant. -/
def IsAssociatedNondegenerateCritical {n m : ℕ} (P : FourierPerturbation n m)
    (φ : PhaseAngle m) (y : Point (n + m)) : Prop :=
  IsAveragedCritical P φ y ∧ (averagedCriticalHessian P φ y).det ≠ 0

/-- The paper's set `O₀(g,G)` of resonant parameters which admit at least one
associated nondegenerate relative equilibrium. -/
def nondegenerateResonantSet {n m : ℕ} (M : Model n m) : Set (Point (n + m)) :=
  {y | y ∈ resonantSet M.frame M.parameterRegion
      (internalFrequency M.integrableHamiltonian) ∧
    ∃ φ, IsAssociatedNondegenerateCritical M.perturbation φ y}

/-- The reduced-frequency image of `O₀(g,G)`.  Boundary distance must be
measured in this `n`-dimensional chart: the ambient boundary of the resonant
surface in `ℝ^(n+m)` would contain the whole surface and make every positive
trim empty. -/
def nondegenerateReducedFrequencyDomain {n m : ℕ} (M : Model n m) :
    Set (Point n) :=
  reducedFrequency M.frame (internalFrequency M.integrableHamiltonian) ''
    nondegenerateResonantSet M

/-- The source trim in reduced-frequency coordinates. -/
def trimmedReducedFrequencyDomain {n m : ℕ} (M : Model n m) (ξ : ℝ) :
    Set (Point n) :=
  {Omega | Omega ∈ nondegenerateReducedFrequencyDomain M ∧
    ξ ≤ Metric.infDist Omega (frontier (nondegenerateReducedFrequencyDomain M))}

/-- Pullback of the reduced-frequency trim to the resonant parameter surface. -/
def trimmedNondegenerateResonantSet {n m : ℕ} (M : Model n m) (ξ : ℝ) :
    Set (Point (n + m)) :=
  {y | y ∈ nondegenerateResonantSet M ∧
    reducedFrequency M.frame (internalFrequency M.integrableHamiltonian) y ∈
      trimmedReducedFrequencyDomain M ξ}

/-- Corrected hypotheses for the concrete KAM target. -/
structure CorrectedHypotheses {n m : ℕ} (M : Model n m) where
  n_pos : 0 < n
  m_pos : 0 < m
  primitive : IsPrimitive M.frame.g
  parameterRegion_closed : IsClosed M.parameterRegion
  parameterRegion_bounded : Bornology.IsBounded M.parameterRegion
  integrableHamiltonian_analytic :
    AnalyticOnNhd ℝ M.integrableHamiltonian M.parameterRegion
  nondegenerate_resonant_nonempty : (nondegenerateResonantSet M).Nonempty
  trimRadius : ℝ
  trimRadius_pos : 0 < trimRadius
  trimmed_measurable :
    ∀ ξ, 0 < ξ → ξ ≤ trimRadius →
      MeasurableSet (trimmedNondegenerateResonantSet M ξ)
  trimmed_compact :
    ∀ ξ, 0 < ξ → ξ ≤ trimRadius →
      IsCompact (trimmedNondegenerateResonantSet M ξ)
  reduced_frequency_positive_measure :
    ∀ ξ, 0 < ξ → ξ ≤ trimRadius →
      0 < MeasureTheory.volume (trimmedReducedFrequencyDomain M ξ)
  /-- The missing Kolmogorov twist used verbatim in Lemma 3.2: because `K₀`
  is unimodular, injectivity of the full Hessian is equivalent to
  nonsingularity of `K₀ᵀ Hess(N) K₀`. -/
  integrableHamiltonian_twist_on_trimmed :
    ∀ ξ, 0 < ξ → ξ ≤ trimRadius →
      ∀ y ∈ trimmedNondegenerateResonantSet M ξ,
      Function.Injective
        (fderiv ℝ (internalFrequency M.integrableHamiltonian) y)
  reduced_frequency_diffeomorphism :
    ∀ ξ, 0 < ξ → ξ ≤ trimRadius →
      IsAnalyticDiffeomorphismOn
        (reducedFrequency M.frame (internalFrequency M.integrableHamiltonian))
        (trimmedNondegenerateResonantSet M ξ)
        (trimmedReducedFrequencyDomain M ξ)
  /-- Printed assumption (A1), restricted to the retained compact trim: every
  critical point which the conclusion quantifies over is nondegenerate.  On
  the compact critical locus analyticity then supplies the uniform gap used by
  one common `epsilonZero`; no numerical gap is inserted as separate data. -/
  all_retained_critical_points_nondegenerate :
    ∀ ξ, 0 < ξ → ξ ≤ trimRadius →
      ∀ y ∈ trimmedNondegenerateResonantSet M ξ, ∀ φ,
        IsAveragedCritical M.perturbation φ y →
          (averagedCriticalHessian M.perturbation φ y).det ≠ 0
  external_nonresonance :
    StronglyNonresonant M.spatialStructure M.externalFrequency
      M.divisorConstant M.approximation
  perturbation_analytic :
    M.perturbation.IsRealAnalyticAlmostPeriodicOn
      M.spatialStructure M.parameterRegion

/-- The rigid translation with external frequency `ω` and reduced internal
frequency `Ω`. -/
def torusTranslation {n : ℕ} (external : ℤ → ℝ)
    (internal : Point n) (t : ℝ) (q : TorusPoint n) : TorusPoint n :=
  (fun j => q.1 j + (t * external j : Real.Angle),
   fun j => q.2 j + (t * internal j : Real.Angle))

/-- The standard suspended resonant torus
`T^ℤ × Tⁿ(φ) × {J=0} × {y}` in the coordinates `(θ,J,x,y)`. -/
def standardSuspendedEmbedding {n m : ℕ} (M : Model n m)
    (y : Point (n + m)) (φ : PhaseAngle m)
    (q : TorusPoint n) : SuspendedPhase (n + m) :=
  ((q.1, 0), (M.frame.originalAngles q.2 φ, y))

/-- A Fourier mode for an almost-periodic torus embedding. -/
abbrev EmbeddingMode (n : ℕ) := FiniteMode × LatticePoint n

/-- Total length of an embedding Fourier mode. -/
def embeddingModeL1 {n : ℕ} (mode : EmbeddingMode n) : ℕ :=
  modeL1 mode.1 + latticeL1 mode.2

/-- One scalar coordinate has a source-style shell expansion at fixed analytic
widths.  Shell bounds are uniform in the torus variables and summable with the
actual `[A]` weight. -/
def HasShellFourierExpansion {n : ℕ} (S : SpatialStructure)
    (angleWidth spatialWidth : ℝ) (f : TorusPoint n → ℂ) : Prop :=
  ∃ coefficient : Finset ℤ → EmbeddingMode n → ℂ,
    ∃ shellBound : Finset ℤ → ℝ,
      (∀ A, 0 ≤ shellBound A) ∧
      (∀ A, A ∉ S.sets → shellBound A = 0) ∧
      Summable (fun A : Finset ℤ =>
        shellBound A *
          Real.exp (spatialWidth * spatialSetWeight S.spatialExponent A)) ∧
      (∀ A mode, ¬ (A ∈ S.sets ∧ mode.1.support ⊆ A) →
        coefficient A mode = 0) ∧
      (∀ A, Summable fun mode : EmbeddingMode n =>
        ‖coefficient A mode‖) ∧
      (∀ A mode,
        ‖coefficient A mode‖ *
          Real.exp (angleWidth * (embeddingModeL1 mode : ℝ)) ≤ shellBound A) ∧
      ∀ q,
        f q = ∑' shellMode : Finset ℤ × EmbeddingMode n,
          coefficient shellMode.1 shellMode.2 *
            externalCharacter shellMode.2.1 q.1 *
            finiteCharacter shellMode.2.2 q.2

/-- One unified weighted-`ℓ¹`-valued shell expansion for the full external
action component.  The coefficient majorant uses the source's inner supremum
norm, while the additional weighted absolute summability explicitly guards
the Banach-valued Fourier `tsum`. -/
def HasWeightedActionShellFourierExpansion {n : ℕ} (S : SpatialStructure)
    (angleWidth spatialWidth actionWeight : ℝ)
    (f : TorusPoint n → ExternalAction) : Prop :=
  ∃ coefficient : Finset ℤ → EmbeddingMode n → ComplexExternalAction,
    ∃ shellBound : Finset ℤ → ℝ,
      (∀ A, 0 ≤ shellBound A) ∧
      (∀ A, A ∉ S.sets → shellBound A = 0) ∧
      Summable (fun A : Finset ℤ =>
        shellBound A *
          Real.exp (spatialWidth * spatialSetWeight S.spatialExponent A)) ∧
      (∀ A mode, ¬ (A ∈ S.sets ∧ mode.1.support ⊆ A) →
        coefficient A mode = 0) ∧
      (∀ A mode,
        HasWeightedComplexExternalAction S actionWeight (coefficient A mode)) ∧
      (∀ A mode,
        weightedComplexExternalActionNorm S actionWeight (coefficient A mode) *
            Real.exp (angleWidth * (embeddingModeL1 mode : ℝ)) ≤
          shellBound A) ∧
      Summable (fun shellMode : Finset ℤ × EmbeddingMode n =>
        weightedComplexExternalActionNorm S actionWeight
          (coefficient shellMode.1 shellMode.2)) ∧
      (∀ q : TorusPoint n, Summable fun shellMode : Finset ℤ × EmbeddingMode n =>
        (externalCharacter shellMode.2.1 q.1 *
          finiteCharacter shellMode.2.2 q.2) •
            coefficient shellMode.1 shellMode.2) ∧
      (∀ q : TorusPoint n, HasWeightedExternalAction S actionWeight (f q)) ∧
      ∀ q : TorusPoint n,
        complexifyExternalAction (f q) =
          ∑' shellMode : Finset ℤ × EmbeddingMode n,
            (externalCharacter shellMode.2.1 q.1 *
              finiteCharacter shellMode.2.2 q.2) •
                coefficient shellMode.1 shellMode.2

/-- Every coordinate of the full suspended embedding has an actual
shell-indexed analytic almost-periodic expansion, including the external
angles and their conjugate actions. -/
def IsRealAnalyticAlmostPeriodicSuspendedEmbedding {n d : ℕ}
    (S : SpatialStructure) (ι : TorusPoint n → SuspendedPhase d) : Prop :=
  ∃ angleWidth spatialWidth actionWeight : ℝ,
    0 < angleWidth ∧ 0 < spatialWidth ∧
    0 ≤ actionWeight ∧ actionWeight < spatialWidth ∧
    (∀ j : ℤ, HasShellFourierExpansion S angleWidth spatialWidth
      (fun q => (((ι q).1.1 j).toCircle : ℂ))) ∧
    HasWeightedActionShellFourierExpansion S angleWidth spatialWidth actionWeight
      (fun q => (ι q).1.2) ∧
    (∀ i : Fin d, HasShellFourierExpansion S angleWidth spatialWidth
      (fun q => (((ι q).2.1 i).toCircle : ℂ))) ∧
    ∀ i : Fin d, HasShellFourierExpansion S angleWidth spatialWidth
      (fun q => ((ι q).2.2 i : ℂ))

/-- A line in the suspended phase in a finitely supported external direction
and an arbitrary finite-dimensional internal direction. -/
def suspendedCylinderPath {d : ℕ} (z : SuspendedPhase d)
    (v : SuspendedCylinderVector d) (t : ℝ) : SuspendedPhase d :=
  ((fun j => z.1.1 j + (t * v.1.1 j : Real.Angle),
    z.1.2 + t • v.1.2),
   (fun i => z.2.1 i + (t * v.2.1 i : Real.Angle),
    fun i => z.2.2 i + t * v.2.2 i))

/-- Coordinatewise derivative of a suspended transformation on cylinder
directions.  Circle derivatives recover angular velocities canonically. -/
noncomputable def suspendedTransformationTangent {d : ℕ}
    (F : SuspendedPhase d → SuspendedPhase d) (z : SuspendedPhase d)
    (v : SuspendedCylinderVector d) : SuspendedPhaseVector d :=
  let curve := fun t => F (suspendedCylinderPath z v t)
  let image := F z
  ((fun j =>
      (star (((image.1.1 j).toCircle : ℂ)) *
        deriv (fun t => (((curve t).1.1 j).toCircle : ℂ)) 0).im,
    deriv (fun t => (curve t).1.2) 0),
   (fun i =>
      (star (((image.2.1 i).toCircle : ℂ)) *
        deriv (fun t => (((curve t).2.1 i).toCircle : ℂ)) 0).im,
    deriv (fun t => (curve t).2.2) 0))

/-- The coordinate curves used above are genuinely differentiable, preventing
the total `deriv` operator from falling back to zero. -/
def CylinderDifferentiableOn {d : ℕ}
    (F : SuspendedPhase d → SuspendedPhase d) (U : Set (SuspendedPhase d)) : Prop :=
  ∀ z ∈ U, ∀ v : SuspendedCylinderVector d,
    (∀ j, DifferentiableAt ℝ
      (fun t => (((F (suspendedCylinderPath z v t)).1.1 j).toCircle : ℂ)) 0) ∧
    DifferentiableAt ℝ
      (fun t => (F (suspendedCylinderPath z v t)).1.2) 0 ∧
    (∀ i, DifferentiableAt ℝ
      (fun t => (((F (suspendedCylinderPath z v t)).2.1 i).toCircle : ℂ)) 0) ∧
    DifferentiableAt ℝ (fun t => (F (suspendedCylinderPath z v t)).2.2) 0

/-- Summability of the infinite external part of the canonical two-form. -/
def ExternalSymplecticSummable {d : ℕ}
    (u v : SuspendedPhaseVector d) : Prop :=
  Summable fun j : ℤ =>
    u.1.1 j * v.1.2 j - u.1.2 j * v.1.1 j

/-- The full suspended canonical form
`Σ dθⱼ∧dJⱼ + Σ dxᵢ∧dyᵢ`.  Every use below carries the explicit summability
guard for its infinite first series. -/
noncomputable def suspendedCanonicalSymplecticForm {d : ℕ}
    (u v : SuspendedPhaseVector d) : ℝ :=
  (∑' j : ℤ, (u.1.1 j * v.1.2 j - u.1.2 j * v.1.1 j)) +
    ∑ i, (u.2.1 i * v.2.2 i - u.2.2 i * v.2.1 i)

/-- Inclusion of cylinder directions into the ambient coordinate tangent. -/
def suspendedCylinderVectorToPhaseVector {d : ℕ}
    (v : SuspendedCylinderVector d) : SuspendedPhaseVector d :=
  ((fun j => v.1.1 j, v.1.2), v.2)

/-- A local change of suspended canonical coordinates with an actual inverse
on open source and target neighborhoods. -/
structure LocalSuspendedTransformation (d : ℕ) where
  source : Set (SuspendedPhase d)
  target : Set (SuspendedPhase d)
  source_open : IsOpen source
  target_open : IsOpen target
  toFun : SuspendedPhase d → SuspendedPhase d
  invFun : SuspendedPhase d → SuspendedPhase d
  mapsTo : Set.MapsTo toFun source target
  invMapsTo : Set.MapsTo invFun target source
  left_inverse : ∀ z ∈ source, invFun (toFun z) = z
  right_inverse : ∀ z ∈ target, toFun (invFun z) = z
  continuous_to : ContinuousOn toFun source
  continuous_inv : ContinuousOn invFun target

/-- Preservation of the full suspended canonical form on all cylinder
directions, by the derivative of the concrete local transformation. -/
def LocalSuspendedTransformation.IsSymplectic {d : ℕ}
    (F : LocalSuspendedTransformation d) : Prop :=
  CylinderDifferentiableOn F.toFun F.source ∧
    ∀ z ∈ F.source, ∀ u v : SuspendedCylinderVector d,
      ExternalSymplecticSummable
        (suspendedTransformationTangent F.toFun z u)
        (suspendedTransformationTangent F.toFun z v) ∧
      suspendedCanonicalSymplecticForm
          (suspendedTransformationTangent F.toFun z u)
          (suspendedTransformationTangent F.toFun z v) =
        suspendedCanonicalSymplecticForm
          (suspendedCylinderVectorToPhaseVector u)
          (suspendedCylinderVectorToPhaseVector v)

/-- The perturbed suspended torus is the image of the standard one under an
actual local symplectic coordinate change. -/
def IsSymplecticallyConjugateSuspendedEmbedding {n m : ℕ} (M : Model n m)
    (y : Point (n + m)) (φ : PhaseAngle m)
    (ι : TorusPoint n → SuspendedPhase (n + m)) : Prop :=
  ∃ F : LocalSuspendedTransformation (n + m),
    Set.range (standardSuspendedEmbedding M y φ) ⊆ F.source ∧
      F.IsSymplectic ∧
      (∀ z ∈ F.source, (F.toFun z).1.1 = z.1.1) ∧
      ∀ q, ι q = F.toFun (standardSuspendedEmbedding M y φ q)

/-- The formal suspended Hamiltonian
`⟨ω,J⟩ + N(y) + εP(θ,x,y,ε)`. -/
noncomputable def Model.suspendedHamiltonian {n m : ℕ} (M : Model n m) (ε : ℝ)
    (z : SuspendedPhase (n + m)) : ℝ :=
  (∑' j : ℤ, M.externalFrequency j * z.1.2 j) +
    M.hamiltonian ε z.1.1 z.2

/-- The formal external pairing is a genuine convergent series at this point. -/
def Model.SuspendedHamiltonianDefined {n m : ℕ} (M : Model n m)
    (z : SuspendedPhase (n + m)) : Prop :=
  Summable fun j : ℤ => M.externalFrequency j * z.1.2 j

/-- Vary one external angle along its standard circle coordinate. -/
def externalAngleLine (θ : ExternalAngle) (j : ℤ) (s : ℝ) : ExternalAngle :=
  fun k => θ k + (if k = j then (s : Real.Angle) else 0)

/-- The raw external-action component `-∂θ H`. -/
noncomputable def Model.externalActionVelocityRaw {n m : ℕ}
    (M : Model n m) (ε : ℝ) (z : SuspendedPhase (n + m)) : ℤ → ℝ :=
  fun j => -deriv
    (fun s => M.hamiltonian ε (externalAngleLine z.1.1 j s) z.2) 0

/-- The external-action velocity belongs to the source phase space `ℓ¹`. -/
def Model.ExternalActionVelocityDefined {n m : ℕ}
    (M : Model n m) (ε : ℝ) (z : SuspendedPhase (n + m)) : Prop :=
  Memℓp (M.externalActionVelocityRaw ε z) 1

/-- Package the actual external-action velocity in `ℓ¹`; every use in the
invariance predicate carries `ExternalActionVelocityDefined`, excluding the
fallback branch. -/
noncomputable def Model.externalActionVelocity {n m : ℕ}
    (M : Model n m) (ε : ℝ) (z : SuspendedPhase (n + m)) : ExternalAction :=
  by
    classical
    exact if h : M.ExternalActionVelocityDefined ε z then
      ⟨M.externalActionVelocityRaw ε z, h⟩
    else 0

/-- The canonical Hamiltonian vector field of the suspended Hamiltonian.  Its
external components are `θdot=ω` and `Jdot=-∂θ P`; the finite components are
the actual `(∂y H,-∂x H)` defined above. -/
noncomputable def Model.suspendedHamiltonianVectorField {n m : ℕ}
    (M : Model n m) (ε : ℝ) (z : SuspendedPhase (n + m)) :
    SuspendedPhaseVector (n + m) :=
  ((M.externalFrequency, M.externalActionVelocity ε z),
   M.hamiltonianVectorField ε z.1.1 z.2)

/-- The rigid almost-periodic orbit solves every coordinate of the concrete
suspended Hamilton equation. -/
def IsSuspendedHamiltonianInvariantTorus {n m : ℕ} (M : Model n m) (ε : ℝ)
    (y : Point (n + m))
    (ι : TorusPoint n → SuspendedPhase (n + m)) : Prop :=
  let Ω := reducedFrequency M.frame
    (internalFrequency M.integrableHamiltonian) y
  ∀ q t,
    let translated := torusTranslation M.externalFrequency Ω t q
    let z := ι translated
    let thetaLift : ℤ → ℝ := fun j => (z.1.1 j).toReal
    let xLift : Point (n + m) := fun j => (z.2.1 j).toReal
    let X := M.suspendedHamiltonianVectorField ε z
    M.SuspendedHamiltonianDefined z ∧
      M.ExternalActionVelocityDefined ε z ∧
      (∀ j, DifferentiableAt ℝ
        (fun s => M.hamiltonian ε (externalAngleLine z.1.1 j s) z.2) 0) ∧
      DifferentiableAt ℝ
        (fun y => M.hamiltonianLifted ε thetaLift (xLift, y)) z.2.2 ∧
      DifferentiableAt ℝ
        (fun x => M.hamiltonianLifted ε thetaLift (x, z.2.2)) xLift ∧
      (∀ j,
        HasDerivAt
          (fun s =>
            (((ι (torusTranslation M.externalFrequency Ω s q)).1.1 j).toCircle : ℂ))
          (Complex.I * (X.1.1 j : ℂ) * (((z.1.1 j).toCircle : ℂ))) t) ∧
      HasDerivAt
        (fun s => (ι (torusTranslation M.externalFrequency Ω s q)).1.2)
        X.1.2 t ∧
      (∀ j,
        HasDerivAt
          (fun s =>
            (((ι (torusTranslation M.externalFrequency Ω s q)).2.1 j).toCircle : ℂ))
          (Complex.I * (X.2.1 j : ℂ) * (((z.2.1 j).toCircle : ℂ))) t) ∧
      HasDerivAt
        (fun s => (ι (torusTranslation M.externalFrequency Ω s q)).2.2)
        X.2.2 t

/-- Coordinatewise uniform closeness of the full suspended torus to the
standard one, including the external actions omitted by a non-autonomous
physical-only formulation. -/
def SuspendedCloseToUnperturbed {n m : ℕ} (M : Model n m)
    (rate : ℝ → ℝ) (ε : ℝ) (y : Point (n + m)) (φ : PhaseAngle m)
    (ι : TorusPoint n → SuspendedPhase (n + m)) : Prop :=
  ∀ q,
    (∀ j, dist ((ι q).1.1 j) (q.1 j) ≤ rate ε) ∧
    ‖(ι q).1.2‖ ≤ rate ε ∧
    (∀ i, dist ((ι q).2.1 i) (M.frame.originalAngles q.2 φ i) ≤ rate ε) ∧
    ∀ i, |(ι q).2.2 i - y i| ≤ rate ε

end KAMInterfaces

/-! ## The complete corrected persistence proposition -/

namespace KAMMainCorrected

open Filter MeasureTheory Set
open scoped Topology
open KAMInterfaces

/-- Corrected headline persistence problem for the actual suspended
Hamiltonian `⟨ω,J⟩ + N + epsilon P`.  The radius `ξ` is quantified outside the
smallness threshold, exactly as in Theorem 2.7. -/
def PoincareTreshchevPersistenceProblem {n m : ℕ} (M : Model n m) : Prop :=
  ∀ hypotheses : CorrectedHypotheses M,
    ∀ ξ : ℝ, 0 < ξ → ξ ≤ hypotheses.trimRadius →
      ∃ epsilonZero : ℝ, 0 < epsilonZero ∧ epsilonZero ≤ 1 ∧
      ∃ closenessRate : ℝ → ℝ,
        (∀ epsilon, 0 < epsilon → epsilon ≤ epsilonZero →
          0 ≤ closenessRate epsilon) ∧
        Tendsto closenessRate (𝓝[>] 0) (𝓝 0) ∧
        ∃ Lambda : ℝ → Set (Point (n + m)),
          (∀ epsilon, 0 < epsilon → epsilon ≤ epsilonZero →
            IsClosed (Lambda epsilon) ∧
            MeasurableSet (Lambda epsilon) ∧
            (Lambda epsilon).Nonempty ∧
            Lambda epsilon ⊆ trimmedNondegenerateResonantSet M ξ) ∧
          Tendsto
            (fun epsilon => MeasureTheory.volume
              ((reducedFrequency M.frame
                (internalFrequency M.integrableHamiltonian)) ''
                (trimmedNondegenerateResonantSet M ξ \ Lambda epsilon)))
            (𝓝[>] 0) (𝓝 0) ∧
          ∀ epsilon, 0 < epsilon → epsilon ≤ epsilonZero →
            ∀ y ∈ Lambda epsilon, ∀ 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

end KAMMainCorrected