Elementary enclosures evaluated on a binary grid

Taylor polynomials and remainder bounds use integer interval arithmetic at precision fractional bits. Each multiplication and scalar division rounds outward on that grid. Argument reduction and scalar factors use exact rational arithmetic, and only the final endpoints are decoded.

The degree selects the same Taylor polynomial as the rational kernels in Elementary.Runtime. Containment holds at every degree and precision, including zero, so the precision and degree estimates below guide refinement and never affect soundness. Coarse grids can give wide bounds.

Long logarithm polynomials share a table of powers through rectangular splitting, as in Section 4 of Fredrik Johansson, Efficient implementation of elementary functions in the medium-precision range.

def FloatLib.Numerics.Enclosure.BinaryGrid.workingPrecision (targetBits degree : ℕ) : ℕ

Add guard bits and a degree-dependent rounding allowance to a target grid width.

def FloatLib.Numerics.Enclosure.BinaryGrid.relativePrecision (targetBits : ℕ) (scale : ℚ) (degree : ℕ) : ℕ

Choose a grid width relative to a nonzero result scale.

The integer logarithms estimate the extra fractional bits needed for a small result. Consumers handle exact zero themselves. A higher degree also raises the rounding allowance.

def FloatLib.Numerics.Enclosure.BinaryGrid.expPrecision (targetBits : ℕ) (x : ℚ) (degree : ℕ) (subtractOne : Bool := false) : ℕ

Allow for repeated squaring and small exponential results when choosing a grid width.

Subtracting one also needs enough fractional bits to retain a small input's contribution.

def FloatLib.Numerics.Enclosure.BinaryGrid.logPrecision (targetBits : ℕ) (x : ℚ) (degree : ℕ) : ℕ

Allow for cancellation near one and scaling by a large binary logarithm.

def FloatLib.Numerics.Enclosure.BinaryGrid.toRationalInterval (precision : ℕ) (I : Interval ℤ) : RationalInterval

Decode the two final coefficients as rational endpoints.

def FloatLib.Numerics.Enclosure.BinaryGrid.scaleRat (I : Interval ℤ) (factor : ℚ) : Interval ℤ

Scale an interval by an exact rational, rounding the integer coefficients outward.

The rational denominator is positive, so scalar division remains defined on every grid.

def FloatLib.Numerics.Enclosure.BinaryGrid.divideNat (I : Interval ℤ) (n : ℕ) : Interval ℤ

Divide the coefficients by a natural scalar with outward rounding.

@[inline]

def FloatLib.Numerics.Enclosure.BinaryGrid.Internal.divideNat (I : Interval ℤ) (n : ℕ) : Interval ℤ

Integer floor and ceiling division. A zero divisor gives the zero interval.

@[inline]

def FloatLib.Numerics.Enclosure.BinaryGrid.Internal.mul (precision : ℕ) (I J : Interval ℤ) : Interval ℤ

Grid multiplication with two corner products when either factor is a point, in any order.

@[csimp]

theorem FloatLib.Numerics.Enclosure.BinaryGrid.divideNat_eq_direct : divideNat = Internal.divideNat

divideNat equals the integer floor and ceiling division that compiled code runs.

@[csimp]

theorem FloatLib.Numerics.Enclosure.BinaryGrid.mul_eq_point : Interval.BinaryGrid.mul = Internal.mul

Grid multiplication equals Internal.mul, which needs two products for a point factor.

def FloatLib.Numerics.Enclosure.BinaryGrid.around (midpoint radius : Interval ℤ) : Interval ℤ

Expand a midpoint interval using the upper endpoint of a radius enclosure.

def FloatLib.Numerics.Enclosure.BinaryGrid.expHorner (precision : ℕ) (X : Interval ℤ) (start : ℕ) : ℕ → Interval ℤ

Exponential Horner steps, with every product and division rounded on the chosen grid.

def FloatLib.Numerics.Enclosure.BinaryGrid.logOddHorner (precision : ℕ) (X Q : Interval ℤ) (start : ℕ) : ℕ → Interval ℤ

Odd logarithm terms evaluated by Horner steps in the square of the argument.

