Integrability of $x^{a}\nu(x)$ for a compactly supported kernel

Proved

Vino.integrable_cpow_mul

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

analytic-number-theoryasymptoticsmellin-transformpnt

Let $\nu$ be continuous with $\operatorname{supp}\nu\subseteq[1/2,2]$ , and let $a\in\mathbb C$ . Then

x\longmapsto x^{a}\,\nu(x)

is integrable on $\mathbb R$ (hence on $(0,\infty)$ ), for every exponent $a$ — no convergence condition on $\operatorname{Re}a$ is needed.

Compact support inside $(0,\infty)$ removes both the singularity of $x^{a}$ at the origin and the growth at infinity, which is why the Mellin transform of such a kernel is entire. Stated in this form, the lemma is the integrability side condition for every manipulation of $\mathcal M\nu$ used in the Mellin calculus of the smoothed cutoff.

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_cpow_mul {ν : ℝ → ℝ} (contν : Continuous ν) (suppν : ν.support ⊆ Icc (1 / 2) 2) (a : ℂ) :
    Integrable (fun x : ℝ => (x : ℂ) ^ a * (ν 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

Integrability of xaν(x)x^{a}\nu(x)xaν(x) for a compactly supported kernel

Integrability of $x^{a}\nu(x)$ for a compactly supported kernel