mathlib documentation

dynamics.circle.rotation_number.translation_number

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 #

Main statements #

We prove the following properties of circle_deg1_lift.translation_number.

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:

References #

TODO #

Here are some short-term goals.

Tags #

circle homeomorphism, rotation number

Definition and monoid structure #

structure circle_deg1_lift  :
Type

A lift of a monotone degree one map S¹ → S¹.

Instances for circle_deg1_lift
@[simp]
theorem circle_deg1_lift.coe_mk (f : ) (h₁ : monotone f) (h₂ : ∀ (x : ), f (x + 1) = f x + 1) :
{to_fun := f, monotone' := h₁, map_add_one' := h₂} = f
theorem circle_deg1_lift.mono (f : circle_deg1_lift) {x y : } (h : x y) :
f x f y
@[simp]
theorem circle_deg1_lift.map_add_one (f : circle_deg1_lift) (x : ) :
f (x + 1) = f x + 1
@[simp]
theorem circle_deg1_lift.map_one_add (f : circle_deg1_lift) (x : ) :
f (1 + x) = 1 + f x
theorem circle_deg1_lift.coe_inj ⦃f g : circle_deg1_lift :
f = gf = g
@[ext]
theorem circle_deg1_lift.ext ⦃f g : circle_deg1_lift (h : ∀ (x : ), f x = g x) :
f = g
theorem circle_deg1_lift.ext_iff {f g : circle_deg1_lift} :
f = g ∀ (x : ), f x = g x
@[protected, instance]
Equations
@[simp]
theorem circle_deg1_lift.mul_apply (f g : circle_deg1_lift) (x : ) :
(f * g) x = f (g x)
@[simp]
@[simp, norm_cast]

If a lift of a circle map is bijective, then it is an order automorphism of the line.

Equations
theorem circle_deg1_lift.coe_pow (f : circle_deg1_lift) (n : ) :
(f ^ n) = (f^[n])

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

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.

@[simp]
theorem circle_deg1_lift.map_int_add (f : circle_deg1_lift) (m : ) (x : ) :
f (m + x) = m + f x
@[simp]
theorem circle_deg1_lift.map_add_int (f : circle_deg1_lift) (x : ) (m : ) :
f (x + m) = f x + m
@[simp]
theorem circle_deg1_lift.map_sub_int (f : circle_deg1_lift) (x : ) (n : ) :
f (x - n) = f x - n
@[simp]
theorem circle_deg1_lift.map_add_nat (f : circle_deg1_lift) (x : ) (n : ) :
f (x + n) = f x + n
@[simp]
theorem circle_deg1_lift.map_nat_add (f : circle_deg1_lift) (n : ) (x : ) :
f (n + x) = n + f x
@[simp]
theorem circle_deg1_lift.map_sub_nat (f : circle_deg1_lift) (x : ) (n : ) :
f (x - n) = f x - n

Pointwise order on circle maps #

@[protected, instance]

Monotone circle maps form a lattice with respect to the pointwise order

Equations
@[simp]
theorem circle_deg1_lift.sup_apply (f g : circle_deg1_lift) (x : ) :
(f g) x = linear_order.max (f x) (g x)
@[simp]
theorem circle_deg1_lift.inf_apply (f g : circle_deg1_lift) (x : ) :
(f g) x = linear_order.min (f x) (g x)
theorem circle_deg1_lift.iterate_mono {f g : circle_deg1_lift} (h : f g) (n : ) :
theorem circle_deg1_lift.pow_mono {f g : circle_deg1_lift} (h : f g) (n : ) :
f ^ n g ^ n

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.

theorem circle_deg1_lift.dist_map_zero_lt_of_semiconj_by {f g₁ g₂ : circle_deg1_lift} (h : semiconj_by f g₁ g₂) :
has_dist.dist (g₁ 0) (g₂ 0) < 2

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.

theorem circle_deg1_lift.iterate_le_of_map_le_add_int (f : circle_deg1_lift) {x : } {m : } (h : f x x + m) (n : ) :
f^[n] x x + n * m
theorem circle_deg1_lift.le_iterate_of_add_int_le_map (f : circle_deg1_lift) {x : } {m : } (h : x + m f x) (n : ) :
x + n * m f^[n] x
theorem circle_deg1_lift.iterate_eq_of_map_eq_add_int (f : circle_deg1_lift) {x : } {m : } (h : f x = x + m) (n : ) :
f^[n] x = x + n * m
theorem circle_deg1_lift.iterate_pos_le_iff (f : circle_deg1_lift) {x : } {m : } {n : } (hn : 0 < n) :
f^[n] x x + n * m f x x + m
theorem circle_deg1_lift.iterate_pos_lt_iff (f : circle_deg1_lift) {x : } {m : } {n : } (hn : 0 < n) :
f^[n] x < x + n * m f x < x + m
theorem circle_deg1_lift.iterate_pos_eq_iff (f : circle_deg1_lift) {x : } {m : } {n : } (hn : 0 < n) :
f^[n] x = x + n * m f x = x + m
theorem circle_deg1_lift.le_iterate_pos_iff (f : circle_deg1_lift) {x : } {m : } {n : } (hn : 0 < n) :
x + n * m f^[n] x x + m f x
theorem circle_deg1_lift.lt_iterate_pos_iff (f : circle_deg1_lift) {x : } {m : } {n : } (hn : 0 < n) :
x + n * m < f^[n] x x + m < f x

Definition of translation number #

noncomputable def circle_deg1_lift.transnum_aux_seq (f : circle_deg1_lift) (n : ) :

An auxiliary sequence used to define the translation number.

Equations

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
theorem circle_deg1_lift.tendsto_translation_number_of_dist_bounded_aux (f : circle_deg1_lift) (x : ) (C : ) (H : ∀ (n : ), has_dist.dist ((f ^ n) 0) (x n) C) :

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.

theorem circle_deg1_lift.translation_number_of_map_pow_eq_add_int (f : circle_deg1_lift) {x : } {n : } {m : } (h : (f ^ n) x = x + m) (hn : 0 < n) :

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.

theorem circle_deg1_lift.forall_map_sub_of_Icc (f : circle_deg1_lift) (P : → Prop) (h : ∀ (x : ), x set.Icc 0 1P (f x - x)) (x : ) :
P (f x - x)

If a predicate depends only on f x - x and holds for all 0 ≤ x ≤ 1, then it holds for all x.

If f is a continuous monotone map ℝ → ℝ, f (x + 1) = f x + 1, then there exists x such that f x = x + τ f.

theorem circle_deg1_lift.translation_number_eq_rat_iff (f : circle_deg1_lift) (hf : continuous f) {m : } {n : } (hn : 0 < n) :
f.translation_number = m / n ∃ (x : ), (f ^ n) x = x + m
theorem circle_deg1_lift.semiconj_of_group_action_of_forall_translation_number_eq {G : Type u_1} [group G] (f₁ f₂ : G →* circle_deg1_lift) (h : ∀ (g : G), (f₁ g).translation_number = (f₂ g).translation_number) :
∃ (F : circle_deg1_lift), ∀ (g : G), function.semiconj F (f₁ g) (f₂ g)

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.