Circle dynamics

DefinitionTranslation number#

The translation number of a CircleDeg1Lift, \(τ(f)=\lim_{n→∞}\frac{f^n(x)-x}{n}\). We use an auxiliary sequence \frac{f^{2^n}(0)}{2^n} to define τ(f) because some proofs are simpler this way.

CircleDeg1Lift.translationNumber (f : CircleDeg1Lift) : ℝ
Sources
MathlibCircleDeg1Lift.translationNumber
Uses 2 · Used by 2
Statement usesBornology · Order
Used byTranslation number defines a homeomorphism up to semiconjugacy · Translation numbers define a group action up to semiconjugacy

TheoremTranslation numbers define a group action up to semiconjugacy#

Consider two actions f₁ f₂ : G →* CircleDeg1Lift of a group on the real line by lifts of orientation-preserving circle homeomorphisms. Suppose that for each g : G the homeomorphisms f₁ g and f₂ g have equal rotation numbers. Then there exists F : CircleDeg1Lift such that F * f₁ g = f₂ g * F for all g : G.

This is a version of Proposition 5.4 from [Étienne Ghys, Groupes d'homéomorphismes du cercle et cohomologie bornée][ghys87:groupes].

CircleDeg1Lift.semiconj_of_group_action_of_forall_translationNumber_eq.{u_1} {G : Type u_1}
  [Group G] (f₁ f₂ : G →* CircleDeg1Lift)
  (h : ∀ (g : G), (f₁ g).translationNumber = (f₂ g).translationNumber) :
  ∃ F, ∀ (g : G), Function.Semiconj ⇑F ⇑(f₁ g) ⇑(f₂ g)
Sources
MathlibCircleDeg1Lift.semiconj_of_group_action_of_forall_translationNumber_eq
Uses 12 · Used by 1
Statement usesGroup morphism · Translation number
Proof usesAssociative algebra over a commutative ring · Characteristic zero · Closure · Completeness of R · Field \(\Q\) of rational numbers · Hausdorff space · Metric structure · Squeeze theorem · Topological module · Topological ring
Used byTranslation number defines a homeomorphism up to semiconjugacy

TheoremTranslation number defines a homeomorphism up to semiconjugacy#

If two lifts of circle homeomorphisms have the same translation number, then they are semiconjugate by a CircleDeg1Lift. This version uses assumptions bijective f₁ and bijective f₂ to assume that f₁ and f₂ are homeomorphisms.

CircleDeg1Lift.semiconj_of_bijective_of_translationNumber_eq {f₁ f₂ : CircleDeg1Lift}
  (h₁ : Function.Bijective ⇑f₁) (h₂ : Function.Bijective ⇑f₂)
  (h : f₁.translationNumber = f₂.translationNumber) : ∃ F, Function.Semiconj ⇑F ⇑f₁ ⇑f₂
Sources
MathlibCircleDeg1Lift.semiconj_of_bijective_of_translationNumber_eq
Uses 2
Statement usesTranslation number
Proof usesTranslation numbers define a group action up to semiconjugacy

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.