The dyadic rationals

Constructs the dyadic rationals as an ordered ring, equipped with a compatible embedding into the rationals.

def Int.trailingZeros (i : Int) : Nat

The number of trailing zeros in the binary representation of i.

def Int.trailingZeros.aux (k : Nat) (i : Int) (hi : i ≠ 0) (hk : i.natAbs ≤ k) (acc : Nat) : Nat

theorem Int.trailingZeros_zero : trailingZeros 0 = 0

theorem Int.trailingZeros_two_mul_add_one (i : Int) : (2 * i + 1).trailingZeros = 0

theorem Int.trailingZeros_eq_zero_of_mod_eq {i : Int} (h : i % 2 = 1) : i.trailingZeros = 0

theorem Int.trailingZeros_two_mul {i : Int} (h : i ≠ 0) : (2 * i).trailingZeros = i.trailingZeros + 1

@[irreducible]

theorem Int.shiftRight_trailingZeros_mod_two {i : Int} (h : i ≠ 0) : i >>> i.trailingZeros % 2 = 1

@[irreducible]

theorem Int.two_pow_trailingZeros_dvd {i : Int} (h : i ≠ 0) : 2 ^ i.trailingZeros ∣ i

theorem Int.trailingZeros_shiftLeft {x : Int} (hx : x ≠ 0) (n : Nat) : (x <<< n).trailingZeros = x.trailingZeros + n

@[simp, irreducible]

theorem Int.trailingZeros_neg (x : Int) : (-x).trailingZeros = x.trailingZeros

inductive Dyadic : Type

A dyadic rational is either zero or of the form n * 2^(-k) for some (unique) n k : Int where n is odd.

• zero : Dyadic

  The dyadic number 0.

• ofOdd (n k : Int) (hn : n % 2 = 1) : Dyadic

  The dyadic number n * 2^(-k) for some odd n and integer k.

@[implicit_reducible]

instance instDecidableEqDyadic : DecidableEq Dyadic

def instDecidableEqDyadic.decEq (x✝ x✝¹ : Dyadic) : Decidable (x✝ = x✝¹)

def Dyadic.ofIntWithPrec (i prec : Int) : Dyadic

Returns the dyadic number representation of i * 2 ^ (-exp).

def Dyadic.ofInt (i : Int) : Dyadic

Convert an integer to a dyadic number (which will necessarily have non-positive precision).

@[implicit_reducible]

instance Dyadic.instOfNat (n : Nat) : OfNat Dyadic n

@[implicit_reducible]

instance Dyadic.instIntCast : IntCast Dyadic

@[implicit_reducible]

instance Dyadic.instNatCast : NatCast Dyadic

def Dyadic.add (x y : Dyadic) : Dyadic

Add two dyadic numbers.

@[implicit_reducible]

instance Dyadic.instAdd : Add Dyadic

def Dyadic.mul (x y : Dyadic) : Dyadic

Multiply two dyadic numbers.

@[implicit_reducible]

instance Dyadic.instMul : Mul Dyadic

def Dyadic.pow (x : Dyadic) (i : Nat) : Dyadic

Multiply two dyadic numbers.

@[implicit_reducible]

instance Dyadic.instPowNat : Pow Dyadic Nat

def Dyadic.neg (x : Dyadic) : Dyadic

Negate a dyadic number.

@[implicit_reducible]

instance Dyadic.instNeg : Neg Dyadic

def Dyadic.sub (x y : Dyadic) : Dyadic

Subtract two dyadic numbers.

@[implicit_reducible]

instance Dyadic.instSub : Sub Dyadic

def Dyadic.shiftLeft (x : Dyadic) (i : Int) : Dyadic

Shift a dyadic number left by i bits.

def Dyadic.shiftRight (x : Dyadic) (i : Int) : Dyadic

Shift a dyadic number right by i bits.

@[implicit_reducible]

instance Dyadic.instHShiftLeftInt : HShiftLeft Dyadic Int Dyadic

@[implicit_reducible]

instance Dyadic.instHShiftRightInt : HShiftRight Dyadic Int Dyadic

@[implicit_reducible]

instance Dyadic.instHShiftLeftNat : HShiftLeft Dyadic Nat Dyadic

@[implicit_reducible]

instance Dyadic.instHShiftRightNat : HShiftRight Dyadic Nat Dyadic

theorem Int.natAbs_emod_two (i : Int) : i.natAbs % 2 = (i % 2).natAbs

def Dyadic.toRat (x : Dyadic) : Rat

Convert a dyadic number to a rational number.

@[simp]

theorem Dyadic.zero_eq : zero = 0

@[simp]

theorem Dyadic.add_zero (x : Dyadic) : x + 0 = x

@[simp]

theorem Dyadic.zero_add (x : Dyadic) : 0 + x = x

