α : Type u_1
β : Type ?u.441500
ι : Type ?u.441503
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ⊤
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ edist (f n) a ≤ 2 * C * 2⁻¹ ^ n
α : Type u_1
β : Type ?u.441500
ι : Type ?u.441503
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / 2 ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ edist (f n) a ≤ 2 * C / 2 ^ n
simp only [div_eq_mul_inv, ENNReal.inv_pow] at *
α : Type u_1
β : Type ?u.441500
ι : Type ?u.441503
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ⊤
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ edist (f n) a ≤ C * 2⁻¹ ^ n * 2
α : Type u_1
β : Type ?u.441500
ι : Type ?u.441503
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ⊤
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ edist (f n) a ≤ 2 * C * 2⁻¹ ^ n
rw [mul_assoc, mul_comm]
case h.e'_4
α : Type u_1
β : Type ?u.441500
ι : Type ?u.441503
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ⊤
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ C * 2⁻¹ ^ n * 2 = C * 2⁻¹ ^ n / (1 - 2⁻¹)
α : Type u_1
β : Type ?u.441500
ι : Type ?u.441503
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ⊤
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ edist (f n) a ≤ C * 2⁻¹ ^ n * 2
convert edist_le_of_edist_le_geometric_of_tendsto 2⁻¹ C hu ha n using 1
no goals
case h.e'_4
α : Type u_1
β : Type ?u.441500
ι : Type ?u.441503
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ⊤
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ C * 2⁻¹ ^ n * 2 = C * 2⁻¹ ^ n / (1 - 2⁻¹)
rw [ENNReal.one_sub_inv_two, div_eq_mul_inv, inv_inv]