$|x^{w}-1|\le 3\|w\|$ on the dyadic interval

Proved

Vino.norm_cpow_sub_one_le

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

analytic-number-theoryasymptoticsmellin-transformpnt

Let $x\in[1/2,2]$ and let $w$ be a complex number with $0<\operatorname{Re}w\le1$ . Then

\bigl|x^{w}-1\bigr|\;\le\;3\|w\|,

with an absolute constant and no restriction on $\operatorname{Im}w$ .

The point is the uniformity in the imaginary direction. For $\|w\|\le1$ the estimate is the first-order expansion $x^{w}-1=e^{w\log x}-1=O(|w\log x|)$ ; for $\|w\|\ge1$ it is the trivial bound $|x^{w}|=x^{\operatorname{Re}w}\le2$ , which is already $\le3\|w\|$ . Splitting this way is what makes the estimate valid on the whole strip rather than only near the origin, and that is exactly what a Mellin transform evaluated along a vertical line requires.

Preamble

import Mathlib.Analysis.SpecialFunctions.Pow.Complex
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.Complex.Exponential
import Mathlib.Analysis.SpecialFunctions.Log.Basic
open Set Complex

Formal statement

namespace Vino

theorem norm_cpow_sub_one_le {x : ℝ} (hx1 : 1/2 ≤ x) (hx2 : x ≤ 2) {w : ℂ} (hw0 : 0 < w.re) (hw1 : w.re ≤ 1) :
    ‖(x : ℂ) ^ w - 1‖ ≤ 3 * ‖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

∣xw−1∣≤3∥w∥|x^{w}-1|\le 3\|w\|∣xw−1∣≤3∥w∥ on the dyadic interval

$|x^{w}-1|\le 3\|w\|$ on the dyadic interval