Format-generic executable exponential and logarithm

expWith and logWith take their approximation data as an argument. The convenience operations exp and log select Config.forFormat. Their finite results are deterministic approximations, and accuracy bounds need their own certificates.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.mulDyadic (left right : Numerics.Dyadic) : Numerics.Dyadic

Exact dyadic multiplication without rounding.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.dyadicOfInt (value : ℤ) : Numerics.Dyadic

Embed an integer as an exact dyadic.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.oneDyadic : Numerics.Dyadic

Exact dyadic one.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.zeroDyadic : Numerics.Dyadic

Exact dyadic zero.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.evalDyadicPolyAsc (coefficients : List ℤ) (value : Numerics.Dyadic) : Numerics.Dyadic

Evaluate ascending integer coefficients as an exact polynomial in a dyadic argument.

An empty coefficient list evaluates to zero.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.roundDyadicDivNat (fmt : FloatFormat) (value : Numerics.Dyadic) (denominator : ℕ) : Model fmt

Round value / denominator to the destination format for a positive denominator. A zero numerator preserves its sign, and a zero denominator with nonzero numerator gives invalidResult.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.expGuardBits : ℕ

Bits kept beyond twice the destination precision by the small-argument exponential.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.expTaylorDegree (target magnitude : ℕ) : ℕ

Degree of the Taylor polynomial of exp for an argument below 2^(-magnitude), with magnitude ≥ 1.

Returns the first n with 2^(magnitude * (n + 1)) * (n + 1)! ≥ 2^target, so the first omitted term x^(n+1)/(n+1)! is below 2^(-target). The fuel target exceeds the point where the power of two alone reaches the target.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.expTaylorDegree.go (target magnitude : ℕ) : ℕ → ℕ → ℕ

Search upward from count, with fuel remaining steps.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.expTaylorData (terms : ℕ) : ℕ × List ℤ

Exact common-denominator coefficients of sum k in [0, terms], x^k/k!, as (terms!, coefficients).

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.expReduce (config : Config) (exact : Numerics.Dyadic) : ℤ × ℤ

Reduce x / log 2 to the nearest integer n and a remainder in [-1/2, 1/2] at config.fixed fractional bits, so that exp x = 2^n * 2^remainder.

x / log 2 carries the error of 1 / log 2 times |x|. For |x| ≥ 1 the reduction therefore runs at bits |x| more fractional bits, with log 2 from the shared constants cache (Numerics.Enclosure.Constants.ln2Faithful, within one unit), which keeps the remainder accurate at config.fixed bits for every argument. Smaller arguments use the configured reciprocal.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.atanhSeries (fixed : FixedPoint) (t : ℤ) (terms : ℕ) : ℤ

Evaluate the first terms terms of t + t^3/3 + t^5/5 + ... in a fixed-point context.

def FloatLib.Floats.Formats.BinaryInterchange.Model.expWithProvider {fmt : FloatFormat} (getConfig : Unit → Transcendentals.Config) (x : Model fmt) : Model fmt

Evaluate exponential using a delayed configuration provider.

The provider is called only for a finite input that is neither tiny nor beyond the overflow and underflow bounds, so generated configurations are not constructed for NaNs, infinities, or those arguments. Below 2^-(p+1) the nearest result is one. Two kinds of argument below one half evaluate sum x^k/k! exactly with enough terms for 2p + expGuardBits bits and round once: one whose bits extend below the fixed-point scale, which conversion would round so that neighbouring inputs share a result; and one whose x^2/2 is within 2^15 of the fixed-point resolution, since near zero exp x can sit just x^2/2 off a rounding midpoint. Every other argument uses the configured fixed-point path.

def FloatLib.Floats.Formats.BinaryInterchange.Model.logWithProvider {fmt : FloatFormat} (getConfig : Unit → Transcendentals.Config) (x : Model fmt) : Model fmt

Evaluate logarithm using a delayed configuration provider.

The provider is called only for a finite positive input.

def FloatLib.Floats.Formats.BinaryInterchange.Model.expWith {fmt : FloatFormat} (config : Transcendentals.Config) (x : Model fmt) : Model fmt

Deterministic exponential using range reduction and a fixed-point polynomial.

NaNs are quieted and infinities use the destination format's native overflow and zero policies.

def FloatLib.Floats.Formats.BinaryInterchange.Model.logWith {fmt : FloatFormat} (config : Transcendentals.Config) (x : Model fmt) : Model fmt

Deterministic natural logarithm using centered dyadic normalization and an odd atanh series.

Inputs near one use additional working precision and avoid a logarithmic subtraction. Special values follow the destination format's native overflow and invalid-result policies.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.exp {fmt : FloatFormat} (x : Model fmt) : Model fmt

Exponential using the default configuration for the destination format.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.log {fmt : FloatFormat} (x : Model fmt) : Model fmt

Natural logarithm using the default configuration for the destination format.