α : Type u_1
β : Type ?u.451019
ι : Type ?u.451022
inst✝ : PseudoMetricSpace α
r C : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun n => C * r ^ n) (C / (1 - r))
⊢ dist (f n) a ≤ C * r ^ n / (1 - r)
α : Type u_1
β : Type ?u.451019
ι : Type ?u.451022
inst✝ : PseudoMetricSpace α
r C : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ dist (f n) a ≤ C * r ^ n / (1 - r)
have := aux_hasSum_of_le_geometric hr hu
case h.e'_4
α : Type u_1
β : Type ?u.451019
ι : Type ?u.451022
inst✝ : PseudoMetricSpace α
r C : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun n => C * r ^ n) (C / (1 - r))
⊢ C * r ^ n / (1 - r) = ∑' (m : ℕ), C * r ^ (n + m)
α : Type u_1
β : Type ?u.451019
ι : Type ?u.451022
inst✝ : PseudoMetricSpace α
r C : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun n => C * r ^ n) (C / (1 - r))
⊢ dist (f n) a ≤ C * r ^ n / (1 - r)
convert dist_le_tsum_of_dist_le_of_tendsto _ hu ⟨_, this⟩ ha n
case h.e'_4
α : Type u_1
β : Type ?u.451019
ι : Type ?u.451022
inst✝ : PseudoMetricSpace α
r C : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun n => C * r ^ n) (C / (1 - r))
⊢ C / (1 - r) * r ^ n = ∑' (m : ℕ), r ^ n * (C * r ^ m)
case h.e'_4
α : Type u_1
β : Type ?u.451019
ι : Type ?u.451022
inst✝ : PseudoMetricSpace α
r C : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun n => C * r ^ n) (C / (1 - r))
⊢ C * r ^ n / (1 - r) = ∑' (m : ℕ), C * r ^ (n + m)
simp only [pow_add, mul_left_comm C, mul_div_right_comm]
case h.e'_4
α : Type u_1
β : Type ?u.451019
ι : Type ?u.451022
inst✝ : PseudoMetricSpace α
r C : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun n => C * r ^ n) (C / (1 - r))
⊢ r ^ n * (C / (1 - r)) = ∑' (m : ℕ), r ^ n * (C * r ^ m)
case h.e'_4
α : Type u_1
β : Type ?u.451019
ι : Type ?u.451022
inst✝ : PseudoMetricSpace α
r C : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun n => C * r ^ n) (C / (1 - r))
⊢ C / (1 - r) * r ^ n = ∑' (m : ℕ), r ^ n * (C * r ^ m)
rw [mul_comm]
no goals
case h.e'_4
α : Type u_1
β : Type ?u.451019
ι : Type ?u.451022
inst✝ : PseudoMetricSpace α
r C : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun n => C * r ^ n) (C / (1 - r))
⊢ r ^ n * (C / (1 - r)) = ∑' (m : ℕ), r ^ n * (C * r ^ m)
exact (this.mul_left _).tsum_eq.symm