Zulip Chat Archive
Stream: Is there code for X?
Topic: Abel's summation and/or Stieltjes integration
Meow (Jan 12 2023 at 11:16):
Is Abel's summation and Euler-Maclaurin summation formalized in Lean? In mathlib we have Stieltjes measure (for monotone functions), and Abel's summation is just the integration by part of Stieltjes integration.
Meow (Jan 12 2023 at 11:18):
David Loeffler (Jan 12 2023 at 11:26):
Euler-Maclaurin summation isn't in mathlib but it will be easy to add, since it doesn't need any new work on the measure-theory side.
David Loeffler (Jan 12 2023 at 11:29):
For Abel summation (assuming you mean the first statement here : https://en.wikipedia.org/wiki/Abel%27s_summation_formula), it might be easier to prove it more directly, rather than going through the work of defining the Stieltjes integral in the relevant settings.
Meow (Jan 12 2023 at 11:52):
Yes, that's my opinion.
Last updated: Dec 20 2023 at 11:08 UTC