scilib documentation

LeanChemicalTheories / math.infinite_series

theorem tsum_coe_mul_geometric_succ {x : ℝ} (hx1 : x < 1) (hx2 : 0 < x) :

∑' (k : ℕ), (↑k + 1) * x ^ (k + 1) = x / (1 - x) ^ 2

theorem tsum_geometric_of_lt_1_pow_succ {x : ℝ} (hx1 : x < 1) (hx2 : 0 < x) :

∑' (k : ℕ), x ^ (k + 1) = x / (1 - x)

theorem nnreal.tsum_eq_zero_add {f : ℕ → nnreal} (hf : summable f) :

∑' (b : ℕ), f b = f 0 + ∑' (b : ℕ), f (b + 1)

theorem nnreal.tsum_coe_mul_geometric_of_norm_lt_1 {r : nnreal} (hr : r < 1) :

∑' (n : ℕ), ↑n * r ^ n = r / (1 - r) ^ 2