Poincaré–Siegel linearisation theorem

poincare_siegel_linearisation — a formalization challenge from the lean-eval benchmark.

Notes

Siegel 1942: a holomorphic germ f near 0 with f 0 = 0 and multiplier λ = e^{2πiα} (α Diophantine) is locally analytically conjugate to z ↦ λz. The conjugating germ u satisfies u 0 = 0, u'(0) = 1, and f(u z) = u(λ z) near 0 (Schröder equation). The file ships an IsDiophantine predicate parameterised by an arbitrary exponent τ (∃ C, ∃ τ, ∀ p q ≠ 0, C / |q|^τ ≤ |α − p/q|); the constant-type / exponent-2 condition is the special case fixing τ = 2.

Formal statement

/-- **Poincaré–Siegel linearisation theorem.** If `α` is Diophantine,
`λ = e^{2πiα}`, and `f` is holomorphic near `0` with `f 0 = 0` and
`f'(0) = λ`, then there is a holomorphic germ `u` with `u 0 = 0`,
`u'(0) = 1`, and `f(u z) = u(λ z)` for `z` near `0`. -/
theorem 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) := by
  sorry

Informal solution sketch

Construct the formal Schröder series u(z) = ∑ uₙ zⁿ from the conjugacy equation f(u z) = u(λ z), giving the recursion (λⁿ − λ) uₙ = (lower-order polynomial in u_{<n} and f_{≥2}). An arithmetic condition on the rotation number is essential to control the small divisors (λⁿ − 1); the Diophantine hypothesis gives a polynomial lower bound |λⁿ − 1| ≥ c n^{-(τ−1)} that is summable against Cauchy estimates. Siegel's geometric majorant-series argument bounds u by an explicit analytic envelope of positive radius of convergence.

Source

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).

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: poincare_siegel
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.