Rational enclosures for exponential and logarithm

Taylor polynomials and their remainder bounds are evaluated with exact rational arithmetic. exp reduces the argument by a power of two and restores the scale by repeated squaring. The reduced logarithm series uses the identity log x = log (1 + t) - log (1 - t), where t = (x - 1) / (x + 1). log first reduces a positive argument to [1, 2), then restores the removed multiple of log 2. Every series argument satisfies |t| ≤ 1/3.

The natural argument controls the polynomial degree, not a floating-point precision or a search timeout. The endpoint error tends to zero as it increases. These kernels return bounds. A caller can use them to separate the exact value from rounding boundaries, or show that both endpoints round to the same result.

The soundness theorems in Elementary.Proof use Mathlib's real Taylor remainder bounds.

The underlying series are the exponential and logarithm expansions in the NIST Digital Library of Mathematical Functions, §4.2.E19 and §4.6.E1. The logarithm change of variable is also used in §4.6.E4.

def FloatLib.Numerics.Enclosure.expTaylor (x : ℚ) (n : ℕ) : ℚ

The first n terms of the exponential series, evaluated exactly.

@[csimp]

theorem FloatLib.Numerics.Enclosure.expTaylor_eq_binarySplit : expTaylor = Taylor.exp

The exponential Taylor sum equals its evaluation by binary splitting.

def FloatLib.Numerics.Enclosure.expRadius (x : ℚ) (n : ℕ) : ℚ

Absolute exponential remainder bound for |x| ≤ 1 and n > 0.

def FloatLib.Numerics.Enclosure.expSmall (x : ℚ) (degree : ℕ) : RationalInterval

Enclose exp x on |x| ≤ 1, using at least the constant Taylor term.

def FloatLib.Numerics.Enclosure.expScale (x : ℚ) : ℕ

A binary reduction scale determined by the integer part of the absolute argument.

Dividing by this power of two puts the absolute argument below one. Using the quotient rather than the numerator keeps the scale small for high-precision rational inputs close to one.

def FloatLib.Numerics.Enclosure.exp (x : ℚ) (degree : ℕ) : RationalInterval

Enclose the exponential of any rational argument by reduction and repeated squaring.

def FloatLib.Numerics.Enclosure.logOneSubTaylor (x : ℚ) (n : ℕ) : ℚ

The first n terms of -log (1 - x), before restoring the sign.

@[csimp]

theorem FloatLib.Numerics.Enclosure.logOneSubTaylor_eq_binarySplit : logOneSubTaylor = Taylor.logOneSub

The Taylor sum for -log (1 - x) equals its evaluation by binary splitting.

def FloatLib.Numerics.Enclosure.logOneSubRadius (x : ℚ) (n : ℕ) : ℚ

Absolute logarithm remainder bound on |x| < 1.

def FloatLib.Numerics.Enclosure.logOneSub (x : ℚ) (degree : ℕ) : RationalInterval

Enclose log (1 - x) for |x| < 1.

def FloatLib.Numerics.Enclosure.logSeries (x : ℚ) (degree : ℕ) : RationalInterval

Enclose the natural logarithm of a positive rational with its transformed series.

The change of variable maps every positive argument into (-1, 1). Argument reduction before this kernel is useful when a value is far from one, since the series then converges slowly.

def FloatLib.Numerics.Enclosure.logScale (x : ℚ) : ℕ

Binary logarithm of the integer part, used to reduce arguments at least one.

def FloatLib.Numerics.Enclosure.logLarge (x : ℚ) (degree : ℕ) : RationalInterval

Enclose the logarithm after removing an exact power of two from the argument.

def FloatLib.Numerics.Enclosure.logLargeReduced (x : ℚ) (degree : ℕ) : RationalInterval

Omit the log 2 enclosure when its coefficient is zero.

@[csimp]

theorem FloatLib.Numerics.Enclosure.logLarge_eq_reduced : logLarge = logLargeReduced

Omitting the log 2 term when its coefficient is zero preserves both endpoints.

def FloatLib.Numerics.Enclosure.log (x : ℚ) (degree : ℕ) : RationalInterval

Enclose the logarithm of a positive rational with binary argument reduction.

Inputs below one are inverted first and the resulting interval is negated. Every series is therefore evaluated in [1, 2], independently of the original input's exponent.