translationNumber_of_map_pow_eq_add_int

English

If there exist x, n ∈ ℕ and m ∈ ℤ with (f^n)(x) = x + m and n > 0, then τ(f) = m / n.

Русский

Если существуют x ∈ ℝ, n ∈ ℕ, m ∈ ℤ такие, что (f^n)(x) = x + m и n > 0, тогда τ(f) = m / n.

LaTeX

$$$$ \\exists x \\in \\mathbb{R}, \\exists n \\in \\mathbb{N}, \\exists m \\in \\mathbb{Z}, (f^n)(x) = x + m \\;\\&\\; n > 0 \\Rightarrow \\tau f = \\dfrac{m}{n}. $$$$

Lean4

/-- 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 translationNumber_of_map_pow_eq_add_int {x : ℝ} {n : ℕ} {m : ℤ} (h : (f ^ n) x = x + m) (hn : 0 < n) :
    τ f = m / n := by
  have := (f ^ n).translationNumber_of_eq_add_int h
  rwa [translationNumber_pow, mul_comm, ← eq_div_iff] at this
  exact Nat.cast_ne_zero.2 (ne_of_gt hn)

Похожие утверждения