Prove2Me

Fixed-point real exponentials e−πj/ke^{-\pi j/k} and 2−σeπj/k2^{-\sigma}e^{\pi j/k} (Harvey–van der Hoeven Lemmas 2.13–2.14)

Definition
IntMul_HvdH_RealExp

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

integer-multiplication

Computable integer approximations of real exponentials.

  • expNegFix n M X approximates 2neX/2M2^n e^{X/2^M} for an integer X≤0X\le0: writing X/2M=z−τlog⁡2X/2^M=z-\tau\log 2 with τ=⌊−X/L⌋\tau=\lfloor -X/L\rfloor, where LL = log2Bits M, it approximates 2Mez2^Me^{z} with expBits and divides by 2M−n+τ2^{M-n+\tau}, rounding to nearest.
  • expNeg n k j approximates 2ne−πj/k2^n e^{-\pi j/k}: it returns 00 when j>knj>kn and otherwise applies expNegFix at precision M=2n+10M=2n+10 to −⌊piBits(M) j/k⌋-\lfloor \mathrm{piBits}(M)\,j/k\rfloor.
  • expPos n k j σ approximates 2n 2−σeπj/k2^n\,2^{-\sigma}e^{\pi j/k} by applying expNegFix to min⁡(0,⌊piBits(M) j/k⌋−σ log2Bits(M))\min(0,\lfloor \mathrm{piBits}(M)\,j/k\rfloor-\sigma\,\mathrm{log2Bits}(M)).
Definition code
import Definitions.Def_IntMul_HvdH_Numeric
import Definitions.Def_IntMul_HvdH_ExpApprox

/-! Fixed-point real exponentials `e^{-πj/k}` and `2^{-σ} e^{πj/k}`
(Harvey–van der Hoeven Lemmas 2.13 and 2.14). -/

namespace IntMul.HvdH

/-- Approximation of `2^n exp(X / 2^M)` for `X ≤ 0`: write `X / 2^M = z - τ log 2` with
`z ∈ (-log 2, 0]` (using the `M`-bit approximation `log2Bits M`), approximate `2^M e^z` with
`expBits`, and divide by `2^{M - n + τ}` with rounding to nearest. -/
def expNegFix (n M : ℕ) (X : ℤ) : ℤ :=
  let L := log2Bits M
  let τ := (-X) / L
  let u := (expBits M (X + τ * L) 0).1
  let s := M - n - 1 + τ.toNat
  (u + 2 ^ s) / 2 ^ (s + 1)

/-- Approximation of `2^n e^{-πj/k}` (Lemma 2.13). -/
def expNeg (n k j : ℕ) : ℤ :=
  if k * n < j then 0
  else expNegFix n (2 * n + 10) (-(piBits (2 * n + 10) * j / k))

/-- Approximation of `2^n · 2^{-σ} e^{πj/k}`, meaningful when `e^{πj/k} ≤ 2^σ` (Lemma 2.14). -/
def expPos (n k j σ : ℕ) : ℤ :=
  expNegFix n (2 * n + 10)
    (min 0 (piBits (2 * n + 10) * j / k - σ * log2Bits (2 * n + 10)))

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