translationNumber — Mathlib

English

The translation number τ(f) is defined as the limit of transnumAuxSeq along atTop:

Русский

Погрешность перевода τ(f) задается как предел transnumAuxSeq при стремлении к atTop:

LaTeX

$$$\operatorname{translationNumber}(f) = \lim_{\!\to\text{atTop}} f.transnumAuxSeq$$$

Lean4

/-- 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. -/
def translationNumber : ℝ :=
  limUnder atTop f.transnumAuxSeq

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