α : Type ?u.155279
β : Type ?u.155282
ι : Type ?u.155285
𝕜 : Type u_1
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
r : 𝕜
hr : ‖r‖ < 1
A : Summable fun n => ↑n * r ^ n
⊢ HasSum (fun n => ↑n * r ^ n) (r / (1 - r) ^ 2)
α : Type ?u.155279
β : Type ?u.155282
ι : Type ?u.155285
𝕜 : Type u_1
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
r : 𝕜
hr : ‖r‖ < 1
⊢ HasSum (fun n => ↑n * r ^ n) (r / (1 - r) ^ 2)
have A : Summable (fun n ↦ (n : 𝕜) * r ^ n : ℕ → 𝕜) := by
  simpa only [pow_one] using summable_pow_mul_geometric_of_norm_lt_1 1 hr
α : Type ?u.155279
β : Type ?u.155282
ι : Type ?u.155285
𝕜 : Type u_1
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
r : 𝕜
hr : ‖r‖ < 1
A : Summable fun n => ↑n * r ^ n
B : HasSum (fun x => r ^ x) (1 - r)⁻¹
⊢ (∑' (b : ℕ), ↑b * r ^ b) = r / (1 - r) ^ 2
α : Type ?u.155279
β : Type ?u.155282
ι : Type ?u.155285
𝕜 : Type u_1
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
r : 𝕜
hr : ‖r‖ < 1
A : Summable fun n => ↑n * r ^ n
B : HasSum (fun x => r ^ x) (1 - r)⁻¹
⊢ HasSum (fun n => ↑n * r ^ n) (r / (1 - r) ^ 2)
refine' A.hasSum_iff.2 _
α : Type ?u.155279
β : Type ?u.155282
ι : Type ?u.155285
𝕜 : Type u_1
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
r : 𝕜
hr : ‖r‖ < 1
A : Summable fun n => ↑n * r ^ n
B : HasSum (fun x => r ^ x) (1 - r)⁻¹
hr' : r ≠ 1
⊢ (∑' (b : ℕ), ↑b * r ^ b) = r / (1 - r) ^ 2
α : Type ?u.155279
β : Type ?u.155282
ι : Type ?u.155285
𝕜 : Type u_1
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
r : 𝕜
hr : ‖r‖ < 1
A : Summable fun n => ↑n * r ^ n
B : HasSum (fun x => r ^ x) (1 - r)⁻¹
⊢ (∑' (b : ℕ), ↑b * r ^ b) = r / (1 - r) ^ 2
have hr' : r ≠ 1 := by
  rintro rfl
  simp [lt_irrefl] at hr
α : Type ?u.155279
β : Type ?u.155282
ι : Type ?u.155285
𝕜 : Type u_1
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
r : 𝕜
hr : ‖r‖ < 1
A : Summable fun n => ↑n * r ^ n
B : HasSum (fun x => r ^ x) (1 - r)⁻¹
hr' : r ≠ 1
s : 𝕜 := ∑' (n : ℕ), ↑n * r ^ n
⊢ s = r / (1 - r) ^ 2
α : Type ?u.155279
β : Type ?u.155282
ι : Type ?u.155285
𝕜 : Type u_1
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
r : 𝕜
hr : ‖r‖ < 1
A : Summable fun n => ↑n * r ^ n
B : HasSum (fun x => r ^ x) (1 - r)⁻¹
hr' : r ≠ 1
⊢ (∑' (b : ℕ), ↑b * r ^ b) = r / (1 - r) ^ 2
set s : 𝕜 := ∑' n : ℕ, n * r ^ n
no goals
α : Type ?u.155279
β : Type ?u.155282
ι : Type ?u.155285
𝕜 : Type u_1
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
r : 𝕜
hr : ‖r‖ < 1
A : Summable fun n => ↑n * r ^ n
B : HasSum (fun x => r ^ x) (1 - r)⁻¹
hr' : r ≠ 1
s : 𝕜 := ∑' (n : ℕ), ↑n * r ^ n
⊢ s = r / (1 - r) ^ 2
calc
  s = (1 - r) * s / (1 - r) := (mul_div_cancel_left _ (sub_ne_zero.2 hr'.symm)).symm
  _ = (s - r * s) / (1 - r) := by rw [_root_.sub_mul, one_mul]
  _ = (((0 : ℕ) * r ^ 0 + ∑' n : ℕ, (n + 1 : ℕ) * r ^ (n + 1)) - r * s) / (1 - r) := by
    rw [← tsum_eq_zero_add A]
  _ = ((r * ∑' n : ℕ, (n + 1) * r ^ n) - r * s) / (1 - r) := by
    simp [_root_.pow_succ, mul_left_comm _ r, _root_.tsum_mul_left]
  _ = r / (1 - r) ^ 2 := by
    simp [add_mul, tsum_add A B.summable, mul_add, B.tsum_eq, ← div_eq_mul_inv, sq, div_div]
no goals
α : Type ?u.155279
β : Type ?u.155282
ι : Type ?u.155285
𝕜 : Type u_1
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
r : 𝕜
hr : ‖r‖ < 1
⊢ Summable fun n => ↑n * r ^ n
simpa only [pow_one] using summable_pow_mul_geometric_of_norm_lt_1 1 hr
α : Type ?u.155279
β : Type ?u.155282
ι : Type ?u.155285
𝕜 : Type u_1
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
hr : ‖1‖ < 1
A : Summable fun n => ↑n * 1 ^ n
B : HasSum (fun x => 1 ^ x) (1 - 1)⁻¹
⊢ False
α : Type ?u.155279
β : Type ?u.155282
ι : Type ?u.155285
𝕜 : Type u_1
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
r : 𝕜
hr : ‖r‖ < 1
A : Summable fun n => ↑n * r ^ n
B : HasSum (fun x => r ^ x) (1 - r)⁻¹
⊢ r ≠ 1
rintro rfl
no goals
α : Type ?u.155279
β : Type ?u.155282
ι : Type ?u.155285
𝕜 : Type u_1
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
hr : ‖1‖ < 1
A : Summable fun n => ↑n * 1 ^ n
B : HasSum (fun x => 1 ^ x) (1 - 1)⁻¹
⊢ False
simp [lt_irrefl] at hr
no goals
α : Type ?u.155279
β : Type ?u.155282
ι : Type ?u.155285
𝕜 : Type u_1
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
r : 𝕜
hr : ‖r‖ < 1
A : Summable fun n => ↑n * r ^ n
B : HasSum (fun x => r ^ x) (1 - r)⁻¹
hr' : r ≠ 1
s : 𝕜 := ∑' (n : ℕ), ↑n * r ^ n
⊢ (1 - r) * s / (1 - r) = (s - r * s) / (1 - r)
rw [_root_.sub_mul, one_mul]
no goals
α : Type ?u.155279
β : Type ?u.155282
ι : Type ?u.155285
𝕜 : Type u_1
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
r : 𝕜
hr : ‖r‖ < 1
A : Summable fun n => ↑n * r ^ n
B : HasSum (fun x => r ^ x) (1 - r)⁻¹
hr' : r ≠ 1
s : 𝕜 := ∑' (n : ℕ), ↑n * r ^ n
⊢ (s - r * s) / (1 - r) = ((↑0 * r ^ 0 + ∑' (n : ℕ), ↑(n + 1) * r ^ (n + 1)) - r * s) / (1 - r)
rw [← tsum_eq_zero_add A]
no goals
α : Type ?u.155279
β : Type ?u.155282
ι : Type ?u.155285
𝕜 : Type u_1
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
r : 𝕜
hr : ‖r‖ < 1
A : Summable fun n => ↑n * r ^ n
B : HasSum (fun x => r ^ x) (1 - r)⁻¹
hr' : r ≠ 1
s : 𝕜 := ∑' (n : ℕ), ↑n * r ^ n
⊢ ((↑0 * r ^ 0 + ∑' (n : ℕ), ↑(n + 1) * r ^ (n + 1)) - r * s) / (1 - r) =
    ((r * ∑' (n : ℕ), (↑n + 1) * r ^ n) - r * s) / (1 - r)
simp [_root_.pow_succ, mul_left_comm _ r, _root_.tsum_mul_left]
no goals
α : Type ?u.155279
β : Type ?u.155282
ι : Type ?u.155285
𝕜 : Type u_1
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
r : 𝕜
hr : ‖r‖ < 1
A : Summable fun n => ↑n * r ^ n
B : HasSum (fun x => r ^ x) (1 - r)⁻¹
hr' : r ≠ 1
s : 𝕜 := ∑' (n : ℕ), ↑n * r ^ n
⊢ ((r * ∑' (n : ℕ), (↑n + 1) * r ^ n) - r * s) / (1 - r) = r / (1 - r) ^ 2
simp [add_mul, tsum_add A B.summable, mul_add, B.tsum_eq, ← div_eq_mul_inv, sq, div_div]