Commit 2024-09-02 07:21 197868c8

feat: remove completeness assumption in the formula for ∑ n, n * r ^ n (#15270) Currently, the formula ∑ n, n * r ^ n = r / (1 - r) ^ 2 in a field assumes that the field is complete to get summability of the series from the summability of the norms. However, as ∑ r ^ n is converging (to 1 / (1 - r)), the summability of the Cauchy product is automatic thanks to a variation around results we already have, so completeness can be removed. In the same way, ∑ n ^ k * r ^ n is summable without completeness assumptions. The proof is a little bit indirect (first get summability of ∑ n, (n + k).choose k * r ^ n for each k, as this is (∑ r ^ n) ^ k, and then deduce the other one), but it gives the nice formula ∑ n, (n + k).choose k * r ^ n = 1 / (1 - r) ^ k along the way, which is nice to have. This is a preliminary PR before unifying several results between [NormedRing R] [CompleteSpace R] and [NontriviallyNormedField R], which are proved twice with very similar arguments at several places in mathlib.