PadeExp — Padé Approximant for exp(x) with Interval Bounds

[4/4] Padé approximant for exp(x) on [-1, 1], with argument reduction for arbitrary x ∈ ℝ. The approximant has relative error < 10⁻⁷ on [-1,1], so the error bound 1/4000000 provides a 2.3× safety margin.

Strategy

For small |x| ≤ 1: exp(x) ≈ padeNum(x) / padeDen(x) (within padeErrorBound)

For large |x|:

1. Choose k so x/2^k ∈ [-1, 1]
2. Compute exp(x/2^k) via Padé
3. Square k times: exp(x) = exp(x/2^k)^(2^k)

def Linglib.Interval.padeNum (x : ℚ) : ℚ

Padé [4/4] numerator: 1 + x/2 + 3x²/28 + x³/84 + x⁴/1680 (Horner form).

Equations

• Linglib.Interval.padeNum x = 1 + x * (1 / 2 + x * (3 / 28 + x * (1 / 84 + x * (1 / 1680))))

def Linglib.Interval.padeDen (x : ℚ) : ℚ

Padé [4/4] denominator: padeNum(-x).

Equations

• Linglib.Interval.padeDen x = Linglib.Interval.padeNum (-x)

def Linglib.Interval.padeExp (x : ℚ) : ℚ

Padé [4/4] approximant: padeNum(x) / padeDen(x).

Equations

• Linglib.Interval.padeExp x = Linglib.Interval.padeNum x / Linglib.Interval.padeDen x

def Linglib.Interval.padeErrorBound : ℚ

Conservative error bound for Padé [4/4] on [-1, 1]. True error is ~4.3×10⁻⁸; this bound gives 2.3× safety margin.

Equations

• Linglib.Interval.padeErrorBound = 1 / 4000000

theorem Linglib.Interval.pade_error_bound (q : ℚ) (hq_lo : -1 ≤ q) (hq_hi : q ≤ 1) (hden_pos : 0 < padeDen q) : |Real.exp ↑q - ↑(padeExp q)| ≤ ↑padeErrorBound

The Padé [4/4] approximant is within padeErrorBound of exp on [-1, 1].

Proof via triangle inequality: |exp(q) - P(q)/Q(q)| ≤ |exp(q) - T₁₀(q)| + |T₁₀(q) - P(q)/Q(q)| where T₁₀ is the degree-10 Taylor polynomial. The first term is bounded by Real.exp_bound with n = 11 (≤ 1/36590400 ≈ 2.73×10⁻⁸). The second term equals |T₁₀·Q - P|/Q; the numerator is a polynomial with terms only at degrees 9-14 (Padé matching property), bounded by 187/2032128000 ≈ 9.2×10⁻⁸ via coefficient sum, and Q ≥ 143/240.

def Linglib.Interval.reductionSteps (q : ℚ) : ℕ

Number of halvings needed so q / 2^k ∈ [-1, 1].

Equations

• Linglib.Interval.reductionSteps q = if q.num.natAbs ≤ q.den then 0 else Nat.log 2 q.num.natAbs - Nat.log 2 q.den + 1

def Linglib.Interval.repeatedSq (I : QInterval) (n : ℕ) (h : 0 ≤ I.lo) : QInterval

Repeated squaring of a nonneg interval. Squares I a total of n times: repeatedSq I 0 = I, repeatedSq I (n+1) = (repeatedSq I n)².

Equations

• Linglib.Interval.repeatedSq I n h = ↑(Linglib.Interval.repeatedSqCore✝ I n h)

theorem Linglib.Interval.repeatedSq_nonneg (I : QInterval) (n : ℕ) (h : 0 ≤ I.lo) : 0 ≤ (repeatedSq I n h).lo

def Linglib.Interval.expPoint (q : ℚ) : QInterval

Point interval containing exp(q) for arbitrary rational q.

Strategy: reduce q → q' = q/2^k with |q'| ≤ 1 via reductionSteps, compute exp(q') via Padé [4/4], then square k times since exp(q) = exp(q')^(2^k).

The nonneg guard on small.lo is always true by construction: padeExp(q') ≈ exp(q') ≥ exp(-1) ≈ 0.368 >> padeErrorBound = 2.5×10⁻⁷.

Equations

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

theorem Linglib.Interval.expPoint_containsReal (q : ℚ) : (expPoint q).containsReal (Real.exp ↑q)

Containment theorem for expPoint.

def Linglib.Interval.expInterval (I : QInterval) : QInterval

Interval containing exp(x) for x in rational interval I.

Uses monotonicity of exp: for x ∈ [lo, hi], exp(lo) ≤ exp(x) ≤ exp(hi) so exp(x) ∈ [expPoint(lo).lo, expPoint(hi).hi].

Equations

• Linglib.Interval.expInterval I = { lo := (Linglib.Interval.expPoint I.lo).lo, hi := (Linglib.Interval.expPoint I.hi).hi, valid := ⋯ }

theorem Linglib.Interval.expInterval_containsReal {I : QInterval} {x : ℝ} (hx : I.containsReal x) : (expInterval I).containsReal (Real.exp x)

Containment theorem for expInterval: monotonicity of exp + expPoint containment.