Real containment for integer binary-grid intervals

Signed integer division supplies floor and ceiling bounds before interpretation in the reals. The four-corner theorems then enclose every real member of the input intervals, including values between grid points. The runtime definitions compute entirely with integers after input conversion.

theorem FloatLib.Numerics.Interval.BinaryGrid.scale_eq_pow (precision : ℕ) : scale precision = 2 ^ precision

The shift-based scale is 2 ^ precision.

theorem FloatLib.Numerics.Interval.BinaryGrid.scale_pos (precision : ℕ) : 0 < scale precision

Every binary grid has a positive scale.

noncomputable def FloatLib.Numerics.Interval.BinaryGrid.value (precision : ℕ) (z : ℤ) : ℝ

Real interpretation of a coefficient, used only in mathematical statements and proofs.

@[simp]

theorem FloatLib.Numerics.Interval.BinaryGrid.cast_toRat (precision : ℕ) (z : ℤ) : ↑(toRat precision z) = value precision z

Rational decoding agrees with the real interpretation of the coefficient.

@[simp]

theorem FloatLib.Numerics.Interval.BinaryGrid.containsReal_iff (precision : ℕ) (I : Interval ℤ) (x : ℝ) : ContainsReal (decode precision) I x ↔ value precision I.lo ≤ x ∧ x ≤ value precision I.hi

Real membership in a binary-grid interval is given by its scaled endpoint inequalities.

@[simp]

theorem FloatLib.Numerics.Interval.BinaryGrid.value_zero (precision : ℕ) : value precision 0 = 0

A zero coefficient represents zero on every grid.

@[simp]

theorem FloatLib.Numerics.Interval.BinaryGrid.value_scale (precision : ℕ) : value precision (scale precision) = 1

The grid scale is the coefficient representing one.

@[simp]

theorem FloatLib.Numerics.Interval.BinaryGrid.value_neg (precision : ℕ) (z : ℤ) : value precision (-z) = -value precision z

Negating a coefficient negates its real value.

@[simp]

theorem FloatLib.Numerics.Interval.BinaryGrid.value_add (precision : ℕ) (a b : ℤ) : value precision (a + b) = value precision a + value precision b

Coefficient addition is exact on a common grid.

@[simp]

theorem FloatLib.Numerics.Interval.BinaryGrid.value_sub (precision : ℕ) (a b : ℤ) : value precision (a - b) = value precision a - value precision b

Coefficient subtraction is exact on a common grid.

@[simp]

theorem FloatLib.Numerics.Interval.BinaryGrid.value_le_value_iff (precision : ℕ) (a b : ℤ) : value precision a ≤ value precision b ↔ a ≤ b

Non-strict comparison of coefficients agrees with comparison of their real values.

@[simp]

theorem FloatLib.Numerics.Interval.BinaryGrid.value_lt_value_iff (precision : ℕ) (a b : ℤ) : value precision a < value precision b ↔ a < b

Strict comparison of coefficients agrees with comparison of their real values.

@[simp]

theorem FloatLib.Numerics.Interval.BinaryGrid.value_min (precision : ℕ) (a b : ℤ) : value precision (min a b) = min (value precision a) (value precision b)

Taking the smaller coefficient gives the smaller real value.

@[simp]

theorem FloatLib.Numerics.Interval.BinaryGrid.value_max (precision : ℕ) (a b : ℤ) : value precision (max a b) = max (value precision a) (value precision b)

Taking the larger coefficient gives the larger real value.

