Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-17 07:44 abea2984

View on Github →

refactor(analysis/specific_limits): use ennreals instead of nnreals in *_edist_le_geometric (#1759)

  • feat(data/real/ennreal): more lemmas, *_cast tags, use lift tactic
  • Undo name change
  • Fix compile
  • nnreal: add move_cast
  • ennreal: more lemmas
  • Fix compile
  • feat(topology/instances/ennreal): more lemmas
  • Fix compile
  • Rewrite cauchy_seq_of_edist_le_geometric etc in terms of ennreals I tried to actually use nnreals, and it leads to coercions nightmare.
  • Simplify some proofs using new lemmas
  • Fix compile
  • Fix compile

Estimated changes

added theorem ennreal.tsum_geometric
deleted theorem has_sum_geometric_nnreal
deleted theorem summable_geometric_nnreal