Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-17 06:22 7000efb8

View on Github →

refactor(analysis/specific_limits): split into two files (#12759) Split the 1200-line file analysis.specific_limits into two:

  • analysis.specific_limits.normed imports normed_space and covers limits in normed rings/fields
  • analysis.specific_limits.basic imports only topology, and is still a bit of a grab-bag, covering limits in metric spaces, ordered rings, ennreal, etc.

Estimated changes

added theorem ennreal.tsum_geometric
added theorem geom_le
added theorem geom_lt
added theorem has_sum_geometric_two'
added theorem has_sum_geometric_two
added theorem le_geom
added theorem lt_geom
added theorem sum_geometric_two_le
added theorem summable_geometric_two
added theorem tsum_geometric_inv_two
added theorem tsum_geometric_nnreal
added theorem tsum_geometric_of_lt_1
added theorem tsum_geometric_two'
added theorem tsum_geometric_two
deleted theorem ennreal.tsum_geometric
deleted theorem factorial_tendsto_at_top
deleted theorem geom_le
deleted theorem geom_lt
deleted theorem has_sum_geometric_of_lt_1
deleted theorem has_sum_geometric_two'
deleted theorem has_sum_geometric_two
deleted theorem le_geom
deleted theorem lt_geom
deleted theorem nnreal.has_sum_geometric
deleted theorem nnreal.summable_geometric
deleted theorem sum_geometric_two_le
deleted theorem summable_geometric_two'
deleted theorem summable_geometric_two
deleted theorem tendsto_at_top_of_geom_le
deleted theorem tsum_geometric_inv_two
deleted theorem tsum_geometric_inv_two_ge
deleted theorem tsum_geometric_nnreal
deleted theorem tsum_geometric_of_lt_1
deleted theorem tsum_geometric_two'
deleted theorem tsum_geometric_two