[KADIRI]: Von Mangoldt sum as a Mellin integral (equation (11))

[teorth]

Description

Should follow from Laplace inversion and rearranging sums. Main difficulty is to justify interchange of the summation and contour integral.

Blueprint

Sublemma 8.5.2

Zulip

Link

[Robby955]

The stated form of eq. (11) appears to use a whole-line Bochner integral over ℝ of
(-ζ'/ζ)((1+a)+it) * Φ(-((1+a)+it)).

Under the current C¹-with-decay hypotheses on φ, one integration by parts gives only
Φ(σ+it) = O(1 / ‖t‖) on vertical strips. On the line σ = 1+a > 1, -ζ'/ζ is bounded, so the resulting integrand is generally only O(1 / ‖t‖), which is not absolutely integrable over ℝ.

So the whole-line Bochner-integral formulation seems stronger than what the current hypotheses support. This also matches Kadiri’s Theorem 3.1 setup: the vertical integral is handled as a symmetric truncated limit I(T) as T → ∞, rather than as an absolutely convergent integral over all of ℝ.

A faithful recut under the same C¹ hypotheses would be something like:

Tendsto (fun T => I φ a T) atTop (𝓝 (∑' n, Λ n * φ (Real.log n)))

using the blueprint’s truncated integral I(T). I have a sorry-free proof of that truncated-limit form.

The alternative is to strengthen the test-function hypotheses, for example to a C² condition with the corresponding endpoint/decay assumptions. Then a second integration by parts gives Φ(σ+it) = O(1 / ‖t‖²), which should restore absolute convergence of the whole-line integral. However I note this carefully because this does seem to have implications regarding the maintainers blueprint

[teorth]

Ah, yes, one this is an improper integral rather than a Bochner integral, and the change you suggest makes sense. (It will impact some downstream theorems, but most of these should be sorried currently.)

[Robby955]

claim

[Robby955]

propose #1603