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 CircleDeg1Lift for bundled maps with these properties, define translation number of f : CircleDeg1Lift, 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

• CircleDeg1Lift: a monotone map f : ℝ → ℝ such that f (x + 1) = f x + 1 for all x; the type CircleDeg1Lift is equipped with Lattice and Monoid structures; the multiplication is given by composition: (f * g) x = f (g x).
• CircleDeg1Lift.translationNumber: translation number of f : CircleDeg1Lift.

Main statements

We prove the following properties of CircleDeg1Lift.translationNumber.

• CircleDeg1Lift.translationNumber_eq_of_dist_bounded: if the distance between (f^n) 0 and (g^n) 0 is bounded from above uniformly in n : ℕ, then f and g have equal translation numbers.

• CircleDeg1Lift.translationNumber_eq_of_semiconjBy: if two CircleDeg1Lift maps f, g are semiconjugate by a CircleDeg1Lift map, then τ f = τ g.

• CircleDeg1Lift.translationNumber_units_inv: if f is an invertible CircleDeg1Lift map (equivalently, f is a lift of an orientation-preserving circle homeomorphism), then the translation number of f⁻¹ is the negative of the translation number of f.

• CircleDeg1Lift.translationNumber_mul_of_commute: if f and g commute, then τ (f * g) = τ f + τ g.

• CircleDeg1Lift.translationNumber_eq_rat_iff: the translation number of f is equal to a rational number m / n if and only if (f^n) x = x + m for some x.

• CircleDeg1Lift.semiconj_of_bijective_of_translationNumber_eq: if f and g are two bijective CircleDeg1Lift maps and their translation numbers are equal, then these maps are semiconjugate to each other.

