English
If there exists a bound C and a sequence x with dist((f^n)0, x(n)) ≤ C for all n, then x(2^n)/2^n converges to τ f.
Русский
Если существует константа границы C и последовательность x с условием dist((f^n)0, x(n)) ≤ C для всех n, то x(2^n)/2^n сходится к τ f.
LaTeX
$$$ \forall f, x: \mathbb{N} \to \mathbb{R}, C \in \mathbb{R}, \left( \forall n, \operatorname{dist}((f^n)0, x(n)) \le C \right) \Rightarrow \operatorname{Tendsto} (n \mapsto x(2^n)/2^n)_{atTop} (\mathcal{N}(τ f)). $$$
Lean4
theorem tendsto_translationNumber_of_dist_bounded_aux (x : ℕ → ℝ) (C : ℝ) (H : ∀ n : ℕ, dist ((f ^ n) 0) (x n) ≤ C) :
Tendsto (fun n : ℕ => x (2 ^ n) / 2 ^ n) atTop (𝓝 <| τ f) :=
by
apply f.tendsto_translationNumber_aux.congr_dist (squeeze_zero (fun _ => dist_nonneg) _ _)
· exact fun n => C / 2 ^ n
· intro n
have : 0 < (2 ^ n : ℝ) := pow_pos zero_lt_two _
convert (div_le_div_iff_of_pos_right this).2 (H (2 ^ n)) using 1
rw [transnumAuxSeq, Real.dist_eq, ← sub_div, abs_div, abs_of_pos this, Real.dist_eq]
·
exact
mul_zero C ▸ tendsto_const_nhds.mul <| tendsto_inv_atTop_zero.comp <| tendsto_pow_atTop_atTop_of_one_lt one_lt_two
