LogInterval — Interval Arithmetic for Real.log via Bisection

Computes log(q) for rational q > 0 by bisecting against expPoint: find lo, hi such that exp(lo) ≤ q ≤ exp(hi), then refine by bisection.

Strategy

1. Initial bracket: log(q) ∈ [-(log₂(den)+1), log₂(num)+1] Uses bit lengths for a tight bracket proportional to log(q), not q itself. (since n < 2^(log₂ n + 1) ≤ exp(log₂ n + 1) for positive n)
2. Bisect 50 iterations: check exp(mid) vs q using expPoint bounds
3. Return [lo, hi] as QInterval containing Real.log q

Precision

50 bisection iterations on a bracket of width W give precision W/2^50 ≈ W × 10⁻¹⁵. Bracket width is log₂(num) + log₂(den) + 2, so for 64-bit rationals: W ≤ 130, precision ≈ 1.2 × 10⁻¹³.

def Linglib.Interval.logIterations : ℕ

Number of bisection iterations.

Equations

• Linglib.Interval.logIterations = 50

def Linglib.Interval.logPoint (q : ℚ) (_hq : 0 < q) : QInterval

Point interval containing log(q) for rational q > 0.

Initial bracket: [-(Nat.log 2 q.den + 1), Nat.log 2 q.num.natAbs + 1]. This uses bit lengths instead of raw values, giving a bracket width proportional to log₂(q) rather than q itself — critical for large-denominator rationals from interval arithmetic chains.

Lower: exp(-(log₂ d + 1)) < 1/d ≤ q since d < 2^(log₂ d + 1) ≤ exp(log₂ d + 1). Upper: q ≤ p ≤ exp(log₂ p + 1) by the same argument.

50 bisection iterations narrow this to precision bracket_width / 2^50.

Equations

• One or more equations did not get rendered due to their size.

theorem Linglib.Interval.logPoint_containsReal (q : ℚ) (hq : 0 < q) : (logPoint q hq).containsReal (Real.log ↑q)

Containment theorem for logPoint: the bisection invariant exp(lo) ≤ q ≤ exp(hi) implies lo ≤ log(q) ≤ hi by monotonicity of log.

def Linglib.Interval.logInterval (I : QInterval) (hI : 0 < I.lo) : QInterval

Interval containing log(x) for x in a positive rational interval I.

Uses monotonicity of log: for x ∈ [lo, hi] with lo > 0, log(lo) ≤ log(x) ≤ log(hi) so log(x) ∈ [logPoint(lo).lo, logPoint(hi).hi].

Equations

• Linglib.Interval.logInterval I hI = { lo := (Linglib.Interval.logPoint I.lo hI).lo, hi := (Linglib.Interval.logPoint I.hi ⋯).hi, valid := ⋯ }

theorem Linglib.Interval.logInterval_containsReal {I : QInterval} {x : ℝ} (hI : 0 < I.lo) (hx : I.containsReal x) : (logInterval I hI).containsReal (Real.log x)

Containment theorem for logInterval: monotonicity of log + logPoint containment.

theorem Linglib.Interval.log_zero_containsReal {I : QInterval} {x : ℝ} (hx : I.containsReal x) (hlo : 0 ≤ I.lo) (hhi : I.hi ≤ 0) : (QInterval.exact 0).containsReal (Real.log x)

When the argument is known to be zero (from interval [0,0]), Real.log x = Real.log 0 = 0, contained in exact 0.