Commit 2024-04-30 15:37 3a7e6bb7

View on Github →

chore: move summable lemmas (#12503) We move some lemmas out of Topology/Instances/ENNReal into Topology/Algebra/InfiniteSum/Real. Also use this to address a porting TODO. This was originally part of #12446

Estimated changes

Modified Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean

Modified Mathlib/Analysis/Normed/Field/InfiniteSum.lean

Modified Mathlib/Analysis/SpecificLimits/Basic.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Real.lean

added theorem Real.tsum_le_of_sum_range_le

deleted theorem cauchySeq_of_edist_le_of_summable

added theorem not_summable_iff_tendsto_nat_atTop_of_nonneg

added theorem summable_iff_not_tendsto_nat_atTop_of_nonneg

added theorem summable_of_sum_le

added theorem summable_of_sum_range_le

added theorem summable_prod_of_nonneg

added theorem summable_sigma_of_nonneg

added theorem tsum_lt_tsum_of_nonneg

Modified Mathlib/Topology/Instances/ENNReal.lean

deleted theorem Real.tsum_le_of_sum_range_le

added theorem cauchySeq_of_edist_le_of_summable

deleted theorem not_summable_iff_tendsto_nat_atTop_of_nonneg

deleted theorem summable_iff_not_tendsto_nat_atTop_of_nonneg

deleted theorem summable_of_sum_le

deleted theorem summable_of_sum_range_le

deleted theorem summable_prod_of_nonneg

deleted theorem summable_sigma_of_nonneg

deleted theorem tsum_lt_tsum_of_nonneg