@[simp]

theorem Dyadic.neg_zero : -0 = 0

@[simp]

theorem Dyadic.mul_zero (x : Dyadic) : x * 0 = 0

@[simp]

theorem Dyadic.zero_mul (x : Dyadic) : 0 * x = 0

@[simp]

theorem Dyadic.toRat_zero : toRat 0 = 0

theorem Rat.mkRat_one (x : Int) : mkRat x 1 = ↑x

theorem Dyadic.toRat_ofOdd_eq_mkRat {n k : Int} {hn : n % 2 = 1} : (ofOdd n k hn).toRat = mkRat (n <<< (-k).toNat) (1 <<< k.toNat)

theorem Dyadic.toRat_ofIntWithPrec_eq_mkRat {n k : Int} : (ofIntWithPrec n k).toRat = mkRat (n <<< (-k).toNat) (1 <<< k.toNat)

theorem Dyadic.toRat_ofIntWithPrec_eq_mul_two_pow {n k : Int} : (ofIntWithPrec n k).toRat = ↑n * 2 ^ (-k)

@[simp]

theorem Dyadic.toRat_add (x y : Dyadic) : (x + y).toRat = x.toRat + y.toRat

@[simp]

theorem Dyadic.toRat_neg (x : Dyadic) : (-x).toRat = -x.toRat

@[simp]

theorem Dyadic.toRat_sub (x y : Dyadic) : (x - y).toRat = x.toRat - y.toRat

@[simp]

theorem Dyadic.toRat_mul (x y : Dyadic) : (x * y).toRat = x.toRat * y.toRat

@[simp]

theorem Dyadic.pow_zero (x : Dyadic) : x ^ 0 = 1

theorem Dyadic.pow_succ (x : Dyadic) (n : Nat) : x ^ (n + 1) = x ^ n * x

@[simp]

theorem Dyadic.toRat_pow (x : Dyadic) (n : Nat) : (x ^ n).toRat = x.toRat ^ n

@[simp]

theorem Dyadic.toRat_intCast (x : Int) : (↑x).toRat = ↑x

@[simp]

theorem Dyadic.toRat_natCast (x : Nat) : (↑x).toRat = ↑x

@[simp]

theorem Dyadic.of_ne_zero {n k : Int} {hn : n % 2 = 1} : ofOdd n k hn ≠ 0

@[simp]

theorem Dyadic.zero_ne_of {n k : Int} {hn : n % 2 = 1} : 0 ≠ ofOdd n k hn

@[simp]

theorem Dyadic.toRat_eq_zero_iff {x : Dyadic} : x.toRat = 0 ↔ x = 0

theorem Dyadic.ofOdd_eq_ofIntWithPrec {n k : Int} {hn : n % 2 = 1} : ofOdd n k hn = ofIntWithPrec n k

theorem Dyadic.toRat_ofOdd_eq_mul_two_pow {n k : Int} {hn : n % 2 = 1} : (ofOdd n k hn).toRat = ↑n * 2 ^ (-k)

@[simp]

theorem Dyadic.ofIntWithPrec_zero {i : Int} : ofIntWithPrec 0 i = 0

@[simp]

theorem Dyadic.neg_ofOdd {n k : Int} {hn : n % 2 = 1} : -ofOdd n k hn = ofOdd (-n) k ⋯

@[simp]

theorem Dyadic.neg_ofIntWithPrec {i prec : Int} : -ofIntWithPrec i prec = ofIntWithPrec (-i) prec

theorem Dyadic.ofIntWithPrec_shiftLeft_add {x i : Int} {n : Nat} : ofIntWithPrec (x <<< n) (i + ↑n) = ofIntWithPrec x i

def Dyadic.precision : Dyadic → Option Int

The "precision" of a dyadic number, i.e. in n * 2^(-p) with n odd the precision is p.

theorem Dyadic.precision_ofIntWithPrec_le {i : Int} (h : i ≠ 0) (prec : Int) : (ofIntWithPrec i prec).precision ≤ some prec

@[simp]

theorem Dyadic.precision_zero : precision 0 = none

@[simp]

theorem Dyadic.precision_neg {x : Dyadic} : (-x).precision = x.precision

def Rat.toDyadic (x : Rat) (prec : Int) : Dyadic

Convert a rational number x to the greatest dyadic number with precision at most prec which is less than or equal to x.

theorem Rat.toDyadic_mkRat (a : Int) (b : Nat) (prec : Int) : (mkRat a b).toDyadic prec = Dyadic.ofIntWithPrec (a <<< prec.toNat / ↑(b <<< (-prec).toNat)) prec

theorem Rat.toDyadic_eq_ofIntWithPrec (x : Rat) (prec : Int) : x.toDyadic prec = Dyadic.ofIntWithPrec (x.num <<< prec.toNat / ↑(x.den <<< (-prec).toNat)) prec

