English
If n is an integer with n < τ(f), then for all x, x + n < f(x).
Русский
Если n ∈ ℤ и n < τ(f), то для всех x выполняется x + n < f(x).
LaTeX
$$$$ \\forall f, \\forall n \\in \\mathbb{Z}, \\ n < \\tau f \\Rightarrow \\forall x \\in \\mathbb{R}, \\ x + n < f(x). $$$$
Lean4
/-- 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 semiconj_of_group_action_of_forall_translationNumber_eq {G : Type*} [Group G] (f₁ f₂ : G →* CircleDeg1Lift)
(h : ∀ g, τ (f₁ g) = τ (f₂ g)) : ∃ F : CircleDeg1Lift, ∀ g, Semiconj F (f₁ g) (f₂ g) := by
-- Equality of translation number guarantees that for each `x`
-- the set `{f₂ g⁻¹ (f₁ g x) | g : G}` is bounded above.
have : ∀ x, BddAbove (range fun g => f₂ g⁻¹ (f₁ g x)) :=
by
refine fun x => ⟨x + 2, ?_⟩
rintro _ ⟨g, rfl⟩
have : τ (f₂ g⁻¹) = -τ (f₂ g) := by
rw [← MonoidHom.coe_toHomUnits, MonoidHom.map_inv, translationNumber_units_inv, MonoidHom.coe_toHomUnits]
calc
f₂ g⁻¹ (f₁ g x) ≤ f₂ g⁻¹ (x + τ (f₁ g) + 1) := mono _ (map_lt_add_translationNumber_add_one _ _).le
_ = f₂ g⁻¹ (x + τ (f₂ g)) + 1 := by rw [h, map_add_one]
_ ≤ x + τ (f₂ g) + τ (f₂ g⁻¹) + 1 + 1 := (add_le_add_right (map_lt_add_translationNumber_add_one _ _).le _)
_ = x + 2 := by
simp [this, add_assoc, one_add_one_eq_two]
-- We have a theorem about actions by `OrderIso`, so we introduce auxiliary maps
-- to `ℝ ≃o ℝ`.
set F₁ := toOrderIso.comp f₁.toHomUnits
set F₂ := toOrderIso.comp f₂.toHomUnits
have hF₁ : ∀ g, ⇑(F₁ g) = f₁ g := fun _ => rfl
have hF₂ : ∀ g, ⇑(F₂ g) = f₂ g := fun _ => rfl
refine
⟨⟨⟨fun x ↦ ⨆ g', (F₂ g')⁻¹ (F₁ g' x), fun x y hxy => ?_⟩, fun x => ?_⟩, csSup_div_semiconj F₂ F₁ fun x => ?_⟩ <;>
simp only [hF₁, hF₂, ← map_inv]
· exact ciSup_mono (this y) fun g => mono _ (mono _ hxy)
· simp only [map_add_one]
exact
(Monotone.map_ciSup_of_continuousAt (continuousAt_id.add continuousAt_const) (monotone_id.add_const (1 : ℝ))
(this x)).symm
· exact this x
