Rational and binary-grid expression backends

Backend.ofRounding combines the interval operations with any rational outward rounder. Backend.rational keeps exact rational endpoints. Backend.binaryGrid uses integer arithmetic for algebraic operations and rounds rational elementary-function bounds back onto its grid.

The elementary enclosures and their domain checks are shared by all endpoint backends. BackendsProof proves the common Backend.Sound contract for all three backends.

def FloatLib.Numerics.Interval.Backend.elementaryBounds? (config : Config) : UnaryOp → Interval ℚ → Option (Interval ℚ)

Rational enclosures for elementary expression operations.

Arithmetic constructors return none; the backends dispatch them to their own arithmetic. Logarithm requires a positive lower endpoint, and square root requires a nonnegative one. Inverse sine and cosine require inputs in [-1, 1]; tangent requires a cosine enclosure that excludes zero.

def FloatLib.Numerics.Interval.Backend.ofRounding {α : Type u_1} (R : OutwardRounding α ℚ) (config : Config := { }) : Backend α

Build an expression backend from a partial rational outward rounder.

Algebraic operations compute exact rational endpoint bounds before rounding. Elementary operations first produce rational enclosures at the configured accuracy, then round outward. Failed decoding, rejected domains, and unrepresentable output bounds propagate as none.

def FloatLib.Numerics.Interval.Backend.rational (config : Config := { }) : Backend ℚ

Exact rational endpoints, with configurable rational elementary-function enclosures.

def FloatLib.Numerics.Interval.Backend.binaryGrid (config : Config := { }) : Backend ℤ

Integer endpoints representing multiples of 2^(-config.precision).

Arithmetic, absolute value, powers, and endpoint comparisons stay in integer arithmetic. Elementary functions decode their input once and round the rational result bounds onto the same grid. The scale is supplied by this backend, so intervals from different grids must be converted before they are combined.

def FloatLib.Numerics.Interval.Backend.elementaryExtension (op : UnaryOp) : Extension

Adapt an existing unary elementary enclosure to the extension interface.

def FloatLib.Numerics.Interval.Backend.asinhExtension : Extension

Inverse hyperbolic sine enclosure for registered evaluation.

def FloatLib.Numerics.Interval.Backend.acoshExtension : Extension

Inverse hyperbolic cosine enclosure for registered evaluation.

def FloatLib.Numerics.Interval.Backend.atanhExtension : Extension

Inverse hyperbolic tangent enclosure for registered evaluation.

def FloatLib.Numerics.Interval.Backend.rpowExtension : Extension

Real powers on positive bases for registered evaluation.

def FloatLib.Numerics.Interval.Backend.logbExtension : Extension

Logarithms with a supplied positive base separated from one.