Elementary functions on rational intervals

Monotone functions use lower and upper endpoint enclosures. Sine and cosine instead enclose the midpoint and add the half-width, using their global Lipschitz constant one. Intersecting with [-1, 1] keeps the bounds useful even when the requested Taylor degree is small.

The analytic point enclosures come from Numerics.Enclosure. Square root uses an integer square root after exact dyadic scaling. ElementaryProof proves containment of every real member of the input interval, including irrational members.

def FloatLib.Numerics.Interval.monotoneBounds (enclose : ℚ → Interval ℚ) (I : Interval ℚ) : Interval ℚ

Combine the lower enclosure at the left endpoint with the upper enclosure at the right.

Soundness requires a monotone real function and sound point enclosures. A point interval evaluates the enclosure only once.

def FloatLib.Numerics.Interval.expBounds (I : Interval ℚ) (terms : ℕ) : Interval ℚ

Enclose the exponential on the whole interval, with the supplied Taylor degree.

def FloatLib.Numerics.Interval.logBounds? (I : Interval ℚ) (terms : ℕ) : Option (Interval ℚ)

Enclose the logarithm when the entire input interval is strictly positive.

def FloatLib.Numerics.Interval.atanBounds (I : Interval ℚ) (terms : ℕ) : Interval ℚ

Enclose arctangent on the whole interval, using the reduced rational point kernel.

def FloatLib.Numerics.Interval.lipschitzUnitBounds (enclose : ℚ → Interval ℚ) (I : Interval ℚ) : Interval ℚ

Enclose a function with Lipschitz constant one and range in [-1, 1].

The midpoint enclosure is widened by the half-width. Widths at least four already give the whole unit range after this widening, so they skip the point kernel.

def FloatLib.Numerics.Interval.Internal.reducedTrigBounds (taylor : ℚ → ℕ → ℚ) (x : ℚ) (terms : ℕ) : RationalInterval

Share the period certificate and turn count between the value and error bounds.

def FloatLib.Numerics.Interval.sinBounds (I : Interval ℚ) (terms : ℕ) : Interval ℚ

Enclose sine for every real in the interval, including intervals crossing an extremum.

Small midpoints use the direct Taylor kernel. Larger ones use proved rational period reduction; the resulting period error is included in the point enclosure.

def FloatLib.Numerics.Interval.cosBounds (I : Interval ℚ) (terms : ℕ) : Interval ℚ

Enclose cosine by the midpoint Lipschitz bound, without assuming endpoint monotonicity.

def FloatLib.Numerics.Interval.sqrtPointBounds (x : ℚ) (precision : ℕ) : Interval ℚ

Dyadic bounds for the square root of a nonnegative rational.

The lower endpoint is floor (sqrt x * 2^precision) / 2^precision, computed by an integer square root. The upper endpoint is one grid step higher, unless the lower endpoint squares to x exactly. The width is therefore at most 2^(-precision).

def FloatLib.Numerics.Interval.sqrtBounds? (I : Interval ℚ) (precision : ℕ) : Option (Interval ℚ)

Enclose square root on a nonnegative interval with a dyadic grid of step 2^(-precision).

A negative lower endpoint returns none, including intervals that cross zero from below. Zero and exact dyadic squares are accepted without an artificial positive lower bound.