Commit 2024-12-01 09:59 822e8564

View on Github →

feat(NumberTheory): Abel summation (#19289) Proof of several versions of Abel summation formula. This PR is part of the proof of the Analytic Class Number Formula.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Module.lean

added theorem Finset.sum_Ioc_by_parts

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral.lean

added theorem IntervalIntegrable.congr

Created Mathlib/NumberTheory/AbelSummation.lean

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