theorem FloatLib.Numerics.Interval.BinaryGrid.divBounds_bounds {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (a b : ℤ) (hb : b ≠ 0) : ↑(divBounds a b).lo ≤ ↑a / ↑b ∧ ↑a / ↑b ≤ ↑(divBounds a b).hi

The integer quotient bounds enclose exact division in any ordered field.

theorem FloatLib.Numerics.Interval.BinaryGrid.roundDown_le (precision : ℕ) (z : ℤ) : ↑(roundDown precision z) ≤ value precision z

Rounding down by a signed shift stays below the exact scaled coefficient.

theorem FloatLib.Numerics.Interval.BinaryGrid.le_roundUp (precision : ℕ) (z : ℤ) : value precision z ≤ ↑(roundUp precision z)

Rounding up by a signed shift stays above the exact scaled coefficient.

theorem FloatLib.Numerics.Interval.BinaryGrid.containsReal_coarsen {shift precision : ℕ} {I : Interval ℤ} {x : ℝ} (hx : ContainsReal (decode (precision + shift)) I x) : ContainsReal (decode precision) (coarsen shift I) x

Coarsening a grid interval keeps every real member, on the coarser grid.

theorem FloatLib.Numerics.Interval.BinaryGrid.contains_enclose (precision : ℕ) (q : ℚ) : Contains (decode precision) (enclose precision q) q

Conversion from an exact rational produces a containing binary-grid interval.

def FloatLib.Numerics.Interval.BinaryGrid.rounding (precision : ℕ) : OutwardRounding ℤ ℚ

Total outward rounding from exact rationals onto a fixed binary grid.

theorem FloatLib.Numerics.Interval.BinaryGrid.containsReal_enclose (precision : ℕ) (q : ℚ) : ContainsReal (decode precision) (enclose precision q) ↑q

Rational conversion contains the corresponding real number.

theorem FloatLib.Numerics.Interval.BinaryGrid.containsReal_neg (precision : ℕ) {I : Interval ℤ} {x : ℝ} (hx : ContainsReal (decode precision) I x) : ContainsReal (decode precision) (neg I) (-x)

Exact grid negation encloses the negative of every real input member.

theorem FloatLib.Numerics.Interval.BinaryGrid.containsReal_add (precision : ℕ) {I J : Interval ℤ} {x y : ℝ} (hx : ContainsReal (decode precision) I x) (hy : ContainsReal (decode precision) J y) : ContainsReal (decode precision) (add I J) (x + y)

Exact grid addition encloses the sum of arbitrary real input members.

theorem FloatLib.Numerics.Interval.BinaryGrid.containsReal_sub (precision : ℕ) {I J : Interval ℤ} {x y : ℝ} (hx : ContainsReal (decode precision) I x) (hy : ContainsReal (decode precision) J y) : ContainsReal (decode precision) (sub I J) (x - y)

Exact grid subtraction encloses the difference of arbitrary real input members.

theorem FloatLib.Numerics.Interval.BinaryGrid.containsReal_mul (precision : ℕ) {I J : Interval ℤ} {x y : ℝ} (hx : ContainsReal (decode precision) I x) (hy : ContainsReal (decode precision) J y) : ContainsReal (decode precision) (mul precision I J) (x * y)

Integer four-corner multiplication encloses products of arbitrary real input members.

theorem FloatLib.Numerics.Interval.BinaryGrid.containsReal_div? (precision : ℕ) {I J K : Interval ℤ} (h : div? precision I J = some K) {x y : ℝ} (hx : ContainsReal (decode precision) I x) (hy : ContainsReal (decode precision) J y) : ContainsReal (decode precision) K (x / y)

Successful integer division encloses quotients of arbitrary real input members.

theorem FloatLib.Numerics.Interval.BinaryGrid.containsReal_abs (precision : ℕ) {I : Interval ℤ} {x : ℝ} (hx : ContainsReal (decode precision) I x) : ContainsReal (decode precision) (abs I) |x|

Exact grid absolute value encloses the absolute value of every real input member.

theorem FloatLib.Numerics.Interval.BinaryGrid.containsReal_square (precision : ℕ) {I : Interval ℤ} {x : ℝ} (hx : ContainsReal (decode precision) I x) : ContainsReal (decode precision) (square precision I) (x ^ 2)

The specialized square encloses the square of every real input member.

theorem FloatLib.Numerics.Interval.BinaryGrid.containsReal_pow (precision : ℕ) {I : Interval ℤ} {x : ℝ} (hx : ContainsReal (decode precision) I x) (n : ℕ) : ContainsReal (decode precision) (pow precision I n) (x ^ n)

Parity-aware endpoint bounds enclose every natural power of an arbitrary real input member.