@[specialize #[]]

def FloatLib.Numerics.Enclosure.BinaryGrid.Internal.reverseHorner (step : ℕ → Interval ℤ → Interval ℤ) (start : ℕ) : ℕ → Interval ℤ → Interval ℤ

Apply Horner steps from the highest index down, keeping the partial result in an accumulator.

def FloatLib.Numerics.Enclosure.BinaryGrid.expHornerIter (precision : ℕ) (X : Interval ℤ) (start n : ℕ) : Interval ℤ

Exponential Horner evaluation with an accumulator and one shared grid coefficient for one.

def FloatLib.Numerics.Enclosure.BinaryGrid.logOddHornerIter (precision : ℕ) (X Q : Interval ℤ) (start n : ℕ) : Interval ℤ

Odd logarithm Horner evaluation with an accumulator.

@[csimp]

theorem FloatLib.Numerics.Enclosure.BinaryGrid.expHorner_eq_iter : expHorner = expHornerIter

Exponential Horner evaluation equals the accumulator loop that compiled code runs.

@[csimp]

theorem FloatLib.Numerics.Enclosure.BinaryGrid.logOddHorner_eq_iter : logOddHorner = logOddHornerIter

Odd logarithm Horner evaluation equals the accumulator loop that compiled code runs.

def FloatLib.Numerics.Enclosure.BinaryGrid.expRadius (precision : ℕ) (X : Interval ℤ) (n : ℕ) : Interval ℤ

Evaluate the exponential remainder bound without forming an exact rational power.

def FloatLib.Numerics.Enclosure.BinaryGrid.expSmall (x : ℚ) (degree precision : ℕ) : Interval ℤ

Enclose the exponential of a small argument with its Taylor polynomial and remainder bound.

def FloatLib.Numerics.Enclosure.BinaryGrid.squareRepeat (precision : ℕ) (I : Interval ℤ) : ℕ → Interval ℤ

Square n times, rounding outward after each square, to undo exponential range reduction.

def FloatLib.Numerics.Enclosure.BinaryGrid.expExtraScale (x : ℚ) (degree precision : ℕ) : ℕ

Balance Taylor work against extra squarings using the degree and requested grid width.

The square-root estimate limits squaring work while the degree is small, and the quotient reduces it as refinement raises the degree. A small input already supplies some reduction without squaring.

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

Enclose the exponential, with extra grid bits to cover the extra range-restoring squares.

def FloatLib.Numerics.Enclosure.BinaryGrid.LogPolynomial.powerTableAux (precision : ℕ) (Q : Interval ℤ) : ℕ → Interval ℤ → Array (Interval ℤ) → Array (Interval ℤ)

Extend a table with successive rounded powers, including its final power.

def FloatLib.Numerics.Enclosure.BinaryGrid.LogPolynomial.powerTable (precision : ℕ) (Q : Interval ℤ) (n : ℕ) : Array (Interval ℤ)

Store the powers from zero through n, using one rounded multiplication per new power.

def FloatLib.Numerics.Enclosure.BinaryGrid.LogPolynomial.blockSumAux (powers : Array (Interval ℤ)) (start : ℕ) : ℕ → Interval ℤ → Interval ℤ

Add one block of scalar-divided powers, from the highest index down.

def FloatLib.Numerics.Enclosure.BinaryGrid.LogPolynomial.blockSum (powers : Array (Interval ℤ)) (start n : ℕ) : Interval ℤ

Sum of one block, by scalar division and grid addition alone.

def FloatLib.Numerics.Enclosure.BinaryGrid.LogPolynomial.blockHorner (precision : ℕ) (powers : Array (Interval ℤ)) (stride : Interval ℤ) (start blockSize blocks : ℕ) (tail : Interval ℤ) : Interval ℤ

Apply the block Horner steps from the highest block down.

def FloatLib.Numerics.Enclosure.BinaryGrid.LogPolynomial.logOddRectangular (precision : ℕ) (X Q : Interval ℤ) (start n blockSize : ℕ) : Interval ℤ

Rectangular evaluation with a positive block size and an unpadded final partial block.

def FloatLib.Numerics.Enclosure.BinaryGrid.logOddPolynomial (precision : ℕ) (X Q : Interval ℤ) (start n : ℕ) : Interval ℤ

Odd logarithm polynomial: Horner steps up to four terms, rectangular splitting above.

def FloatLib.Numerics.Enclosure.BinaryGrid.logOddRadius (precision : ℕ) (X Q : Interval ℤ) (x : ℚ) (n : ℕ) : Interval ℤ

Evaluate the odd logarithm remainder with a grid power and an exact scalar denominator.

Using 1 - x² before rounding avoids a zero-crossing grid divisor at low precision.

def FloatLib.Numerics.Enclosure.BinaryGrid.logSeries (x : ℚ) (degree precision : ℕ) : Interval ℤ

Enclose log x with the odd terms of its transformed series.

def FloatLib.Numerics.Enclosure.BinaryGrid.logSeriesDegree (value : ℚ) (bits : ℕ) : ℕ

A logarithm series degree for a positive value whose truncation error is below about 2 ^ -bits.

For value = n / d in lowest terms the series runs in t = (n - d) / (n + d), so each pair of degrees gains log₂ (1 / t²) bits. The estimate uses the integer part of 1 / t².

def FloatLib.Numerics.Enclosure.BinaryGrid.logUnreduced (value : ℚ) (precision : ℕ) : Interval ℤ

Enclose log value for a positive rational on the grid of precision fractional bits with the transformed series in (value - 1) / (value + 1), without the argument reduction of log. It suits values near one.

def FloatLib.Numerics.Enclosure.BinaryGrid.logLarge (x : ℚ) (degree precision : ℕ) : Interval ℤ

Remove a power of two and restore its multiple of log 2, omitting a zero multiple.

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

Enclose the logarithm of a positive rational, inverting arguments below one before reduction.