Integer arithmetic on a binary interval grid

At precision fractional bits, an integer coefficient z represents z / 2^precision. Intervals are the existing Interval Int, and each operation takes the scale as an argument instead of storing it in the interval. Coefficients have unbounded magnitude, so arithmetic cannot overflow.

Addition, subtraction, and negation are exact. Multiplication rounds the smallest and largest integer products with signed shifts. Division uses four integer quotients and rejects a divisor interval containing zero. Values are decoded to rationals at the interface, never between arithmetic steps.

The endpoint construction follows S. M. Rump, Verification methods: Rigorous results using floating-point arithmetic, Acta Numerica 19 (2010), §§5.1–5.3. BinaryGridProof proves containment for arbitrary real members of the input intervals.

def FloatLib.Numerics.Interval.BinaryGrid.scale (precision : ℕ) : ℤ

Positive integer scale 2 ^ precision of a grid with precision fractional bits.

def FloatLib.Numerics.Interval.BinaryGrid.toRat (precision : ℕ) (z : ℤ) : ℚ

Exact rational interpretation of an integer coefficient on the binary grid.

def FloatLib.Numerics.Interval.BinaryGrid.decode (precision : ℕ) (z : ℤ) : Option ℚ

Decode a coefficient as its rational value. Every coefficient is finite.

def FloatLib.Numerics.Interval.BinaryGrid.roundDown (precision : ℕ) (z : ℤ) : ℤ

Floor of z / 2^precision. The signed shift rounds negative values downward too.

def FloatLib.Numerics.Interval.BinaryGrid.roundUp (precision : ℕ) (z : ℤ) : ℤ

Ceiling of z / 2^precision, obtained by negating a downward-rounded negative.

def FloatLib.Numerics.Interval.BinaryGrid.coarsen (shift : ℕ) (I : Interval ℤ) : Interval ℤ

Coarsen a grid interval by shift fractional bits, rounding both endpoints outward.

def FloatLib.Numerics.Interval.BinaryGrid.divBounds (a b : ℤ) : Interval ℤ

Integer floor and ceiling of a / b, for a nonzero denominator of either sign.

One signed floor division supplies both endpoints. Testing the integer product detects exact division without computing another quotient or a rational greatest common divisor.

def FloatLib.Numerics.Interval.BinaryGrid.enclose (precision : ℕ) (q : ℚ) : Interval ℤ

Enclose an exact rational by neighboring grid coefficients.

def FloatLib.Numerics.Interval.BinaryGrid.neg (I : Interval ℤ) : Interval ℤ

Exact negation on the grid, with the endpoints exchanged.

def FloatLib.Numerics.Interval.BinaryGrid.add (I J : Interval ℤ) : Interval ℤ

Exact addition of intervals on the same grid.

def FloatLib.Numerics.Interval.BinaryGrid.sub (I J : Interval ℤ) : Interval ℤ

Exact subtraction of intervals on the same grid.

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

Multiply using four integer products and two outward-rounded shifts.

def FloatLib.Numerics.Interval.BinaryGrid.div? (precision : ℕ) (I J : Interval ℤ) : Option (Interval ℤ)

Divide using scaled integer numerators, returning none for a denominator containing zero.

The four corner divisions round outward on the same grid as the input endpoints. No rational normalization occurs in this operation.

def FloatLib.Numerics.Interval.BinaryGrid.abs (I : Interval ℤ) : Interval ℤ

Exact absolute-value enclosure, taking a zero lower bound when the interval crosses zero.

def FloatLib.Numerics.Interval.BinaryGrid.square (precision : ℕ) (I : Interval ℤ) : Interval ℤ

Square with a nonnegative lower bound, including for intervals that cross zero.

Using the range of the square avoids the negative lower endpoint produced by treating the two occurrences of the input as independent factors.

@[irreducible]

def FloatLib.Numerics.Interval.BinaryGrid.Internal.pow (precision : ℕ) (I : Interval ℤ) (n : ℕ) : Interval ℤ

Repeated squaring for the endpoint evaluations in BinaryGrid.pow.

With the squaring in its own helper, the public operation can use monotonicity before interval evaluation. The exponent-one branch avoids multiplying by a scaled representation of one.

def FloatLib.Numerics.Interval.BinaryGrid.pow (precision : ℕ) (I : Interval ℤ) (n : ℕ) : Interval ℤ

Natural powers with logarithmically many interval operations.

Odd powers are increasing, so their lower and upper bounds come from evaluating at each endpoint. Even powers use the absolute-value interval. These choices avoid treating repeated occurrences of the input as independent values. Each evaluation still rounds outward at intermediate steps. Exponents zero and one are exact, and a point interval needs one repeated-squaring evaluation.