α : Type ?u.1244932
β : Type ?u.1244935
ι : Type ?u.1244938
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
this : HasSum (fun i => x ^ i * (1 - x)) ((∑' (b : ℕ), x ^ b) * (1 - x))
⊢ (∑' (i : ℕ), x ^ i) * (1 - x) = 1
α : Type ?u.1244932
β : Type ?u.1244935
ι : Type ?u.1244938
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
⊢ (∑' (i : ℕ), x ^ i) * (1 - x) = 1
have := (NormedRing.summable_geometric_of_norm_lt_1 x h).hasSum.mul_right (1 - x)
α : Type ?u.1244932
β : Type ?u.1244935
ι : Type ?u.1244938
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
this : HasSum (fun i => x ^ i * (1 - x)) ((∑' (b : ℕ), x ^ b) * (1 - x))
⊢ Tendsto (fun n => ∑ i in Finset.range n, x ^ i * (1 - x)) atTop (𝓝 1)
α : Type ?u.1244932
β : Type ?u.1244935
ι : Type ?u.1244938
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
this : HasSum (fun i => x ^ i * (1 - x)) ((∑' (b : ℕ), x ^ b) * (1 - x))
⊢ (∑' (i : ℕ), x ^ i) * (1 - x) = 1
refine' tendsto_nhds_unique this.tendsto_sum_nat _
α : Type ?u.1244932
β : Type ?u.1244935
ι : Type ?u.1244938
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
this✝ : HasSum (fun i => x ^ i * (1 - x)) ((∑' (b : ℕ), x ^ b) * (1 - x))
this : Tendsto (fun n => 1 - x ^ n) atTop (𝓝 1)
⊢ Tendsto (fun n => ∑ i in Finset.range n, x ^ i * (1 - x)) atTop (𝓝 1)
α : Type ?u.1244932
β : Type ?u.1244935
ι : Type ?u.1244938
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
this : HasSum (fun i => x ^ i * (1 - x)) ((∑' (b : ℕ), x ^ b) * (1 - x))
⊢ Tendsto (fun n => ∑ i in Finset.range n, x ^ i * (1 - x)) atTop (𝓝 1)
have : Tendsto (fun n : ℕ ↦ 1 - x ^ n) atTop (𝓝 1) := by
  simpa using tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_0_of_norm_lt_1 h)
case h.e'_3.h
α : Type ?u.1244932
β : Type ?u.1244935
ι : Type ?u.1244938
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
this✝ : HasSum (fun i => x ^ i * (1 - x)) ((∑' (b : ℕ), x ^ b) * (1 - x))
this : Tendsto (fun n => 1 - x ^ n) atTop (𝓝 1)
x✝ : ℕ
⊢ 1 - x ^ x✝ = ∑ i in Finset.range x✝, x ^ i * (1 - x)
α : Type ?u.1244932
β : Type ?u.1244935
ι : Type ?u.1244938
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
this✝ : HasSum (fun i => x ^ i * (1 - x)) ((∑' (b : ℕ), x ^ b) * (1 - x))
this : Tendsto (fun n => 1 - x ^ n) atTop (𝓝 1)
⊢ Tendsto (fun n => ∑ i in Finset.range n, x ^ i * (1 - x)) atTop (𝓝 1)
convert← this
no goals
case h.e'_3.h
α : Type ?u.1244932
β : Type ?u.1244935
ι : Type ?u.1244938
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
this✝ : HasSum (fun i => x ^ i * (1 - x)) ((∑' (b : ℕ), x ^ b) * (1 - x))
this : Tendsto (fun n => 1 - x ^ n) atTop (𝓝 1)
x✝ : ℕ
⊢ 1 - x ^ x✝ = ∑ i in Finset.range x✝, x ^ i * (1 - x)
rw [← geom_sum_mul_neg, Finset.sum_mul]
no goals
α : Type ?u.1244932
β : Type ?u.1244935
ι : Type ?u.1244938
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
this : HasSum (fun i => x ^ i * (1 - x)) ((∑' (b : ℕ), x ^ b) * (1 - x))
⊢ Tendsto (fun n => 1 - x ^ n) atTop (𝓝 1)
simpa using tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_0_of_norm_lt_1 h)