Translation number of a monotone real map that commutes with x ↦ x + 1
#
Let f : ℝ → ℝ
be a monotone map such that f (x + 1) = f x + 1
for all x
. Then the limit
$$
\tau(f)=\lim_{n\to\infty}{f^n(x)-x}{n}
$$
exists and does not depend on x
. This number is called the translation number of f
.
Different authors use different notation for this number: τ
, ρ
, rot
, etc
In this file we define a structure circle_deg1_lift
for bundled maps with these properties, define
translation number of f : circle_deg1_lift
, prove some estimates relating f^n(x)-x
to τ(f)
. In
case of a continuous map f
we also prove that f
admits a point x
such that f^n(x)=x+m
if and
only if τ(f)=m/n
.
Maps of this type naturally appear as lifts of orientation preserving circle homeomorphisms. More
precisely, let f
be an orientation preserving homeomorphism of the circle $S^1=ℝ/ℤ$, and
consider a real number a
such that
⟦a⟧ = f 0
, where ⟦⟧
means the natural projection ℝ → ℝ/ℤ
. Then there exists a unique
continuous function F : ℝ → ℝ
such that F 0 = a
and ⟦F x⟧ = f ⟦x⟧
for all x
(this fact is
not formalized yet). This function is strictly monotone, continuous, and satisfies
F (x + 1) = F x + 1
. The number ⟦τ F⟧ : ℝ / ℤ
is called the rotation number of f
.
It does not depend on the choice of a
.
Main definitions #
circle_deg1_lift
: a monotone mapf : ℝ → ℝ
such thatf (x + 1) = f x + 1
for allx
; the typecircle_deg1_lift
is equipped withlattice
andmonoid
structures; the multiplication is given by composition:(f * g) x = f (g x)
.circle_deg1_lift.translation_number
: translation number off : circle_deg1_lift
.
Main statements #
We prove the following properties of circle_deg1_lift.translation_number
.
-
circle_deg1_lift.translation_number_eq_of_dist_bounded
: if the distance between(f^n) 0
and(g^n) 0
is bounded from above uniformly inn : ℕ
, thenf
andg
have equal translation numbers. -
circle_deg1_lift.translation_number_eq_of_semiconj_by
: if twocircle_deg1_lift
mapsf
,g
are semiconjugate by acircle_deg1_lift
map, thenτ f = τ g
. -
circle_deg1_lift.translation_number_units_inv
: iff
is an invertiblecircle_deg1_lift
map (equivalently,f
is a lift of an orientation-preserving circle homeomorphism), then the translation number off⁻¹
is the negative of the translation number off
. -
circle_deg1_lift.translation_number_mul_of_commute
: iff
andg
commute, thenτ (f * g) = τ f + τ g
. -
circle_deg1_lift.translation_number_eq_rat_iff
: the translation number off
is equal to a rational numberm / n
if and only if(f^n) x = x + m
for somex
. -
circle_deg1_lift.semiconj_of_bijective_of_translation_number_eq
: iff
andg
are two bijectivecircle_deg1_lift
maps and their translation numbers are equal, then these maps are semiconjugate to each other. -
circle_deg1_lift.semiconj_of_group_action_of_forall_translation_number_eq
: letf₁
andf₂
be two actions of a groupG
on the circle by degree 1 maps (formally,f₁
andf₂
are two homomorphisms fromG →* circle_deg1_lift
). If the translation numbers off₁ g
andf₂ g
are equal to each other for allg : G
, then these two actions are semiconjugate by someF : circle_deg1_lift
. This is a version of Proposition 5.4 from Étienne Ghys, Groupes d'homeomorphismes du cercle et cohomologie bornee.
Notation #
We use a local notation τ
for the translation number of f : circle_deg1_lift
.
Implementation notes #
We define the translation number of f : circle_deg1_lift
to be the limit of the sequence
(f ^ (2 ^ n)) 0 / (2 ^ n)
, then prove that ((f ^ n) x - x) / n
tends to this number for any x
.
This way it is much easier to prove that the limit exists and basic properties of the limit.
We define translation number for a wider class of maps f : ℝ → ℝ
instead of lifts of orientation
preserving circle homeomorphisms for two reasons:
- non-strictly monotone circle self-maps with discontinuities naturally appear as Poincaré maps for some flows on the two-torus (e.g., one can take a constant flow and glue in a few Cherry cells);
- definition and some basic properties still work for this class.
References #
TODO #
Here are some short-term goals.
-
Introduce a structure or a typeclass for lifts of circle homeomorphisms. We use
units circle_deg1_lift
for now, but it's better to have a dedicated type (or a typeclass?). -
Prove that the
semiconj_by
relation on circle homeomorphisms is an equivalence relation. -
Introduce
conditionally_complete_lattice
structure, use it in the proof ofcircle_deg1_lift.semiconj_of_group_action_of_forall_translation_number_eq
. -
Prove that the orbits of the irrational rotation are dense in the circle. Deduce that a homeomorphism with an irrational rotation is semiconjugate to the corresponding irrational translation by a continuous
circle_deg1_lift
.
Tags #
circle homeomorphism, rotation number
Definition and monoid structure #
- to_fun : ℝ → ℝ
- monotone' : monotone self.to_fun
- map_add_one' : ∀ (x : ℝ), self.to_fun (x + 1) = self.to_fun x + 1
A lift of a monotone degree one map S¹ → S¹
.
Instances for circle_deg1_lift
- circle_deg1_lift.has_sizeof_inst
- circle_deg1_lift.has_coe_to_fun
- circle_deg1_lift.monoid
- circle_deg1_lift.inhabited
- circle_deg1_lift.lattice
Equations
Equations
- circle_deg1_lift.monoid = {mul := λ (f g : circle_deg1_lift), {to_fun := ⇑f ∘ ⇑g, monotone' := _, map_add_one' := _}, mul_assoc := circle_deg1_lift.monoid._proof_3, one := {to_fun := id ℝ, monotone' := _, map_add_one' := circle_deg1_lift.monoid._proof_4}, one_mul := circle_deg1_lift.monoid._proof_5, mul_one := circle_deg1_lift.monoid._proof_6, npow := npow_rec (mul_one_class.to_has_mul circle_deg1_lift), npow_zero' := circle_deg1_lift.monoid._proof_9, npow_succ' := circle_deg1_lift.monoid._proof_10}
Equations
Equations
- circle_deg1_lift.units_has_coe_to_fun = {coe := λ (f : circle_deg1_liftˣ), ⇑↑f}
If a lift of a circle map is bijective, then it is an order automorphism of the line.
Translate by a constant #
The map y ↦ x + y
as a circle_deg1_lift
. More precisely, we define a homomorphism from
multiplicative ℝ
to circle_deg1_liftˣ
, so the translation by x
is
translation (multiplicative.of_add x)
.
Equations
- circle_deg1_lift.translate = (units.map {to_fun := λ (x : multiplicative ℝ), {to_fun := λ (y : ℝ), ⇑multiplicative.to_add x + y, monotone' := _, map_add_one' := _}, map_one' := circle_deg1_lift.translate._proof_3, map_mul' := circle_deg1_lift.translate._proof_4}).comp to_units.to_monoid_hom
Commutativity with integer translations #
In this section we prove that f
commutes with translations by an integer number.
First we formulate these statements (for a natural or an integer number,
addition on the left or on the right, addition or subtraction) using function.commute
,
then reformulate as simp
lemmas map_int_add
etc.
Pointwise order on circle maps #
Monotone circle maps form a lattice with respect to the pointwise order
Equations
- circle_deg1_lift.lattice = {sup := λ (f g : circle_deg1_lift), {to_fun := λ (x : ℝ), linear_order.max (⇑f x) (⇑g x), monotone' := _, map_add_one' := _}, le := λ (f g : circle_deg1_lift), ∀ (x : ℝ), ⇑f x ≤ ⇑g x, lt := semilattice_sup.lt._default (λ (f g : circle_deg1_lift), ∀ (x : ℝ), ⇑f x ≤ ⇑g x), le_refl := circle_deg1_lift.lattice._proof_3, le_trans := circle_deg1_lift.lattice._proof_4, lt_iff_le_not_le := circle_deg1_lift.lattice._proof_5, le_antisymm := circle_deg1_lift.lattice._proof_6, le_sup_left := circle_deg1_lift.lattice._proof_7, le_sup_right := circle_deg1_lift.lattice._proof_8, sup_le := circle_deg1_lift.lattice._proof_9, inf := λ (f g : circle_deg1_lift), {to_fun := λ (x : ℝ), linear_order.min (⇑f x) (⇑g x), monotone' := _, map_add_one' := _}, inf_le_left := circle_deg1_lift.lattice._proof_12, inf_le_right := circle_deg1_lift.lattice._proof_13, le_inf := circle_deg1_lift.lattice._proof_14}
Estimates on (f * g) 0
#
We prove the estimates f 0 + ⌊g 0⌋ ≤ f (g 0) ≤ f 0 + ⌈g 0⌉
and some corollaries with added/removed
floors and ceils.
We also prove that for two semiconjugate maps g₁
, g₂
, the distance between g₁ 0
and g₂ 0
is less than two.
Limits at infinities and continuity #
Estimates on (f^n) x
#
If we know that f x
is ≤
/<
/≥
/>
/=
to x + m
, then we have a similar estimate on
f^[n] x
and x + n * m
.
For ≤
, ≥
, and =
we formulate both of
(implication) and iff
versions because implications
work for n = 0
. For <
and >
we formulate only iff
versions.
Definition of translation number #
An auxiliary sequence used to define the translation number.
The translation number of a circle_deg1_lift
, $τ(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.
Equations
For any x : ℝ
the sequence $\frac{f^n(x)-x}{n}$ tends to the translation number of f
.
In particular, this limit does not depend on x
.
If f x - x
is an integer number m
for some point x
, then τ f = m
.
On the circle this means that a map with a fixed point has rotation number zero.
If f^n x - x
, n > 0
, is an integer number m
for some point x
, then
τ f = m / n
. On the circle this means that a map with a periodic orbit has
a rational rotation number.
If f
is a continuous monotone map ℝ → ℝ
, f (x + 1) = f x + 1
, then there exists x
such that f x = x + τ f
.
Consider two actions f₁ f₂ : G →* circle_deg1_lift
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 : circle_deg1_lift
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'homeomorphismes du cercle et cohomologie bornee.
If two lifts of circle homeomorphisms have the same translation number, then they are
semiconjugate by a circle_deg1_lift
. This version uses arguments f₁ f₂ : circle_deg1_liftˣ
to assume that f₁
and f₂
are homeomorphisms.
If two lifts of circle homeomorphisms have the same translation number, then they are
semiconjugate by a circle_deg1_lift
. This version uses assumptions is_unit f₁
and is_unit f₂
to assume that f₁
and f₂
are homeomorphisms.
If two lifts of circle homeomorphisms have the same translation number, then they are
semiconjugate by a circle_deg1_lift
. This version uses assumptions bijective f₁
and
bijective f₂
to assume that f₁
and f₂
are homeomorphisms.