Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-29 18:51 9bb69dca

View on Github →

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

Estimated changes

Modified src/analysis/specific_limits.lean

added theorem aux_has_sum_of_le_geometric

added theorem cauchy_seq_of_edist_le_geometric

modified theorem cauchy_seq_of_le_geometric

added theorem cauchy_seq_of_le_geometric_two

added theorem dist_le_of_le_geometric_of_tendsto

added theorem dist_le_of_le_geometric_of_tendsto₀

added theorem dist_le_of_le_geometric_two_of_tendsto

added theorem dist_le_of_le_geometric_two_of_tendsto₀

added theorem edist_le_of_edist_le_geometric_of_tendsto

added theorem edist_le_of_edist_le_geometric_of_tendsto₀

added theorem has_sum_geometric_nnreal

added theorem summable_geometric_nnreal

modified theorem tsum_geometric

added theorem tsum_geometric_nnreal

Modified src/data/real/cardinality.lean

Modified src/measure_theory/probability_mass_function.lean

Modified src/topology/instances/ennreal.lean

added theorem edist_le_tsum_of_edist_le_of_tendsto

added theorem edist_le_tsum_of_edist_le_of_tendsto₀

Modified src/topology/instances/nnreal.lean

added theorem nnreal.coe_tsum

modified theorem nnreal.has_sum_coe

modified theorem nnreal.summable_coe

added theorem nnreal.summable_comp_injective

deleted theorem nnreal.tsum_coe