$|\log x|\le\log 2$ on $[1/2,2]$

Proved

Vino.abs_log_le_log_two

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

analytic-number-theoryasymptoticsmellin-transformpnt

For every $x$ in the dyadic interval $[1/2,2]$ ,

|\log x|\le\log 2 .

The interval $[1/2,2]$ is where mollifiers of the Mellin calculus live: a smoothing kernel $\nu$ used to build the smoothed cutoff $\widetilde{1_\varepsilon}$ is supported there. Bounding $|\log x|$ on the support is the first step in every estimate of $x^{w}=e^{w\log x}$ against $\|w\|$ .

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 abs_log_le_log_two {x : ℝ} (hx1 : 1/2 ≤ x) (hx2 : x ≤ 2) : |Real.log x| ≤ Real.log 2 := 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

∣log⁡x∣≤log⁡2|\log x|\le\log 2∣logx∣≤log2 on [1/2,2][1/2,2][1/2,2]

$|\log x|\le\log 2$ on $[1/2,2]$