Inversion and division for dyadic numbers

def Dyadic.invAtPrec (x : Dyadic) (prec : Int) : Dyadic

Inverts a dyadic number at a given (maximum) precision. Returns the greatest dyadic number with precision at most prec which is less than or equal to 1/x. For x = 0, returns 0.

This agrees with divAtPrec 1 x prec (see invAtPrec_eq_divAtPrec_one), but is kept as a separate definition to avoid the unnecessary 1 *-by-numerator step in Rat's division at runtime.

Equations

• Dyadic.zero.invAtPrec prec = Dyadic.zero
• x.invAtPrec prec = x.toRat.inv.toDyadic prec

def Dyadic.divAtPrec (a b : Dyadic) (prec : Int) : Dyadic

Divides two dyadic numbers at a given (maximum) precision. Returns the greatest dyadic number with precision at most prec which is less than or equal to a/b. For b = 0, returns 0.

Equations

• a.divAtPrec Dyadic.zero prec = Dyadic.zero
• a.divAtPrec b prec = (a.toRat / b.toRat).toDyadic prec

theorem Dyadic.invAtPrec_eq_divAtPrec_one (x : Dyadic) (prec : Int) : x.invAtPrec prec = divAtPrec 1 x prec

invAtPrec x prec is the special case divAtPrec 1 x prec of dyadic division.

theorem Dyadic.eq_toDyadic_of_precision_le {q : Rat} {y : Dyadic} {prec : Int} (hp : y.precision ≤ some prec) (h1 : y.toRat ≤ q) (h2 : q < y.toRat + 2 ^ (-prec)) : y = q.toDyadic prec

If y : Dyadic has precision at most prec and a rational q lies in the half-open interval [y.toRat, y.toRat + 2 ^ (-prec)), then y is the floor of q at precision prec, i.e. y = q.toDyadic prec.

theorem Dyadic.divAtPrec_mul_le {a b : Dyadic} (hb : 0 < b) (prec : Int) : a.divAtPrec b prec * b ≤ a

For a positive dyadic b, divAtPrec a b prec * b ≤ a.

theorem Dyadic.lt_divAtPrec_add_inc_mul {a b : Dyadic} (hb : 0 < b) (prec : Int) : a < (a.divAtPrec b prec + ofIntWithPrec 1 prec) * b

For a positive dyadic b, a < (divAtPrec a b prec + 2^(-prec)) * b.

theorem Dyadic.eq_divAtPrec {a b : Dyadic} (hb : 0 < b) {prec : Int} {y : Dyadic} (hp : y.precision ≤ some prec) (h1 : y * b ≤ a) (h2 : a < (y + ofIntWithPrec 1 prec) * b) : y = a.divAtPrec b prec

For positive b, divAtPrec a b prec is the unique dyadic with precision at most prec satisfying both _ * b ≤ a and a < (_ + ofIntWithPrec 1 prec) * b.

theorem Dyadic.invAtPrec_mul_le_one {x : Dyadic} (hx : 0 < x) (prec : Int) : x.invAtPrec prec * x ≤ 1

For a positive dyadic x, invAtPrec x prec * x ≤ 1.

theorem Dyadic.one_lt_invAtPrec_add_inc_mul {x : Dyadic} (hx : 0 < x) (prec : Int) : 1 < (x.invAtPrec prec + ofIntWithPrec 1 prec) * x

For a positive dyadic x, 1 < (invAtPrec x prec + 2^(-prec)) * x.

theorem Dyadic.eq_invAtPrec {x : Dyadic} (hx : 0 < x) {prec : Int} {y : Dyadic} (hp : y.precision ≤ some prec) (h1 : y * x ≤ 1) (h2 : 1 < (y + ofIntWithPrec 1 prec) * x) : y = x.invAtPrec prec

invAtPrec x prec is the unique dyadic with precision at most prec satisfying both _ * x ≤ 1 and 1 < (_ + ofIntWithPrec 1 prec) * x, for 0 < x.

theorem Dyadic.mul_invAtPrec_lt_divAtPrec_add {a b : Dyadic} (ha : 0 ≤ a) (hb : 0 < b) (prec : Int) : a * b.invAtPrec prec < a.divAtPrec b prec + ofIntWithPrec 1 prec

The equality divAtPrec a b prec = a * invAtPrec b prec does not hold in general: a * invAtPrec b prec rounds 1/b first and then multiplies, whereas divAtPrec a b prec rounds a/b directly. The next two theorems pin the gap asymmetrically:

divAtPrec a b prec - a * 2 ^ (-prec) < a * invAtPrec b prec < divAtPrec a b prec + 2 ^ (-prec).

For nonneg a and positive b, a * invAtPrec b prec is less than 2 ^ (-prec) larger than divAtPrec a b prec.

theorem Dyadic.divAtPrec_sub_mul_lt_mul_invAtPrec {a b : Dyadic} (ha : 0 < a) (hb : 0 < b) (prec : Int) : a.divAtPrec b prec - a * ofIntWithPrec 1 prec < a * b.invAtPrec prec

For positive a and b, divAtPrec a b prec exceeds a * invAtPrec b prec by less than a * 2 ^ (-prec).