Commit 2024-02-15 20:01 dc082806

View on Github →

chore(CauSeq): Cleanup (#10530)

  • Rename Data.Real.CauSeq to Algebra.Order.CauSeq.Basic
  • Rename Data.Real.CauSeqCompletion to Algebra.Order.CauSeq.Completion
  • Move the general lemmas about CauSeq from Data.Complex.Exponential to a new file Algebra.Order.CauSeq.BigOperators
  • Move the lemmas mentioning Module from Algebra.BigOperators.Intervals to a new file Algebra.BigOperators.Module
  • Move a few more lemmas to earlier files
  • Deprecate abv_sum_le_sum_abv as it's a duplicate of IsAbsoluteValue.abv_sum

Estimated changes

deleted theorem Finset.sum_Ico_by_parts
deleted theorem Finset.sum_range_by_parts
modified theorem CauSeq.bounded'
modified theorem CauSeq.bounded
modified def CauSeq.const
added theorem IsCauSeq.bounded'
added theorem IsCauSeq.bounded
added theorem IsCauSeq.const
added theorem IsCauSeq.mul
deleted theorem exists_forall_ge_and
added theorem isCauSeq_neg
added theorem IsCauSeq.geo_series
added theorem IsCauSeq.of_abv
added theorem IsCauSeq.of_abv_le
added theorem cauchy_product
deleted theorem abv_sum_le_sum_abv
deleted theorem cauchy_product
deleted theorem isCauSeq_geo_series
deleted theorem isCauSeq_geo_series_const
deleted theorem isCauSeq_of_mono_bounded
deleted theorem series_ratio_test
deleted theorem sum_range_diag_flip
added theorem exists_forall_ge_and