Abel's summation and/or Stieltjes integration

Stream: Is there code for X?

[Meow]

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]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/analytical.20number.20theory/near/320708370

[David Loeffler]

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]

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]

Yes, that's my opinion.

[Xavier Roblot]

I have an almost complete proof of Abel summation formula (just a couple of easy sorries to fill in) but I wanted to make sure it is the right formulation / hypotheses before going further. Basically, what I have is the following:

import Mathlib

open Finset intervalIntegral MeasureTheory

variable (c : ℕ → ℂ) (f : ℝ → ℂ)

abbrev S : ℝ → ℂ := fun t ↦ ∑ n ∈ range (⌊t + 1⌋₊), c n

theorem AbelSummation {x : ℝ}
    (h_diff : ∀ t ∈ Set.Icc (0 : ℝ) x, DifferentiableAt ℝ f t)
    (h_integ : IntervalIntegrable (deriv f) volume 0 x) :
    ∑ k ∈ range (⌊x + 1⌋₊), c k * f k = S c x * f x - ∫ t in (0 : ℝ)..x, S c t * deriv f t := by sorry

[Ruben Van de Velde]

Oh, I have a proof in PNT+

[Ruben Van de Velde]

https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/191

[Xavier Roblot]

Are you planning on PR'ing it soon?

[Xavier Roblot]

Also, you use docs#ContinuousOn and I use docs#IntervalIntegrable. One question I have is which one is better in general?

[Ruben Van de Velde]

I have no opinion - I just bashed out something that would work in the case I needed. I had no immediate plans to PR it to mathlib, but I can try to get around to it (or you could, if you have time)

[Vincent Beffara]

How far is this from docs#Finset.sum_range_by_parts plus docs#intervalIntegral.integral_deriv_eq_sub plus docs#intervalIntegral.sum_integral_adjacent_intervals ?

[Xavier Roblot]

Vincent Beffara said:

How far is this from docs#Finset.sum_range_by_parts plus docs#intervalIntegral.integral_deriv_eq_sub plus docs#intervalIntegral.sum_integral_adjacent_intervals ?

This is basically my proof

[Xavier Roblot]

It's pretty straightforward

[Xavier Roblot]

@Ruben Van de Velde I have a version of Abel summation here that I am reasonably happy with and I would like to PR it if you don't mind since I'll need it at some point for the proof of the analytic class number formula. It just needs a good name, a place to live and probably also some golfing

[Ruben Van de Velde]

No, don't mind at all

[Xavier Roblot]

Thanks! I'll be also very interested in your review once it's ready :wink:

[Xavier Roblot]

And any suggestion for names and/or location !

[Ruben Van de Velde]

Please ping me on zulip if you want me to review, I'm in permanent github notification bankrupcy

[Kevin Buzzard]

Do you want some of my notifications?

[Xavier Roblot]

@Ruben Van de Velde , the PR is ready: #19289