Siegel linearization theorem

DefinitionDiophantine real numbers#✓fully proved

A real number \(\alpha\) is Diophantine if there are real numbers \(C > 0\) and \(\tau\) such that \(C / |q|^{\tau} \le |\alpha - p/q|\) for all integers \(p\) and \(q\) with \(q \neq 0\).

Any such exponent \(\tau\) is at least \(2\), by Dirichlet's approximation theorem. A Diophantine \(\alpha\) is irrational, so \(e^{2\pi i \alpha}\) is not a root of unity.

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

Used by 1

Used byPoincaré–Siegel linearisation theorem

TheoremPoincaré–Siegel linearisation theorem#●ready to prove

Let \(\alpha\) be a Diophantine real number and let \(\lambda = e^{2\pi i \alpha}\). If \(f : \mathbb{C} \to \mathbb{C}\) is analytic at \(0\) with \(f(0) = 0\) and \(f'(0) = \lambda\), then there is a function \(u : \mathbb{C} \to \mathbb{C}\), analytic at \(0\) with \(u(0) = 0\) and \(u'(0) = 1\), such that \(f(u(z)) = u(\lambda z)\) for all \(z\) in some neighbourhood of \(0\).

public theorem_wanted poincare_siegel
    (α : ℝ) (_hα : IsDiophantine α)
    (lam : ℂ) (_hlam : lam = Complex.exp (2 * Real.pi * Complex.I * (α : ℂ)))
    (f : ℂ → ℂ) (_hf : AnalyticAt ℂ f 0) (_hf0 : f 0 = 0)
    (_hmult : deriv f 0 = lam) :
    ∃ u : ℂ → ℂ, AnalyticAt ℂ u 0 ∧ u 0 = 0 ∧ deriv u 0 = 1 ∧
      ∀ᶠ z in nhds (0 : ℂ), f (u z) = u (lam * z)

Sources

• C. L. Siegel, Iteration of analytic functions, Annals of Math. 43 (1942), 607-612. Earlier formal-power-series version: H. Poincaré thèse (1879). Listed as §83 (additional statement 1) in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem poincare_siegel_linearisation of the lean-eval benchmark.

Uses 1

Statement usesDiophantine real numbers

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.