$n$ -bit approximation of $2^{-\sigma}e^{\pi j/k}$ (Lemma 2.14)

Proved

IntMul.HvdH.expPos_bound

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

integer-multiplication

Let $n,j,\sigma\ge0$ and $k\ge1$ be integers with $e^{\pi j/k}\le2^\sigma$ and $\sigma\le2n$ , and let $w$ = expPos n k j σ (see IntMul_HvdH_RealExp). Then

\bigl|2^{-n}w-2^{-\sigma}e^{\pi j/k}\bigr|\le2^{-n}.

This is Lemma 2.14 of Harvey–van der Hoeven for an explicit algorithm.

Preamble

import Definitions.Def_IntMul_HvdH_RealExp
import Theorems.Thm_IntMul_HvdH_piBits_bound
import Theorems.Thm_IntMul_HvdH_log2Bits_bound
import Theorems.Thm_IntMul_HvdH_expBits_bound

Formal statement

namespace IntMul.HvdH
theorem expPos_bound (n k j σ : ℕ) (hk : 0 < k) (hσ : Real.exp (Real.pi * j / k) ≤ 2 ^ σ)
    (hσn : σ ≤ 2 * n) :
    |(expPos n k j σ : ℝ) - 2 ^ n * ((2 ^ σ)⁻¹ * Real.exp (Real.pi * j / k))| ≤ 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, Lemmas 2.13 and 2.14 (real exponentials)

View graph

nnn-bit approximation of 2−σeπj/k2^{-\sigma}e^{\pi j/k}2−σeπj/k (Lemma 2.14)

$n$ -bit approximation of $2^{-\sigma}e^{\pi j/k}$ (Lemma 2.14)