Integrability of the multiplicative mass density

Proved

Vino.integrable_abs_div

by tabbott · Sep 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

analytic-number-theoryasymptoticsmellin-transformpnt

For $\nu$ continuous with support in $[1/2,2]$ , the density

x\longmapsto \frac{|\nu(x)|}{x}

is integrable. Its integral $A=\int_0^{\infty}|\nu(x)|\,dx/x$ is the total multiplicative mass of $|\nu|$ , and it is the constant that governs every bound on the Mellin transform of $\nu$ : $|\mathcal M\nu(w)|\le 2A$ throughout the strip $0<\operatorname{Re}w\le1$ , and $|\mathcal M\nu(w)-1|\le 3A\|w\|$ when $\nu$ has mass one.

Preamble

import Mathlib.Analysis.MellinTransform
import Mathlib.Analysis.SpecialFunctions.Pow.Complex
import Mathlib.Analysis.Complex.Exponential
open Set MeasureTheory Complex

Formal statement

namespace Vino

theorem integrable_abs_div {ν : ℝ → ℝ} (contν : Continuous ν) (suppν : ν.support ⊆ Icc (1 / 2) 2) :
    Integrable (fun x : ℝ => |ν x| / x) := by sorry

end Vino

Source

A. Kontorovich et al., PrimeNumberTheoremAnd, https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/master/PrimeNumberTheoremAnd/MellinCalculus.lean (the `MellinOfSmooth1a/b/c` family and the smoothed cutoff `Smooth1`); H. Davenport, Multiplicative Number Theory, 3rd ed., Springer GTM 74, 2000, Chapter 17 (Perron's formula and the smoothed Chebyshev function).

View graph