Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

∣Mν(w)−1∣≪∥w∥|\mathcal M\nu(w)-1|\ll\|w\|∣Mν(w)−1∣≪∥w∥ on the strip, for a mass-one kernel

Proved
Vino.mellin_sub_one_le

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

analytic-number-theoryasymptoticsmellin-transformpnt

Let ν\nuν be a C1C^{1}C1 kernel supported in [1/2,2][1/2,2][1/2,2] with multiplicative mass one,

∫0∞ν(x) dxx=1.\int_0^{\infty}\nu(x)\,\frac{dx}{x}=1 .∫0∞​ν(x)xdx​=1.

Then there is a constant C>0C>0C>0, depending only on ν\nuν, such that for every www in the strip 0<Re⁡w≤10<\operatorname{Re}w\le10<Rew≤1,

∣Mν(w)−1∣  ≤  C∥w∥,\bigl|\mathcal M\nu(w)-1\bigr|\;\le\;C\|w\|,​Mν(w)−1​≤C∥w∥,

where Mν(w)=∫0∞ν(x)xw−1dx\mathcal M\nu(w)=\int_0^{\infty}\nu(x)x^{w-1}dxMν(w)=∫0∞​ν(x)xw−1dx.

The mass-one hypothesis is exactly the statement Mν(0)=1\mathcal M\nu(0)=1Mν(0)=1, so the estimate is a Lipschitz bound for Mν\mathcal M\nuMν measured from the origin — but valid on the whole strip, with Im⁡w\operatorname{Im}wImw unrestricted, rather than only in a neighbourhood of 000. One may take C=3A+1C=3A+1C=3A+1 with A=∫0∞∣ν(x)∣ dx/xA=\int_0^\infty|\nu(x)|\,dx/xA=∫0∞​∣ν(x)∣dx/x.

This is the analytic engine behind the estimate ∣M1ε~(p)−p−1∣≤Cε\bigl|\mathcal M\widetilde{1_\varepsilon}(p)-p^{-1}\bigr|\le C\varepsilon​M1ε​​(p)−p−1​≤Cε for the smoothed cutoff: by the factorisation M1ε~(p)=p−1Mν(εp)\mathcal M\widetilde{1_\varepsilon}(p)=p^{-1}\mathcal M\nu(\varepsilon p)M1ε​​(p)=p−1Mν(εp), that estimate is the present one applied at w=εpw=\varepsilon pw=εp, and the uniformity in Im⁡w\operatorname{Im}wImw is what allows ppp 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 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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me