English
For every n, the distance between consecutive terms of transnumAuxSeq shrinks faster than 1/2^n, concretely dist(f.transnumAuxSeq(n), f.transnumAuxSeq(n+1)) < 1/2/2^n.
Русский
Для каждого n расстояние между соседними членами transnumAuxSeq уменьшается быстрее, чем 1/2^n: dist(f.transnumAuxSeq(n), f.transnumAuxSeq(n+1)) < 1/2/2^n.
LaTeX
$$$ \forall f \in CircleDeg1Lift, \forall n \in \mathbb{N}, \ dist( f.transnumAuxSeq(n), f.transnumAuxSeq(n+1) ) < \dfrac{1}{2^{n+1}}. $$$
Lean4
theorem transnumAuxSeq_dist_lt (n : ℕ) : dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) < 1 / 2 / 2 ^ n :=
by
have : 0 < (2 ^ (n + 1) : ℝ) := pow_pos zero_lt_two _
rw [div_div, ← pow_succ', ← abs_of_pos this]
calc
_ = dist ((f ^ 2 ^ n) 0 + (f ^ 2 ^ n) 0) ((f ^ 2 ^ n) ((f ^ 2 ^ n) 0)) / |2 ^ (n + 1)| :=
by
simp_rw [transnumAuxSeq, Real.dist_eq]
rw [← abs_div, sub_div, pow_succ, pow_succ', ← two_mul, mul_div_mul_left _ _ (two_ne_zero' ℝ), pow_mul, sq,
mul_apply]
_ < _ := by gcongr; exact (f ^ 2 ^ n).dist_map_map_zero_lt (f ^ 2 ^ n)
