$n$ -bit approximation of $\log 2$

Proved

IntMul.HvdH.log2Bits_bound

by xuanji · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

integer-multiplication

For every $n\ge0$ the integer log2Bits n (from $\log 2=2\operatorname{artanh}\frac13$ with truncated, floor-rounded series to $2n+9$ bits, then rounded to $n$ bits; see IntMul_HvdH_Numeric) satisfies $|\mathrm{log2Bits}(n)-2^n\log 2|\le 1$ .

Preamble

import Definitions.Def_IntMul_HvdH_Numeric

Formal statement

namespace IntMul.HvdH
theorem log2Bits_bound (n : ℕ) : |(log2Bits n : ℝ) - 2 ^ n * Real.log 2| ≤ 1 := by sorry
end IntMul.HvdH

Source

Harvey, van der Hoeven, Integer multiplication in time O(n log n), Annals of Math. 193 (2021), https://hal.science/hal-02070778, Section 2.8 (computing pi and log 2 to p bits)

View graph

nnn-bit approximation of log⁡2\log 2log2

$n$ -bit approximation of $\log 2$