Verified Argument Reduction for Logarithm #

This file provides argument reduction for computing log(q) using the identity: log(q) = log(m) + k * log(2) where m = q * 2^(-k) is in a "good" range [1/2, 2] for Taylor series convergence.

Main definitions #

reductionExponent - Find k such that q * 2^(-k) is in [1/2, 2]
reduceMantissa - The reduced mantissa m = q * 2^(-k)

Main theorems #

reconstruction_eq - Algebraic identity: q = m * 2^k
reduced_bounds - Bounds on m: 1/2 ≤ m ≤ 2 for q > 0

Design notes #

This reduction allows us to use the rapidly converging atanh-based series: log(m) = 2 * atanh((m-1)/(m+1)) For m ∈ [1/2, 2], we have (m-1)/(m+1) ∈ [-1/3, 1/3], where atanh converges very fast.

Argument Reduction #

source

def LeanCert.Core.LogReduction.reductionExponent (q : ℚ) :

ℤ

Find k such that q * 2^(-k) is approximately in [1/2, 2]. Implementation: k = log2(num) - log2(den) approximately.

Equations

LeanCert.Core.LogReduction.reductionExponent q = if q ≤ 0 then 0 else have n_log := q.num.natAbs.log2; have d_log := q.den.log2; ↑n_log - ↑d_log

Instances For

source

def LeanCert.Core.LogReduction.reduceMantissa (q : ℚ) :

ℚ

The reduced mantissa m = q * 2^(-k).

Equations

LeanCert.Core.LogReduction.reduceMantissa q = if q ≤ 0 then 1 else have k := LeanCert.Core.LogReduction.reductionExponent q; q * 2 ^ (-k)

Instances For

source

theorem LeanCert.Core.LogReduction.reconstruction_eq {q : ℚ} (hq : 0 < q) :

have k := reductionExponent q; have m := reduceMantissa q; q = m * 2 ^ k

The main algebraic theorem: q = m * 2^k for positive q

source

theorem LeanCert.Core.LogReduction.reduced_bounds_weak {q : ℚ} (hq : 0 < q) :

have m := reduceMantissa q; 1 / 4 ≤ m ∧ m ≤ 4

The reduced mantissa is bounded: 1/4 ≤ m ≤ 4 for q > 0. (We use slightly weaker bounds than [1/2, 2] for simpler proofs, but the series still converges rapidly.)

source