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

Proved

IntMul.HvdH.expNeg_bound

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

integer-multiplication

Let $n,j\ge0$ and $k\ge1$ be integers and let $w$ = expNeg n k j (see IntMul_HvdH_RealExp). Then

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

This is Lemma 2.13 of Harvey–van der Hoeven for an explicit algorithm; these exponentials are the entries of the Gaussian resampling maps.

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 expNeg_bound (n k j : ℕ) (hk : 0 < k) :
    |(expNeg n k j : ℝ) - 2 ^ n * 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 e−πj/ke^{-\pi j/k}e−πj/k (Lemma 2.13)

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