KAM persistence of an invariant curve

kam_invariant_curve

Submitter: Kim Morrison.

Notes: Kolmogorov–Arnold–Moser for a twist map: for Diophantine α and real-analytic, 1-periodic, non-constant, mean-zero f, for small |c| the functional equation q(t+α)−2q(t)+q(t−α) = c·f(q(t)) has a smooth strictly increasing solution with q−id periodic — the c=0 invariant curve persists. The linearisation is non-invertible (small divisors), so the IFT fails and the Diophantine condition drives a Newton/Nash–Moser scheme. The trusted helper IsDiophantine is a non-hole. Mathlib has no KAM theory (no twist maps, invariant curves, small divisors, Nash–Moser). Candidate from §83 of the Knill survey.

Source: A. N. Kolmogorov (1954); V. I. Arnold (1963); J. Moser, *On invariant curves of area-preserving mappings of an annulus*, Nachr. Akad. Wiss. Göttingen (1962). Knill, *Some fundamental theorems in mathematics*, §83.

Informal solution: KAM via a Newton/Nash–Moser iteration with small-divisor control. Linearise the functional operator F(q) = q(·+α) − 2q + q(·−α) − c·f∘q at the approximate solution; the constant-coefficient part L u = u(·+α) − 2u + u(·−α) is diagonal in Fourier with symbol 2cos(2πnα) − 2, invertible off n = 0 with inverse bounded by the Diophantine estimate |2cos(2πnα)−2|⁻¹ ≲ |n|²/C. Run a quadratically-convergent Newton scheme on a scale of analyticity-shrinking norms (Cauchy estimates absorb the polynomial small-divisor loss), solving the cohomological equation at each step after projecting out the mean (using f mean-zero), and control the analyticity-width loss so the iteration converges for |c| < c₀ to a real-analytic q with q−id periodic and StrictMono.

theorem declaration uses `sorry`kam_invariant_curve (α : ℝ) (_hα : LeanEval.Dynamics.IsDiophantine α)
    (f : ℝ → ℝ)
    (_hf_analytic : AnalyticOnNhd ℝ f Set.univ)
    (_hf_per : Function.Periodic f 1)
    (_hf_nonconst : ¬ ∃ k : ℝ, ∀ x, f x = k)
    (_hf_mean : ∫ x in (0 : ℝ)..1, f x = 0) :
    ∃ c₀ : ℝ, 0 < c₀ ∧ ∀ c : ℝ, |c| < c₀ →
      ∃ q : ℝ → ℝ,
        ContDiff ℝ ∞ q ∧ StrictMono q ∧
        Function.Periodic (fun t => q t - t) 1 ∧
        ∀ t : ℝ, q (t + α) - 2 * q t + q (t - α) = c * f (q t) := byα:ℝ_hα:IsDiophantine αf:ℝ → ℝ_hf_analytic:AnalyticOnNhd ℝ f Set.univ_hf_per:Function.Periodic f 1_hf_nonconst:¬∃ k, ∀ (x : ℝ), f x = k_hf_mean:∫ (x : ℝ) in 0..1, f x = 0⊢ ∃ c₀,
  0 < c₀ ∧
    ∀ (c : ℝ),
      |c| < c₀ →
        ∃ q,
          ContDiff ℝ ∞ q ∧
            StrictMono q ∧
              Function.Periodic (fun t => q t - t) 1 ∧ ∀ (t : ℝ), q (t + α) - 2 * q t + q (t - α) = c * f (q t)
  sorryAll goals completed! 🐙

Solved by

Not yet solved.