Euler-Maclaurin, Poisson summation

Stream: PrimeNumberTheorem+

[Harald Helfgott]

Have Euler-Maclaurin and Poisson summation already been formalized? If so, where, and in what generality?

(Meta-question: how do I find this sort of thing out myself?)

[Matteo Cipollina]

Helpful tools are Leansearch, https://deepwiki.com/leanprover-community/mathlib4 and https://www.leanexplore.com
e.g.
https://leansearch.net/?q=poisson+summation

[Harald Helfgott]

Thank you!

I'm finding Poisson summation but not Euler-Maclaurin, oddly. Where is it hiding?

[Matteo Cipollina]

It is not yet in mathlib, here is a step towards it:
https://github.com/leanprover-community/mathlib4/pull/32364

[Harald Helfgott]

I'm not finding it. Do we at least have first-order Euler-Maclaurin? That's all I need.

[Harald Helfgott]

@Matteo Cipollina That may have been on me - now I can see the thread. However, I cannot see a blueprint, or even Lean code. Sorry for the newbie question, but where do I find them? Where do I click?

[Matteo Cipollina]

Sorry if that was a bit cyptic, the lean code in that PR is mostly contained in Mathlib.Analysis.Calculus.ContDiff.Polynomial. No blueprint is provided for mathlib files, they tend to have self-contained doc-strings instead.

[Harald Helfgott]

@Matteo Cipollina All I see is the statement that polynomials are smooth. I just want to know what I can assume in a blueprint. Do we have the following statement (first-order Euler-Maclaurin), or one very close to it? In the latter case, what is it exactly?

Let $a,b\in \mathbb{R}$, $a<b$. Let $f:[a,b]\to \mathbb{C}$ be absolutely continuous. Then
$\sum_{a<n\leq b} f(n) = \int_a^b f(x) dx - ((\{b\}-1/2) f(b) - (\{a\}-1/2) f(a)) + \int_a^b (\{x\}-1/2) f'(x) dx.$

[Matteo Cipollina]

Unfortunately I suspect that the statement under the assumptions you need would require new infrastructure (either a new FTC/IBP theorem for absolutely continuous functions using an ae. derivative, or a refactor of Abel summation to accept ae. differentiability
The below statement assuming continuously differentiable is possibly the closest that can be stated with available mathlib, still someone more familiar with the ongoing PRs may have a better picture of the situation:

import Mathlib

open scoped Real

variable {f : ℝ → ℂ}

/-- **First-order Euler–Maclaurin with fractional part**
We assume `ContDiffOn ℝ 1 f (Icc a b)` (continuously differentiable),
which is sufficient for the first-order case.
-/
theorem first_order_euler_maclaurin_fract {a b : ℝ} (hab : a ≤ b)
    (hf : ContDiffOn ℝ 1 f (Set.Icc a b)) :
    (∑ n ∈ Finset.Icc (Int.floor a + 1) (Int.floor b), f n) =
      (∫ x in a..b, f x) -
        (((Int.fract b - (1 / 2 : ℝ)) • f b) - ((Int.fract a - (1 / 2 : ℝ)) • f a)) +
        ∫ x in a..b, ((Int.fract x - (1 / 2 : ℝ)) • deriv f x) := by
  sorry

[Harald Helfgott]

That's enough for the application I have in my hands right now, but IMHO we really need statements with weaker assumptions, in general (either AC or even BV).

[Alex Kontorovich]

Harald Helfgott said:

Do we have the following statement (first-order Euler-Maclaurin), or one very close to it? In the latter case, what is it exactly?

Let $a,b\in \mathbb{R}$, $a<b$. Let $f:[a,b]\to \mathbb{C}$ be absolutely continuous. Then
$\sum_{a<n\leq b} f(n) = \int_a^b f(x) dx - ((\{b\}-1/2) f(b) - (\{a\}-1/2) f(a)) + \int_a^b (\{x\}-1/2) f'(x) dx.$

Yes, this was proved a while ago in PNT+, see Lemma 3.4.1

[Harald Helfgott]

Right, that's what Matteo just said; thanks. As I said, it would be best not to assume $C^1$ needlessly, but the function I am working with right now is in fact in $C^1$.

[Harald Helfgott]

Now there's an issue with Poisson summation. While the version in mathlib is labelled "most general form", it isn't, and, in particular, it's not general enough for the rather ordinary application I have in my hands. (Read: it won't be the last time this happens.) It would be good to have something like the version I'm attaching, from Montgomery-Vaughan, vol I, Appendix D. My f is actually compactly supported, but Montgomery-Vaughan's assumptions seem to me to have the right amount of generality.

What to do then? The version in mathlib assumes $\widehat{f}$ is summable (and that doesn't hold in general, or in my case).
image.png

[Harald Helfgott]

In the proof in M-V, (D.2) is just this:
image.png

[Ruben Van de Velde]

#maths > Euler-Maclaurin formula

[Harald Helfgott]

Do you think we can issue this form of Poisson summation and its proof (as they stand in M-V) as a blueprint, or is more detail needed?

[Yongxi Lin (Aaron)]

Harald Helfgott said:

Now there's an issue with Poisson summation. While the version in mathlib is labelled "most general form", it isn't, and, in particular, it's not general enough for the rather ordinary application I have in my hands. (Read: it won't be the last time this happens.) It would be good to have something like the version I'm attaching, from Montgomery-Vaughan, vol I, Appendix D. My f is actually compactly supported, but Montgomery-Vaughan's assumptions seem to me to have the right amount of generality.

