Commit 2025-01-07 20:32 22296704

View on Github →

feat(NumberTheory/AbelSummation): add more results (#19942)

Add versions for when the endpoints are Nat (for convenience).
Add limit versions for when the endpoint tends to infinity.
Add summability criteria using Abel summation

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Normed/Module/FiniteDimension.lean

added theorem summable_of_sum_range_norm_le

Modified Mathlib/NumberTheory/AbelSummation.lean

modified theorem sum_mul_eq_sub_integral_mul'

added theorem sum_mul_eq_sub_integral_mul₀'

added theorem sum_mul_eq_sub_integral_mul₀

added theorem sum_mul_eq_sub_sub_integral_mul'

added theorem summable_mul_of_bigO_atTop'

added theorem summable_mul_of_bigO_atTop

added theorem tendsto_sum_mul_atTop_nhds_one_sub_integral

added theorem tendsto_sum_mul_atTop_nhds_one_sub_integral₀

Created Mathlib/Topology/Order/IsLocallyClosed.lean

added theorem isLocallyClosed_Icc

added theorem isLocallyClosed_Ici

added theorem isLocallyClosed_Ico

added theorem isLocallyClosed_Iic

added theorem isLocallyClosed_Iio

added theorem isLocallyClosed_Ioc

added theorem isLocallyClosed_Ioi

added theorem isLocallyClosed_Ioo