Poincaré–Siegel linearisation theorem

poincare_siegel_linearisation

Submitter: Kim Morrison.

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.

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

Informal solution: 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.

theorem declaration uses `sorry`poincare_siegel (α : ℝ) (_hα : LeanEval.ComplexAnalysis.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α:ℝ_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)
  sorryAll goals completed! 🐙

Solved by

Not yet solved.