• CircleDeg1Lift.semiconj_of_group_action_of_forall_translationNumber_eq: let f₁ and f₂ be two actions of a group G on the circle by degree 1 maps (formally, f₁ and f₂ are two homomorphisms from G →* CircleDeg1Lift). If the translation numbers of f₁ g and f₂ g are equal to each other for all g : G, then these two actions are semiconjugate by some F : CircleDeg1Lift. This is a version of Proposition 5.4 from [Étienne Ghys, Groupes d'homeomorphismes du cercle et cohomologie bornee][ghys87:groupes].

Notation

We use a local notation τ for the translation number of f : CircleDeg1Lift.

Implementation notes

We define the translation number of f : CircleDeg1Lift 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

• [Étienne Ghys, Groupes d'homeomorphismes du cercle et cohomologie bornee][ghys87:groupes]

TODO

Here are some short-term goals.

• Introduce a structure or a typeclass for lifts of circle homeomorphisms. We use Units CircleDeg1Lift for now, but it's better to have a dedicated type (or a typeclass?).

• Prove that the SemiconjBy relation on circle homeomorphisms is an equivalence relation.

• Introduce ConditionallyCompleteLattice structure, use it in the proof of CircleDeg1Lift.semiconj_of_group_action_of_forall_translationNumber_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 CircleDeg1Lift.

Tags

circle homeomorphism, rotation number

Definition and monoid structure

structure CircleDeg1Liftextends OrderHom : Type

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

• toFun : ℝ → ℝ
• monotone' : Monotone self.toFun
• map_add_one' : ∀ (x : ℝ), self.toOrderHom.toFun (x + 1) = self.toOrderHom.toFun x + 1

instance CircleDeg1Lift.instFunLikeCircleDeg1LiftReal : FunLike CircleDeg1Lift ℝ ℝ

Equations

• CircleDeg1Lift.instFunLikeCircleDeg1LiftReal = { coe := fun (f : CircleDeg1Lift) => f.toFun, coe_injective' := CircleDeg1Lift.instFunLikeCircleDeg1LiftReal.proof_1 }

instance CircleDeg1Lift.instOrderHomClassCircleDeg1LiftRealInstLERealInstFunLikeCircleDeg1LiftReal : OrderHomClass CircleDeg1Lift ℝ ℝ

Equations

• CircleDeg1Lift.instOrderHomClassCircleDeg1LiftRealInstLERealInstFunLikeCircleDeg1LiftReal = (_ : RelHomClass CircleDeg1Lift (fun (x x_1 : ℝ) => x ≤ x_1) fun (x x_1 : ℝ) => x ≤ x_1)

@[simp]

theorem CircleDeg1Lift.coe_mk (f : ℝ →o ℝ) (h : ∀ (x : ℝ), f.toFun (x + 1) = f.toFun x + 1) : ⇑{ toOrderHom := f, map_add_one' := h } = ⇑f

@[simp]

theorem CircleDeg1Lift.coe_toOrderHom (f : CircleDeg1Lift) : ⇑f.toOrderHom = ⇑f

theorem CircleDeg1Lift.monotone (f : CircleDeg1Lift) : Monotone ⇑f

theorem CircleDeg1Lift.mono (f : CircleDeg1Lift) {x : ℝ} {y : ℝ} (h : x ≤ y) : f x ≤ f y

theorem CircleDeg1Lift.strictMono_iff_injective (f : CircleDeg1Lift) : StrictMono ⇑f ↔ Function.Injective ⇑f

@[simp]

theorem CircleDeg1Lift.map_add_one (f : CircleDeg1Lift) (x : ℝ) : f (x + 1) = f x + 1

@[simp]

theorem CircleDeg1Lift.map_one_add (f : CircleDeg1Lift) (x : ℝ) : f (1 + x) = 1 + f x

theorem CircleDeg1Lift.ext ⦃f : CircleDeg1Lift⦄ ⦃g : CircleDeg1Lift⦄ (h : ∀ (x : ℝ), f x = g x) : f = g

theorem CircleDeg1Lift.ext_iff {f : CircleDeg1Lift} {g : CircleDeg1Lift} : f = g ↔ ∀ (x : ℝ), f x = g x

instance CircleDeg1Lift.instMonoidCircleDeg1Lift : Monoid CircleDeg1Lift

Equations

• CircleDeg1Lift.instMonoidCircleDeg1Lift = Monoid.mk CircleDeg1Lift.instMonoidCircleDeg1Lift.proof_4 CircleDeg1Lift.instMonoidCircleDeg1Lift.proof_5 npowRec

instance CircleDeg1Lift.instInhabitedCircleDeg1Lift : Inhabited CircleDeg1Lift

Equations

• CircleDeg1Lift.instInhabitedCircleDeg1Lift = { default := 1 }

@[simp]

theorem CircleDeg1Lift.coe_mul (f : CircleDeg1Lift) (g : CircleDeg1Lift) : ⇑(f * g) = ⇑f ∘ ⇑g

theorem CircleDeg1Lift.mul_apply (f : CircleDeg1Lift) (g : CircleDeg1Lift) (x : ℝ) : (f * g) x = f (g x)

@[simp]

theorem CircleDeg1Lift.coe_one : ⇑1 = id

instance CircleDeg1Lift.unitsHasCoeToFun : CoeFun CircleDeg1Liftˣ fun (x : CircleDeg1Liftˣ) => ℝ → ℝ

Equations

• CircleDeg1Lift.unitsHasCoeToFun = { coe := fun (f : CircleDeg1Liftˣ) => ⇑↑f }

@[simp]

theorem CircleDeg1Lift.units_inv_apply_apply (f : CircleDeg1Liftˣ) (x : ℝ) : ↑f⁻¹ (↑f x) = x

@[simp]

theorem CircleDeg1Lift.units_apply_inv_apply (f : CircleDeg1Liftˣ) (x : ℝ) : ↑f (↑f⁻¹ x) = x

def CircleDeg1Lift.toOrderIso : CircleDeg1Liftˣ →* ℝ ≃o ℝ

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CircleDeg1Lift.coe_toOrderIso (f : CircleDeg1Liftˣ) : ⇑(CircleDeg1Lift.toOrderIso f) = ⇑↑f

@[simp]

theorem CircleDeg1Lift.coe_toOrderIso_symm (f : CircleDeg1Liftˣ) : ⇑(OrderIso.symm (CircleDeg1Lift.toOrderIso f)) = ⇑↑f⁻¹

@[simp]

theorem CircleDeg1Lift.coe_toOrderIso_inv (f : CircleDeg1Liftˣ) : ⇑(CircleDeg1Lift.toOrderIso f)⁻¹ = ⇑↑f⁻¹

theorem CircleDeg1Lift.isUnit_iff_bijective {f : CircleDeg1Lift} : IsUnit f ↔ Function.Bijective ⇑f

theorem CircleDeg1Lift.coe_pow (f : CircleDeg1Lift) (n : ℕ) : ⇑(f ^ n) = (⇑f)^[n]

theorem CircleDeg1Lift.semiconjBy_iff_semiconj {f : CircleDeg1Lift} {g₁ : CircleDeg1Lift} {g₂ : CircleDeg1Lift} : SemiconjBy f g₁ g₂ ↔ Function.Semiconj ⇑f ⇑g₁ ⇑g₂

theorem CircleDeg1Lift.commute_iff_commute {f : CircleDeg1Lift} {g : CircleDeg1Lift} : Commute f g ↔ Function.Commute ⇑f ⇑g

Translate by a constant

def CircleDeg1Lift.translate : Multiplicative ℝ →* CircleDeg1Liftˣ

The map y ↦ x + y as a CircleDeg1Lift. More precisely, we define a homomorphism from Multiplicative ℝ to CircleDeg1Liftˣ, so the translation by x is translation (Multiplicative.ofAdd x).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CircleDeg1Lift.translate_apply (x : ℝ) (y : ℝ) : ↑(CircleDeg1Lift.translate (Multiplicative.ofAdd x)) y = x + y

@[simp]

theorem CircleDeg1Lift.translate_inv_apply (x : ℝ) (y : ℝ) : ↑(CircleDeg1Lift.translate (Multiplicative.ofAdd x))⁻¹ y = -x + y

@[simp]

theorem CircleDeg1Lift.translate_zpow (x : ℝ) (n : ℤ) : CircleDeg1Lift.translate (Multiplicative.ofAdd x) ^ n = CircleDeg1Lift.translate (Multiplicative.ofAdd (↑n * x))

@[simp]

theorem CircleDeg1Lift.translate_pow (x : ℝ) (n : ℕ) : CircleDeg1Lift.translate (Multiplicative.ofAdd x) ^ n = CircleDeg1Lift.translate (Multiplicative.ofAdd (↑n * x))

@[simp]

theorem CircleDeg1Lift.translate_iterate (x : ℝ) (n : ℕ) : (⇑↑(CircleDeg1Lift.translate (Multiplicative.ofAdd x)))^[n] = ⇑↑(CircleDeg1Lift.translate (Multiplicative.ofAdd (↑n * x)))

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.

theorem CircleDeg1Lift.commute_nat_add (f : CircleDeg1Lift) (n : ℕ) : Function.Commute ⇑f fun (x : ℝ) => ↑n + x

theorem CircleDeg1Lift.commute_add_nat (f : CircleDeg1Lift) (n : ℕ) : Function.Commute ⇑f fun (x : ℝ) => x + ↑n

theorem CircleDeg1Lift.commute_sub_nat (f : CircleDeg1Lift) (n : ℕ) : Function.Commute ⇑f fun (x : ℝ) => x - ↑n

theorem CircleDeg1Lift.commute_add_int (f : CircleDeg1Lift) (n : ℤ) : Function.Commute ⇑f fun (x : ℝ) => x + ↑n

theorem CircleDeg1Lift.commute_int_add (f : CircleDeg1Lift) (n : ℤ) : Function.Commute ⇑f fun (x : ℝ) => ↑n + x

theorem CircleDeg1Lift.commute_sub_int (f : CircleDeg1Lift) (n : ℤ) : Function.Commute ⇑f fun (x : ℝ) => x - ↑n

@[simp]

theorem CircleDeg1Lift.map_int_add (f : CircleDeg1Lift) (m : ℤ) (x : ℝ) : f (↑m + x) = ↑m + f x

@[simp]

theorem CircleDeg1Lift.map_add_int (f : CircleDeg1Lift) (x : ℝ) (m : ℤ) : f (x + ↑m) = f x + ↑m

@[simp]

theorem CircleDeg1Lift.map_sub_int (f : CircleDeg1Lift) (x : ℝ) (n : ℤ) : f (x - ↑n) = f x - ↑n

@[simp]

theorem CircleDeg1Lift.map_add_nat (f : CircleDeg1Lift) (x : ℝ) (n : ℕ) : f (x + ↑n) = f x + ↑n

@[simp]

theorem CircleDeg1Lift.map_nat_add (f : CircleDeg1Lift) (n : ℕ) (x : ℝ) : f (↑n + x) = ↑n + f x

@[simp]

theorem CircleDeg1Lift.map_sub_nat (f : CircleDeg1Lift) (x : ℝ) (n : ℕ) : f (x - ↑n) = f x - ↑n

theorem CircleDeg1Lift.map_int_of_map_zero (f : CircleDeg1Lift) (n : ℤ) : f ↑n = f 0 + ↑n

@[simp]

theorem CircleDeg1Lift.map_fract_sub_fract_eq (f : CircleDeg1Lift) (x : ℝ) : f (Int.fract x) - Int.fract x = f x - x

Pointwise order on circle maps

noncomputable instance CircleDeg1Lift.instLatticeCircleDeg1Lift : Lattice CircleDeg1Lift

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CircleDeg1Lift.sup_apply (f : CircleDeg1Lift) (g : CircleDeg1Lift) (x : ℝ) : (f ⊔ g) x = max (f x) (g x)

@[simp]

theorem CircleDeg1Lift.inf_apply (f : CircleDeg1Lift) (g : CircleDeg1Lift) (x : ℝ) : (f ⊓ g) x = min (f x) (g x)

theorem CircleDeg1Lift.iterate_monotone (n : ℕ) : Monotone fun (f : CircleDeg1Lift) => (⇑f)^[n]

theorem CircleDeg1Lift.iterate_mono {f : CircleDeg1Lift} {g : CircleDeg1Lift} (h : f ≤ g) (n : ℕ) : (⇑f)^[n] ≤ (⇑g)^[n]

theorem CircleDeg1Lift.pow_mono {f : CircleDeg1Lift} {g : CircleDeg1Lift} (h : f ≤ g) (n : ℕ) : f ^ n ≤ g ^ n

theorem CircleDeg1Lift.pow_monotone (n : ℕ) : Monotone fun (f : CircleDeg1Lift) => f ^ 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 CircleDeg1Lift.map_le_of_map_zero (f : CircleDeg1Lift) (x : ℝ) : f x ≤ f 0 + ↑⌈x⌉

theorem CircleDeg1Lift.map_map_zero_le (f : CircleDeg1Lift) (g : CircleDeg1Lift) : f (g 0) ≤ f 0 + ↑⌈g 0⌉

theorem CircleDeg1Lift.floor_map_map_zero_le (f : CircleDeg1Lift) (g : CircleDeg1Lift) : ⌊f (g 0)⌋ ≤ ⌊f 0⌋ + ⌈g 0⌉

theorem CircleDeg1Lift.ceil_map_map_zero_le (f : CircleDeg1Lift) (g : CircleDeg1Lift) : ⌈f (g 0)⌉ ≤ ⌈f 0⌉ + ⌈g 0⌉

theorem CircleDeg1Lift.map_map_zero_lt (f : CircleDeg1Lift) (g : CircleDeg1Lift) : f (g 0) < f 0 + g 0 + 1

theorem CircleDeg1Lift.le_map_of_map_zero (f : CircleDeg1Lift) (x : ℝ) : f 0 + ↑⌊x⌋ ≤ f x

theorem CircleDeg1Lift.le_map_map_zero (f : CircleDeg1Lift) (g : CircleDeg1Lift) : f 0 + ↑⌊g 0⌋ ≤ f (g 0)

theorem CircleDeg1Lift.le_floor_map_map_zero (f : CircleDeg1Lift) (g : CircleDeg1Lift) : ⌊f 0⌋ + ⌊g 0⌋ ≤ ⌊f (g 0)⌋

theorem CircleDeg1Lift.le_ceil_map_map_zero (f : CircleDeg1Lift) (g : CircleDeg1Lift) : ⌈f 0⌉ + ⌊g 0⌋ ≤ ⌈(f * g) 0⌉

theorem CircleDeg1Lift.lt_map_map_zero (f : CircleDeg1Lift) (g : CircleDeg1Lift) : f 0 + g 0 - 1 < f (g 0)

theorem CircleDeg1Lift.dist_map_map_zero_lt (f : CircleDeg1Lift) (g : CircleDeg1Lift) : dist (f 0 + g 0) (f (g 0)) < 1

theorem CircleDeg1Lift.dist_map_zero_lt_of_semiconj {f : CircleDeg1Lift} {g₁ : CircleDeg1Lift} {g₂ : CircleDeg1Lift} (h : Function.Semiconj ⇑f ⇑g₁ ⇑g₂) : dist (g₁ 0) (g₂ 0) < 2

theorem CircleDeg1Lift.dist_map_zero_lt_of_semiconjBy {f : CircleDeg1Lift} {g₁ : CircleDeg1Lift} {g₂ : CircleDeg1Lift} (h : SemiconjBy f g₁ g₂) : dist (g₁ 0) (g₂ 0) < 2

Limits at infinities and continuity

theorem CircleDeg1Lift.tendsto_atBot (f : CircleDeg1Lift) : Filter.Tendsto (⇑f) Filter.atBot Filter.atBot

theorem CircleDeg1Lift.tendsto_atTop (f : CircleDeg1Lift) : Filter.Tendsto (⇑f) Filter.atTop Filter.atTop

theorem CircleDeg1Lift.continuous_iff_surjective (f : CircleDeg1Lift) : Continuous ⇑f ↔ Function.Surjective ⇑f

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 CircleDeg1Lift.iterate_le_of_map_le_add_int (f : CircleDeg1Lift) {x : ℝ} {m : ℤ} (h : f x ≤ x + ↑m) (n : ℕ) : (⇑f)^[n] x ≤ x + ↑n * ↑m

theorem CircleDeg1Lift.le_iterate_of_add_int_le_map (f : CircleDeg1Lift) {x : ℝ} {m : ℤ} (h : x + ↑m ≤ f x) (n : ℕ) : x + ↑n * ↑m ≤ (⇑f)^[n] x

theorem CircleDeg1Lift.iterate_eq_of_map_eq_add_int (f : CircleDeg1Lift) {x : ℝ} {m : ℤ} (h : f x = x + ↑m) (n : ℕ) : (⇑f)^[n] x = x + ↑n * ↑m

theorem CircleDeg1Lift.iterate_pos_le_iff (f : CircleDeg1Lift) {x : ℝ} {m : ℤ} {n : ℕ} (hn : 0 < n) : (⇑f)^[n] x ≤ x + ↑n * ↑m ↔ f x ≤ x + ↑m

theorem CircleDeg1Lift.iterate_pos_lt_iff (f : CircleDeg1Lift) {x : ℝ} {m : ℤ} {n : ℕ} (hn : 0 < n) : (⇑f)^[n] x < x + ↑n * ↑m ↔ f x < x + ↑m

theorem CircleDeg1Lift.iterate_pos_eq_iff (f : CircleDeg1Lift) {x : ℝ} {m : ℤ} {n : ℕ} (hn : 0 < n) : (⇑f)^[n] x = x + ↑n * ↑m ↔ f x = x + ↑m

theorem CircleDeg1Lift.le_iterate_pos_iff (f : CircleDeg1Lift) {x : ℝ} {m : ℤ} {n : ℕ} (hn : 0 < n) : x + ↑n * ↑m ≤ (⇑f)^[n] x ↔ x + ↑m ≤ f x

theorem CircleDeg1Lift.lt_iterate_pos_iff (f : CircleDeg1Lift) {x : ℝ} {m : ℤ} {n : ℕ} (hn : 0 < n) : x + ↑n * ↑m < (⇑f)^[n] x ↔ x + ↑m < f x

theorem CircleDeg1Lift.mul_floor_map_zero_le_floor_iterate_zero (f : CircleDeg1Lift) (n : ℕ) : ↑n * ⌊f 0⌋ ≤ ⌊(⇑f)^[n] 0⌋

Definition of translation number

def CircleDeg1Lift.transnumAuxSeq (f : CircleDeg1Lift) (n : ℕ) : ℝ

An auxiliary sequence used to define the translation number.

Equations

• CircleDeg1Lift.transnumAuxSeq f n = (f ^ 2 ^ n) 0 / 2 ^ n

def CircleDeg1Lift.translationNumber (f : CircleDeg1Lift) : ℝ

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.

Equations

• CircleDeg1Lift.translationNumber f = limUnder Filter.atTop (CircleDeg1Lift.transnumAuxSeq f)

theorem CircleDeg1Lift.transnumAuxSeq_def (f : CircleDeg1Lift) : CircleDeg1Lift.transnumAuxSeq f = fun (n : ℕ) => (f ^ 2 ^ n) 0 / 2 ^ n

theorem CircleDeg1Lift.translationNumber_eq_of_tendsto_aux (f : CircleDeg1Lift) {τ' : ℝ} (h : Filter.Tendsto (CircleDeg1Lift.transnumAuxSeq f) Filter.atTop (nhds τ')) : CircleDeg1Lift.translationNumber f = τ'

theorem CircleDeg1Lift.translationNumber_eq_of_tendsto₀ (f : CircleDeg1Lift) {τ' : ℝ} (h : Filter.Tendsto (fun (n : ℕ) => (⇑f)^[n] 0 / ↑n) Filter.atTop (nhds τ')) : CircleDeg1Lift.translationNumber f = τ'

theorem CircleDeg1Lift.translationNumber_eq_of_tendsto₀' (f : CircleDeg1Lift) {τ' : ℝ} (h : Filter.Tendsto (fun (n : ℕ) => (⇑f)^[n + 1] 0 / (↑n + 1)) Filter.atTop (nhds τ')) : CircleDeg1Lift.translationNumber f = τ'

theorem CircleDeg1Lift.transnumAuxSeq_zero (f : CircleDeg1Lift) : CircleDeg1Lift.transnumAuxSeq f 0 = f 0

theorem CircleDeg1Lift.transnumAuxSeq_dist_lt (f : CircleDeg1Lift) (n : ℕ) : dist (CircleDeg1Lift.transnumAuxSeq f n) (CircleDeg1Lift.transnumAuxSeq f (n + 1)) < 1 / 2 / 2 ^ n

theorem CircleDeg1Lift.tendsto_translationNumber_aux (f : CircleDeg1Lift) : Filter.Tendsto (CircleDeg1Lift.transnumAuxSeq f) Filter.atTop (nhds (CircleDeg1Lift.translationNumber f))

theorem CircleDeg1Lift.dist_map_zero_translationNumber_le (f : CircleDeg1Lift) : dist (f 0) (CircleDeg1Lift.translationNumber f) ≤ 1

theorem CircleDeg1Lift.tendsto_translationNumber_of_dist_bounded_aux (f : CircleDeg1Lift) (x : ℕ → ℝ) (C : ℝ) (H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C) : Filter.Tendsto (fun (n : ℕ) => x (2 ^ n) / 2 ^ n) Filter.atTop (nhds (CircleDeg1Lift.translationNumber f))

theorem CircleDeg1Lift.translationNumber_eq_of_dist_bounded {f : CircleDeg1Lift} {g : CircleDeg1Lift} (C : ℝ) (H : ∀ (n : ℕ), dist ((f ^ n) 0) ((g ^ n) 0) ≤ C) : CircleDeg1Lift.translationNumber f = CircleDeg1Lift.translationNumber g

@[simp]

theorem CircleDeg1Lift.translationNumber_one : CircleDeg1Lift.translationNumber 1 = 0

theorem CircleDeg1Lift.translationNumber_eq_of_semiconjBy {f : CircleDeg1Lift} {g₁ : CircleDeg1Lift} {g₂ : CircleDeg1Lift} (H : SemiconjBy f g₁ g₂) : CircleDeg1Lift.translationNumber g₁ = CircleDeg1Lift.translationNumber g₂

theorem CircleDeg1Lift.translationNumber_eq_of_semiconj {f : CircleDeg1Lift} {g₁ : CircleDeg1Lift} {g₂ : CircleDeg1Lift} (H : Function.Semiconj ⇑f ⇑g₁ ⇑g₂) : CircleDeg1Lift.translationNumber g₁ = CircleDeg1Lift.translationNumber g₂

theorem CircleDeg1Lift.translationNumber_mul_of_commute {f : CircleDeg1Lift} {g : CircleDeg1Lift} (h : Commute f g) : CircleDeg1Lift.translationNumber (f * g) = CircleDeg1Lift.translationNumber f + CircleDeg1Lift.translationNumber g

@[simp]

theorem CircleDeg1Lift.translationNumber_units_inv (f : CircleDeg1Liftˣ) : CircleDeg1Lift.translationNumber ↑f⁻¹ = -CircleDeg1Lift.translationNumber ↑f

@[simp]

theorem CircleDeg1Lift.translationNumber_pow (f : CircleDeg1Lift) (n : ℕ) : CircleDeg1Lift.translationNumber (f ^ n) = ↑n * CircleDeg1Lift.translationNumber f

@[simp]

theorem CircleDeg1Lift.translationNumber_zpow (f : CircleDeg1Liftˣ) (n : ℤ) : CircleDeg1Lift.translationNumber ↑(f ^ n) = ↑n * CircleDeg1Lift.translationNumber ↑f

@[simp]

theorem CircleDeg1Lift.translationNumber_conj_eq (f : CircleDeg1Liftˣ) (g : CircleDeg1Lift) : CircleDeg1Lift.translationNumber (↑f * g * ↑f⁻¹) = CircleDeg1Lift.translationNumber g

@[simp]

theorem CircleDeg1Lift.translationNumber_conj_eq' (f : CircleDeg1Liftˣ) (g : CircleDeg1Lift) : CircleDeg1Lift.translationNumber (↑f⁻¹ * g * ↑f) = CircleDeg1Lift.translationNumber g

theorem CircleDeg1Lift.dist_pow_map_zero_mul_translationNumber_le (f : CircleDeg1Lift) (n : ℕ) : dist ((f ^ n) 0) (↑n * CircleDeg1Lift.translationNumber f) ≤ 1

theorem CircleDeg1Lift.tendsto_translation_number₀' (f : CircleDeg1Lift) : Filter.Tendsto (fun (n : ℕ) => (f ^ (n + 1)) 0 / (↑n + 1)) Filter.atTop (nhds (CircleDeg1Lift.translationNumber f))

theorem CircleDeg1Lift.tendsto_translation_number₀ (f : CircleDeg1Lift) : Filter.Tendsto (fun (n : ℕ) => (f ^ n) 0 / ↑n) Filter.atTop (nhds (CircleDeg1Lift.translationNumber f))

theorem CircleDeg1Lift.tendsto_translationNumber (f : CircleDeg1Lift) (x : ℝ) : Filter.Tendsto (fun (n : ℕ) => ((f ^ n) x - x) / ↑n) Filter.atTop (nhds (CircleDeg1Lift.translationNumber f))

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.

theorem CircleDeg1Lift.tendsto_translation_number' (f : CircleDeg1Lift) (x : ℝ) : Filter.Tendsto (fun (n : ℕ) => ((f ^ (n + 1)) x - x) / (↑n + 1)) Filter.atTop (nhds (CircleDeg1Lift.translationNumber f))

theorem CircleDeg1Lift.translationNumber_mono : Monotone CircleDeg1Lift.translationNumber

theorem CircleDeg1Lift.translationNumber_translate (x : ℝ) : CircleDeg1Lift.translationNumber ↑(CircleDeg1Lift.translate (Multiplicative.ofAdd x)) = x

theorem CircleDeg1Lift.translationNumber_le_of_le_add (f : CircleDeg1Lift) {z : ℝ} (hz : ∀ (x : ℝ), f x ≤ x + z) : CircleDeg1Lift.translationNumber f ≤ z

theorem CircleDeg1Lift.le_translationNumber_of_add_le (f : CircleDeg1Lift) {z : ℝ} (hz : ∀ (x : ℝ), x + z ≤ f x) : z ≤ CircleDeg1Lift.translationNumber f

theorem CircleDeg1Lift.translationNumber_le_of_le_add_int (f : CircleDeg1Lift) {x : ℝ} {m : ℤ} (h : f x ≤ x + ↑m) : CircleDeg1Lift.translationNumber f ≤ ↑m

theorem CircleDeg1Lift.translationNumber_le_of_le_add_nat (f : CircleDeg1Lift) {x : ℝ} {m : ℕ} (h : f x ≤ x + ↑m) : CircleDeg1Lift.translationNumber f ≤ ↑m

theorem CircleDeg1Lift.le_translationNumber_of_add_int_le (f : CircleDeg1Lift) {x : ℝ} {m : ℤ} (h : x + ↑m ≤ f x) : ↑m ≤ CircleDeg1Lift.translationNumber f

theorem CircleDeg1Lift.le_translationNumber_of_add_nat_le (f : CircleDeg1Lift) {x : ℝ} {m : ℕ} (h : x + ↑m ≤ f x) : ↑m ≤ CircleDeg1Lift.translationNumber f

theorem CircleDeg1Lift.translationNumber_of_eq_add_int (f : CircleDeg1Lift) {x : ℝ} {m : ℤ} (h : f x = x + ↑m) : CircleDeg1Lift.translationNumber f = ↑m

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 CircleDeg1Lift.floor_sub_le_translationNumber (f : CircleDeg1Lift) (x : ℝ) : ↑⌊f x - x⌋ ≤ CircleDeg1Lift.translationNumber f

theorem CircleDeg1Lift.translationNumber_le_ceil_sub (f : CircleDeg1Lift) (x : ℝ) : CircleDeg1Lift.translationNumber f ≤ ↑⌈f x - x⌉

theorem CircleDeg1Lift.map_lt_of_translationNumber_lt_int (f : CircleDeg1Lift) {n : ℤ} (h : CircleDeg1Lift.translationNumber f < ↑n) (x : ℝ) : f x < x + ↑n

theorem CircleDeg1Lift.map_lt_of_translationNumber_lt_nat (f : CircleDeg1Lift) {n : ℕ} (h : CircleDeg1Lift.translationNumber f < ↑n) (x : ℝ) : f x < x + ↑n

theorem CircleDeg1Lift.map_lt_add_floor_translationNumber_add_one (f : CircleDeg1Lift) (x : ℝ) : f x < x + ↑⌊CircleDeg1Lift.translationNumber f⌋ + 1

theorem CircleDeg1Lift.map_lt_add_translationNumber_add_one (f : CircleDeg1Lift) (x : ℝ) : f x < x + CircleDeg1Lift.translationNumber f + 1

theorem CircleDeg1Lift.lt_map_of_int_lt_translationNumber (f : CircleDeg1Lift) {n : ℤ} (h : ↑n < CircleDeg1Lift.translationNumber f) (x : ℝ) : x + ↑n < f x

theorem CircleDeg1Lift.lt_map_of_nat_lt_translationNumber (f : CircleDeg1Lift) {n : ℕ} (h : ↑n < CircleDeg1Lift.translationNumber f) (x : ℝ) : x + ↑n < f x

theorem CircleDeg1Lift.translationNumber_of_map_pow_eq_add_int (f : CircleDeg1Lift) {x : ℝ} {n : ℕ} {m : ℤ} (h : (f ^ n) x = x + ↑m) (hn : 0 < n) : CircleDeg1Lift.translationNumber f = ↑m / ↑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 CircleDeg1Lift.forall_map_sub_of_Icc (f : CircleDeg1Lift) (P : ℝ → Prop) (h : ∀ x ∈ Set.Icc 0 1, P (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.

theorem CircleDeg1Lift.translationNumber_lt_of_forall_lt_add (f : CircleDeg1Lift) (hf : Continuous ⇑f) {z : ℝ} (hz : ∀ (x : ℝ), f x < x + z) : CircleDeg1Lift.translationNumber f < z

theorem CircleDeg1Lift.lt_translationNumber_of_forall_add_lt (f : CircleDeg1Lift) (hf : Continuous ⇑f) {z : ℝ} (hz : ∀ (x : ℝ), x + z < f x) : z < CircleDeg1Lift.translationNumber f

theorem CircleDeg1Lift.exists_eq_add_translationNumber (f : CircleDeg1Lift) (hf : Continuous ⇑f) : ∃ (x : ℝ), f x = x + CircleDeg1Lift.translationNumber f

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

theorem CircleDeg1Lift.translationNumber_eq_int_iff (f : CircleDeg1Lift) (hf : Continuous ⇑f) {m : ℤ} : CircleDeg1Lift.translationNumber f = ↑m ↔ ∃ (x : ℝ), f x = x + ↑m

theorem CircleDeg1Lift.continuous_pow (f : CircleDeg1Lift) (hf : Continuous ⇑f) (n : ℕ) : Continuous ⇑(f ^ n)

theorem CircleDeg1Lift.translationNumber_eq_rat_iff (f : CircleDeg1Lift) (hf : Continuous ⇑f) {m : ℤ} {n : ℕ} (hn : 0 < n) : CircleDeg1Lift.translationNumber f = ↑m / ↑n ↔ ∃ (x : ℝ), (f ^ n) x = x + ↑m

theorem CircleDeg1Lift.semiconj_of_group_action_of_forall_translationNumber_eq {G : Type u_1} [Group G] (f₁ : G →* CircleDeg1Lift) (f₂ : G →* CircleDeg1Lift) (h : ∀ (g : G), CircleDeg1Lift.translationNumber (f₁ g) = CircleDeg1Lift.translationNumber (f₂ g)) : ∃ (F : CircleDeg1Lift), ∀ (g : G), Function.Semiconj ⇑F ⇑(f₁ g) ⇑(f₂ g)

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'homeomorphismes du cercle et cohomologie bornee][ghys87:groupes].

theorem CircleDeg1Lift.units_semiconj_of_translationNumber_eq {f₁ : CircleDeg1Liftˣ} {f₂ : CircleDeg1Liftˣ} (h : CircleDeg1Lift.translationNumber ↑f₁ = CircleDeg1Lift.translationNumber ↑f₂) : ∃ (F : CircleDeg1Lift), Function.Semiconj ⇑F ⇑↑f₁ ⇑↑f₂

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

theorem CircleDeg1Lift.semiconj_of_isUnit_of_translationNumber_eq {f₁ : CircleDeg1Lift} {f₂ : CircleDeg1Lift} (h₁ : IsUnit f₁) (h₂ : IsUnit f₂) (h : CircleDeg1Lift.translationNumber f₁ = CircleDeg1Lift.translationNumber f₂) : ∃ (F : CircleDeg1Lift), Function.Semiconj ⇑F ⇑f₁ ⇑f₂

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

theorem CircleDeg1Lift.semiconj_of_bijective_of_translationNumber_eq {f₁ : CircleDeg1Lift} {f₂ : CircleDeg1Lift} (h₁ : Function.Bijective ⇑f₁) (h₂ : Function.Bijective ⇑f₂) (h : CircleDeg1Lift.translationNumber f₁ = CircleDeg1Lift.translationNumber f₂) : ∃ (F : CircleDeg1Lift), Function.Semiconj ⇑F ⇑f₁ ⇑f₂

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.