f g : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ dist (transnumAuxSeq f n) (transnumAuxSeq f (n + 1)) < 1 / 2 / 2 ^ n
f g : CircleDeg1Lift
n : ℕ
⊢ dist (transnumAuxSeq f n) (transnumAuxSeq f (n + 1)) < 1 / 2 / 2 ^ n
have : 0 < (2 ^ (n + 1) : ℝ) := pow_pos zero_lt_two _
f g : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ dist (transnumAuxSeq f n) (transnumAuxSeq f (n + 1)) < 1 / abs (2 ^ (n + 1))
f g : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ dist (transnumAuxSeq f n) (transnumAuxSeq f (n + 1)) < 1 / 2 / 2 ^ n
rw [div_div, ← pow_succ, ← abs_of_pos this]
f g : CircleDeg1Lift
n : ℕ
this : 0 < abs (2 ^ (n + 1))
⊢ dist (transnumAuxSeq f n) (transnumAuxSeq f (n + 1)) < 1 / abs (2 ^ (n + 1))
f g : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ dist (transnumAuxSeq f n) (transnumAuxSeq f (n + 1)) < 1 / abs (2 ^ (n + 1))
replace := abs_pos.2 (ne_of_gt this)
case h.e'_3
f g : CircleDeg1Lift
n : ℕ
this : 0 < abs (2 ^ (n + 1))
⊢ dist (transnumAuxSeq f n) (transnumAuxSeq f (n + 1)) =
    dist (↑(f ^ 2 ^ n) 0 + ↑(f ^ 2 ^ n) 0) (↑(f ^ 2 ^ n) (↑(f ^ 2 ^ n) 0)) / abs (2 ^ (n + 1))
f g : CircleDeg1Lift
n : ℕ
this : 0 < abs (2 ^ (n + 1))
⊢ dist (transnumAuxSeq f n) (transnumAuxSeq f (n + 1)) < 1 / abs (2 ^ (n + 1))
convert (div_lt_div_right this).2 ((f ^ 2 ^ n).dist_map_map_zero_lt (f ^ 2 ^ n)) using 1
case h.e'_3
f g : CircleDeg1Lift
n : ℕ
this : 0 < abs (2 ^ (n + 1))
⊢ abs (↑(f ^ 2 ^ n) 0 / 2 ^ n - ↑(f ^ 2 ^ (n + 1)) 0 / 2 ^ (n + 1)) =
    abs (↑(f ^ 2 ^ n) 0 + ↑(f ^ 2 ^ n) 0 - ↑(f ^ 2 ^ n) (↑(f ^ 2 ^ n) 0)) / abs (2 ^ (n + 1))
case h.e'_3
f g : CircleDeg1Lift
n : ℕ
this : 0 < abs (2 ^ (n + 1))
⊢ dist (transnumAuxSeq f n) (transnumAuxSeq f (n + 1)) =
    dist (↑(f ^ 2 ^ n) 0 + ↑(f ^ 2 ^ n) 0) (↑(f ^ 2 ^ n) (↑(f ^ 2 ^ n) 0)) / abs (2 ^ (n + 1))
simp_rw [transnumAuxSeq, Real.dist_eq]
no goals
case h.e'_3
f g : CircleDeg1Lift
n : ℕ
this : 0 < abs (2 ^ (n + 1))
⊢ abs (↑(f ^ 2 ^ n) 0 / 2 ^ n - ↑(f ^ 2 ^ (n + 1)) 0 / 2 ^ (n + 1)) =
    abs (↑(f ^ 2 ^ n) 0 + ↑(f ^ 2 ^ n) 0 - ↑(f ^ 2 ^ n) (↑(f ^ 2 ^ n) 0)) / abs (2 ^ (n + 1))
rw [← abs_div, sub_div, pow_succ', pow_succ, ← two_mul, mul_div_mul_left _ _ (two_ne_zero' ℝ),
  pow_mul, sq, mul_apply]