on the strip, for a mass-one kernel
ProvedVino.mellin_sub_one_leanalytic-number-theoryasymptoticsmellin-transformpnt
Let be a kernel supported in with multiplicative mass one,
Then there is a constant , depending only on , such that for every in the strip ,
where .
The mass-one hypothesis is exactly the statement , so the estimate is a Lipschitz bound for measured from the origin — but valid on the whole strip, with unrestricted, rather than only in a neighbourhood of . One may take with .
This is the analytic engine behind the estimate for the smoothed cutoff: by the factorisation , that estimate is the present one applied at , and the uniformity in is what allows to range over a full vertical line.
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 mellin_sub_one_le {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (suppν : ν.support ⊆ Icc (1 / 2) 2)
(mass_one : ∫ x in Ioi (0 : ℝ), ν x / x = 1) :
∃ C : ℝ, 0 < C ∧ ∀ w : ℂ, 0 < w.re → w.re ≤ 1 →
‖mellin (fun x ↦ (ν x : ℂ)) w - 1‖ ≤ C * ‖w‖ := by sorry
end VinoSource
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).