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.
We chose to define translation number for a wider class of maps f : ℝ → ℝ 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.
Notation
We use a local notation τ for the translation number of f : circle_deg1_lift.
Tags
circle homeomorphism, rotation number
Definition and monoid structure
Equations
- circle_deg1_lift.has_coe_to_fun = {F := λ (_x : circle_deg1_lift), ℝ → ℝ, coe := circle_deg1_lift.to_fun}
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}
Equations
Equations
- circle_deg1_lift.units_has_coe_to_fun = {F := λ (_x : units circle_deg1_lift), ℝ → ℝ, coe := λ (f : units circle_deg1_lift), ⇑↑f}
Translate by a constant
The map y ↦ x + y as a circle_deg1_lift. More precisely, we define a homomorphism from
multiplicative ℝ to units 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 : ℝ), x.to_add + 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 : ℝ), 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 : ℝ), 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.
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.