mathlib3

9bb69dca - feat(analysis/specific_limits): add `cauchy_seq_of_edist_le_geometric` (#1743)

feat(analysis/specific_limits): add `cauchy_seq_of_edist_le_geometric` (#1743) * feat(analysis/specific_limits): add `cauchy_seq_of_edist_le_geometric` Other changes: * Estimates on the convergence rate both in `edist` and `dist` cases. * Swap lhs with lhs in `ennreal.tsum_coe` and `nnreal.tsum_coe`, rename accordingly * Use `(1 - r)⁻¹` instead of `1 / (1 - r)` in `has_sum_geometric` * Add some docstrings * Update src/analysis/specific_limits.lean