Kolmogorov–Arnold–Moser theorem

DefinitionDiophantine number#✓fully proved

A real number \(\alpha\) is Diophantine (with exponent \(2\), as used in KAM theory) if there is \(C > 0\) such that \(C / q^2 \le |\alpha - p/q|\) for all integers \(p\) and \(q\) with \(q \neq 0\).

def IsDiophantine (α : ℝ) : Prop :=
  ∃ C : ℝ, 0 < C ∧ ∀ p q : ℤ, q ≠ 0 →
    C / (q : ℝ) ^ 2 ≤ |α - (p : ℝ) / (q : ℝ)|

Used by 1

Used byKAM theorem for twist maps (persistence of an invariant curve)

TheoremKAM theorem for twist maps (persistence of an invariant curve)#●ready to prove

Let \(\alpha\) be a Diophantine real number and let \(f : \mathbb{R} \to \mathbb{R}\) be real-analytic, \(1\)-periodic and not constant, with \(\int_0^1 f(x)\,dx = 0\). Then there is \(c_0 > 0\) such that for every real \(c\) with \(|c| < c_0\) there is a \(C^\infty\), strictly increasing function \(q : \mathbb{R} \to \mathbb{R}\) such that \(t \mapsto q(t) - t\) is \(1\)-periodic and, for every real \(t\),

\[q(t + \alpha) - 2q(t) + q(t - \alpha) = c\, f(q(t)).\]

public theorem_wanted kam_invariant_curve
    (α : ℝ) (_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)

Sources

• 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. Problem kam_invariant_curve of the lean-eval benchmark.

Uses 1

Statement usesDiophantine number

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.