Linearization of circle diffeomorphisms

DefinitionDiophantine numbers#✓fully proved

A real number \(\alpha\) is Diophantine when there are real numbers \(\gamma > 0\) and \(\tau \ge 0\) such that \(|\alpha - p/q| \ge \gamma / q^{2 + \tau}\) for every integer \(p\) and every integer \(q \ge 1\).

def IsDiophantine (α : ℝ) : Prop :=
  ∃ γ : ℝ, 0 < γ ∧ ∃ τ : ℝ, 0 ≤ τ ∧ ∀ p : ℤ, ∀ q : ℕ, 1 ≤ q →
    γ / (q : ℝ) ^ (2 + τ) ≤ |α - (p : ℝ) / (q : ℝ)|

Sources

• Hayman (2018), Problem 2.90; https://arxiv.org/abs/1809.07200.

Used by 1

Used byHerman's analytic linearization problem

StructureReal-analytic circle diffeomorphisms#✓fully proved

A real-analytic orientation-preserving diffeomorphism of the circle is given by a lift \(F : \mathbb{R} \to \mathbb{R}\) together with an inverse lift \(G : \mathbb{R} \to \mathbb{R}\), both real-analytic on all of \(\mathbb{R}\), such that for every real \(x\) we have \(F(x + 1) = F(x) + 1\), \(G(x + 1) = G(x) + 1\), \(G(F(x)) = x\) and \(F(G(x)) = x\), and \(F\) is strictly increasing.

structure AnalyticCircleDiffeo where
  toLift : ℝ → ℝ
  invLift : ℝ → ℝ
  analytic_to : AnalyticOn ℝ toLift Set.univ
  analytic_inv : AnalyticOn ℝ invLift Set.univ
  lift_periodic : ∀ x : ℝ, toLift (x + 1) = toLift x + 1
  inv_periodic : ∀ x : ℝ, invLift (x + 1) = invLift x + 1
  left_inv : ∀ x : ℝ, invLift (toLift x) = x
  right_inv : ∀ x : ℝ, toLift (invLift x) = x
  strictly_mono : StrictMono toLift

Sources

• Hayman (2018), Problem 2.90; https://arxiv.org/abs/1809.07200.

Used by 2

Used byHerman's analytic linearization problem · Analytic conjugacy to a rotation

DefinitionRotation number of a lift#✓fully proved

Let \(F : \mathbb{R} \to \mathbb{R}\) be a function, and for a natural number \(n\) write \(F^n\) for the \(n\)-th iterate of \(F\). Then \(F\) has rotation number \(\alpha \in \mathbb{R}\) when, for every real \(x\), \((F^n(x) - x)/n\) tends to \(\alpha\) as \(n\) tends to infinity.

def HasRotationNumber (F : ℝ → ℝ) (α : ℝ) : Prop :=
  ∀ x : ℝ, Filter.Tendsto (fun n : ℕ => (F^[n] x - x) / (n : ℝ)) Filter.atTop (nhds α)

Sources

• Hayman (2018), Problem 2.90; https://arxiv.org/abs/1809.07200.

Used by 1

Used byHerman's analytic linearization problem

DefinitionAnalytic conjugacy to a rotation#✓fully proved

A function \(F : \mathbb{R} \to \mathbb{R}\) is analytically conjugate to the rotation by \(\alpha \in \mathbb{R}\) when there is a real-analytic circle diffeomorphism with lift \(H\) such that \(H(F(x)) = H(x) + \alpha\) for every real \(x\).

def IsAnalyticallyConjugateToRotation (F : ℝ → ℝ) (α : ℝ) : Prop :=
  ∃ H : AnalyticCircleDiffeo, ∀ x : ℝ, H.toLift (F x) = H.toLift x + α

Sources

• Hayman (2018), Problem 2.90; https://arxiv.org/abs/1809.07200.

Uses 1 · Used by 1

Statement usesReal-analytic circle diffeomorphisms

Used byHerman's analytic linearization problem

DefinitionHerman's analytic linearization problem#✓fully proved

The statement that there is an irrational real number \(\alpha\) that is not Diophantine such that, for every real-analytic circle diffeomorphism whose lift \(F\) has rotation number \(\alpha\), \(F\) is analytically conjugate to the rotation by \(\alpha\).

M. R. Herman asked whether such an \(\alpha\) exists; this is Problem 2.90 in Hayman's list.

def conjecture : Prop :=
  ∃ α : ℝ, Irrational α ∧ ¬ IsDiophantine α ∧
    ∀ F : AnalyticCircleDiffeo, HasRotationNumber F.toLift α →
      IsAnalyticallyConjugateToRotation F.toLift α

Sources

• Hayman (2018), Problem 2.90; https://arxiv.org/abs/1809.07200.

Uses 4 · Used by 1

Statement usesReal-analytic circle diffeomorphisms · Rotation number of a lift · Analytic conjugacy to a rotation · Diophantine numbers

Used byHerman's analytic linearization problem has a positive answer

TheoremHerman's analytic linearization problem has a positive answer#●ready to prove

There is an irrational real number \(\alpha\) that is not Diophantine such that, for every real-analytic circle diffeomorphism whose lift \(F\) has rotation number \(\alpha\), \(F\) is analytically conjugate to the rotation by \(\alpha\).

Yoccoz characterized the Herman class \(\mathcal{H}\) of rotation numbers \(\alpha\) for which every real-analytic circle diffeomorphism with rotation number \(\alpha\) is analytically linearizable, and proved that \(\mathcal{H}\) strictly contains the set of Diophantine numbers; any \(\alpha\) in \(\mathcal{H}\) that is not Diophantine has the required property.

public theorem_wanted conjecture_holds : conjecture

Sources

• H. Eliasson, B. Fayad and R. Krikorian, Jean-Christophe Yoccoz and the theory of circle diffeomorphisms (2018), arXiv:1810.07107 (account of J.-C. Yoccoz, Analytic linearization of circle diffeomorphisms, Lecture Notes in Math. 1784, Springer (2002), 125-173), https://arxiv.org/abs/1810.07107.

Uses 1

Statement usesHerman's analytic linearization problem

5 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.