What to do then? The version in mathlib assumes $\widehat{f}$ is summable (and that doesn't hold in general, or in my case).
image.png

I would like to push back slightly on the claim that the Mathlib version is not general. The theorem in MV is of a genuinely different nature, since the convergence of the Fourier coefficients there is not unconditional, whereas the Mathlib version assumes unconditional convergence. For this reason, I think it would be both nice and essentially important to eventually have both versions available in Mathlib.

[Yongxi Lin (Aaron)]

Harald Helfgott said:

Do you think we can issue this form of Poisson summation and its proof (as they stand in M-V) as a blueprint, or is more detail needed?

The version for functions of bounded variation is definitely not easy to formalize and I believe it should not be a single issue. I am pretty sure we don't have the theorem about the convergence of Fourier series (D.2 in the picture above) and integration by parts for functions of bounded variation in Mathlib.

[Harald Helfgott]

Hi @Yongxi Lin (Aaron) -

I would like to push back slightly on the claim that the Mathlib version is not general.

Let me reply equally gently. What I objected to was not the Mathlib version, or the claim that is general, but rather the claim in its description that it is most general.

For this reason, I think it would be both nice and essentially important to eventually have both versions available in Mathlib.

I agree.

[Harald Helfgott]

@Yongxi Lin (Aaron) said:

The version for functions of bounded variation is definitely not easy to formalize and I believe it should not be a >single issue. I am pretty sure we don't have the theorem about the convergence of Fourier series (D.2 in the >picture above) and integration by parts for functions of bounded variation in Mathlib.

Then this is an excellent opportunity to formalize some basic analytic statements -- starting with the two you mention -- for functions of bounded variation.

Yes, it is not a single issue: lots of folks will need statements in greater generality than $C^1$, and the natural setting for many statements is broader than $C^1$. This is not about pathological functions or edge cases. Plenty of bread-and-butter functions in analysis and applications of analysis -- say, to analytic number theory -- are not $C^1$.

I think we have two options: either

1. gradually generalize basic statements (integration by parts, Euler-Maclaurin, convergence of Fourier series, etc.) to a growing list of classes of functions (piecewise C^1 functions, functions with a finite number of points of discontinuity, etc.), or
2. choose a broad class of functions that

• covers many such cases
• is natural from the point of view of the proofs.
  Or two classes, say, at most; not more.

To me, the second option seems clearly preferable, both from the point of view of proof and usage (or "mathematics" and "engineering" if you prefer).

For this kind of practical statements in analysis, the two plausible candidates for such "broad classes" seem to me to be:

• functions of bounded variation,
• absolutely continuous functions.
  People: if I am missing anything, please tell me.

The function I'm dealing with right now ($1_{[a,b} t^{-s}$) is of bounded variation but not absolutely continuous, or even continuous. Functions like this come up all the time in analytic number theory.

Since absolutely continuous functions are of bounded variation on compact intervals, the simplest option seems to be to prove things with the condition:

• bounded variation on $[a,b]$
  whenever possible. This is often the weakest condition that makes a statement true and straightforward to prove. Then we can have additional conditions if they are really needed: AC, global BV (i.e., total variation $<\infty$ on all of $\mathbb{R}$), etc.

This would give us a stable class that would cover plenty of others, accommodating the smoother cases as special instances. Even for those special instances, it would be good to settle on a small number of "standard" regimes, rather than multiplying them. One such regime is $C^1$, which is used in much of Mathlib already. Absolute continuity would be another sensible regime; often statements that are proved for piecewise $C^1$ functions, say, can be proved just as easily assuming AC.

[Sébastien Gouëzel]

Current status of these things in Mathlib: We have functions of bounded variation (docs#BoundedVariationOn), with a basic API. So it could be used today to state and prove theorems (this would probably highlight a lot of gaps in the API, but this is well and good). We don't have absolutely continuous functions yet, but there is a series of PRs by @Yizheng Zhu bringing them to mathlib (#29092 has been split into smaller pieces).

[Harald Helfgott]

Thank you, @Sébastien Gouëzel.

What may be more up for discussion is which condition (weaker than $C^k$) we should use when we want, say, Euler-Maclaurin to the $k$th order, or bounds such as $\leq C_k/|t|^k$ on the Fourier transform. A natural candidate seems to be "let $f\in L^1$ be such that the $k$th distributional derivative $D^k$ is a finite signed measure", but I'm all ears as to alternatives.

For $k=2$, in particular, there is at least one alternative which is equivalent mathematically but not at the level of language. (I don't mean W^{2,1}, which is too restrictive.) Among choices of the right strength -- or what that amounts to: reusability -- we should probably use whatever makes proofs more natural. Note that both $k$th-order Euler Maclaurin and the above bound on the Fourier transform are proved by iteration.