Kadiri.summable_linear_geometric_inv_two

theorem summable_linear_geometric_inv_two (C : ℝ) :    Summable (fun k : ℕ => C * ((k + 1 : ℕ) : ℝ) * ((2 : ℝ)⁻¹) ^ k) := by  have hgeom : Summable (fun k : ℕ =>      ((k : ℝ) ^ (1 : ℕ)) * ((2 : ℝ)⁻¹) ^ k) := by    exact summable_pow_mul_geometric_of_norm_lt_one 1      (by norm_num : ‖((2 : ℝ)⁻¹)‖ < 1)  have hgeom0 : Summable (fun k : ℕ => ((2 : ℝ)⁻¹) ^ k) := by    exact summable_geometric_of_lt_one (by positivity) (by norm_num)  have hsum : Summable (fun k : ℕ =>      (((k : ℝ) ^ (1 : ℕ)) + 1) * ((2 : ℝ)⁻¹) ^ k) := by    simpa [add_mul] using hgeom.add hgeom0  have hsum' : Summable (fun k : ℕ =>      ((k + 1 : ℕ) : ℝ) * ((2 : ℝ)⁻¹) ^ k) := by    simpa using hsum  simpa [mul_assoc] using hsum'.mul_left C