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.

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

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

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.

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.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.