translationNumber_mul_of_commute — Mathlib

English

If f and g commute, then the translation number is additive: τ(f g) = τ(f) + τ(g).

Русский

Если f и g commute, то число трансляции удовлетворяет τ(f g) = τ(f) + τ(g).

LaTeX

$$$ \forall f,g \in CircleDeg1Lift, \operatorname{Commute}(f,g) \Rightarrow τ(f g) = τ(f) + τ(g). $$$

Lean4

theorem translationNumber_mul_of_commute {f g : CircleDeg1Lift} (h : Commute f g) : τ (f * g) = τ f + τ g :=
  by
  refine tendsto_nhds_unique ?_ (f.tendsto_translationNumber_aux.add g.tendsto_translationNumber_aux)
  simp only [transnumAuxSeq, ← add_div]
  refine (f * g).tendsto_translationNumber_of_dist_bounded_aux (fun n ↦ (f ^ n) 0 + (g ^ n) 0) 1 fun n ↦ ?_
  rw [h.mul_pow, dist_comm]
  exact le_of_lt ((f ^ n).dist_map_map_zero_lt (g ^ n))

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