no goals
n : ℕ
m : ℝ
m1 : 1 < m
m0 : 0 < m
mi : 1 / m < 1
⊢ (∑' (i : ℕ), 1 / m ^ (i + (n + 1)!)) = ∑' (i : ℕ), (1 / m) ^ i * (1 / m ^ (n + 1)!)
simp only [pow_add, one_div, mul_inv, inv_pow]
no goals
n : ℕ
m : ℝ
m1 : 1 < m
m0 : 0 < m
mi : 1 / m < 1
⊢ (∑' (i : ℕ), (1 / m) ^ i) * (1 / m ^ (n + 1)!) = (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!)
rw [tsum_geometric_of_lt_1 (by positivity) mi]
no goals
n : ℕ
m : ℝ
m1 : 1 < m
m0 : 0 < m
mi : 1 / m < 1
⊢ 0 ≤ 1 / m
positivity