theorem Rat.toRat_toDyadic (x : Rat) (prec : Int) : (x.toDyadic prec).toRat = ↑(x * 2 ^ prec).floor / 2 ^ prec

Converting a rational to a dyadic at a given precision and then back to a rational gives the same result as taking the floor of the rational at precision 2 ^ prec.

theorem Rat.toRat_toDyadic_le {x : Rat} {prec : Int} : (x.toDyadic prec).toRat ≤ x

theorem Rat.lt_toRat_toDyadic_add {x : Rat} {prec : Int} : x < (x.toDyadic prec + Dyadic.ofIntWithPrec 1 prec).toRat

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

Rounds a dyadic rational x down to the greatest dyadic number with precision at most prec which is less than or equal to x.

theorem Dyadic.roundDown_eq_self_of_le {x : Dyadic} {prec : Int} (h : x.precision ≤ some prec) : x.roundDown prec = x

@[simp]

theorem Dyadic.toDyadic_toRat (x : Dyadic) (prec : Int) : x.toRat.toDyadic prec = x.roundDown prec

theorem Dyadic.toRat_inj {x y : Dyadic} : x.toRat = y.toRat ↔ x = y

theorem Dyadic.add_comm (x y : Dyadic) : x + y = y + x

theorem Dyadic.add_assoc (x y z : Dyadic) : x + y + z = x + (y + z)

theorem Dyadic.mul_comm (x y : Dyadic) : x * y = y * x

theorem Dyadic.mul_assoc (x y z : Dyadic) : x * y * z = x * (y * z)

theorem Dyadic.mul_one (x : Dyadic) : x * 1 = x

theorem Dyadic.one_mul (x : Dyadic) : 1 * x = x

theorem Dyadic.add_mul (x y z : Dyadic) : (x + y) * z = x * z + y * z

theorem Dyadic.mul_add (x y z : Dyadic) : x * (y + z) = x * y + x * z

theorem Dyadic.neg_add_cancel (x : Dyadic) : -x + x = 0

theorem Dyadic.neg_mul (x y : Dyadic) : -x * y = -(x * y)

def Dyadic.blt (x y : Dyadic) : Bool

Determine if a dyadic rational is strictly less than another.

def Dyadic.ble (x y : Dyadic) : Bool

Determine if a dyadic rational is less than or equal to another.

theorem Dyadic.blt_iff_toRat {x y : Dyadic} : x.blt y = true ↔ x.toRat < y.toRat

theorem Dyadic.blt_eq_false_iff {x y : Dyadic} : x.blt y = false ↔ y.ble x = true

theorem Dyadic.ble_iff_toRat {x y : Dyadic} : x.ble y = true ↔ x.toRat ≤ y.toRat

@[implicit_reducible]

instance Dyadic.instLT : LT Dyadic

@[implicit_reducible]

instance Dyadic.instLE : LE Dyadic

@[implicit_reducible]

instance Dyadic.instDecidableLT : DecidableLT Dyadic

@[implicit_reducible]

instance Dyadic.instDecidableLE : DecidableLE Dyadic

@[simp]

theorem Dyadic.toRat_lt_toRat_iff {x y : Dyadic} : x.toRat < y.toRat ↔ x < y

@[simp]

theorem Dyadic.toRat_le_toRat_iff {x y : Dyadic} : x.toRat ≤ y.toRat ↔ x ≤ y

@[simp]

theorem Dyadic.not_le {x y : Dyadic} : ¬x < y ↔ y ≤ x

@[simp]

theorem Dyadic.not_lt {x y : Dyadic} : ¬x ≤ y ↔ y < x

@[simp]

theorem Dyadic.le_refl (x : Dyadic) : x ≤ x

theorem Dyadic.le_trans {x y z : Dyadic} (h : x ≤ y) (h' : y ≤ z) : x ≤ z

theorem Dyadic.le_antisymm {x y : Dyadic} (h : x ≤ y) (h' : y ≤ x) : x = y

theorem Dyadic.le_total (x y : Dyadic) : x ≤ y ∨ y ≤ x

instance Dyadic.instLawfulOrderLT : Std.LawfulOrderLT Dyadic

instance Dyadic.instIsPreorder : Std.IsPreorder Dyadic

instance Dyadic.instIsPartialOrder : Std.IsPartialOrder Dyadic

instance Dyadic.instIsLinearPreorder : Std.IsLinearPreorder Dyadic

instance Dyadic.instIsLinearOrder : Std.IsLinearOrder Dyadic

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

roundUp x prec is the least dyadic number with precision at most prec which is greater than or equal to x.

theorem Dyadic.roundUp_eq_neg_roundDown_neg (x : Dyadic) (prec : Int) : x.roundUp prec = -(-x).roundDown prec