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.

Equations

• i.trailingZeros = if h : i = 0 then 0 else Int.trailingZeros.aux i.natAbs i h ⋯ 0

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

Equations

• Int.trailingZeros.aux k_2.succ i hi hk_2 acc = if h : i % 2 = 0 then Int.trailingZeros.aux k_2 (i / 2) ⋯ ⋯ (acc + 1) else acc

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.

instance instDecidableEqDyadic : DecidableEq Dyadic

Equations

• instDecidableEqDyadic = instDecidableEqDyadic.decEq

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

Equations

• One or more equations did not get rendered due to their size.
• instDecidableEqDyadic.decEq Dyadic.zero Dyadic.zero = isTrue ⋯
• instDecidableEqDyadic.decEq Dyadic.zero (Dyadic.ofOdd n k hn) = isFalse ⋯
• instDecidableEqDyadic.decEq (Dyadic.ofOdd n k hn) Dyadic.zero = isFalse ⋯

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

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

Equations

• Dyadic.ofIntWithPrec i prec = if h : i = 0 then Dyadic.zero else Dyadic.ofOdd (i >>> i.trailingZeros) (prec - ↑i.trailingZeros) ⋯

def Dyadic.ofInt (i : Int) : Dyadic

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

Equations

• Dyadic.ofInt i = Dyadic.ofIntWithPrec i 0

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

Equations

• Dyadic.instOfNat n = { ofNat := Dyadic.ofInt ↑n }

instance Dyadic.instIntCast : IntCast Dyadic

Equations

• Dyadic.instIntCast = { intCast := Dyadic.ofInt }

instance Dyadic.instNatCast : NatCast Dyadic

Equations

• Dyadic.instNatCast = { natCast := fun (x : Nat) => Dyadic.ofInt ↑x }

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

Add two dyadic numbers.

Equations

• One or more equations did not get rendered due to their size.
• Dyadic.zero.add y = y
• x.add Dyadic.zero = x

instance Dyadic.instAdd : Add Dyadic

Equations

• Dyadic.instAdd = { add := Dyadic.add }

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

Multiply two dyadic numbers.

Equations

• Dyadic.zero.mul y = Dyadic.zero
• x.mul Dyadic.zero = Dyadic.zero
• (Dyadic.ofOdd n₁ k₁ hn₁).mul (Dyadic.ofOdd n₂ k₂ hn₂) = Dyadic.ofOdd (n₁ * n₂) (k₁ + k₂) ⋯

instance Dyadic.instMul : Mul Dyadic

Equations

• Dyadic.instMul = { mul := Dyadic.mul }

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

Multiply two dyadic numbers.

Equations

• Dyadic.zero.pow i = if i = 0 then 1 else 0
• (Dyadic.ofOdd n k hn).pow i = Dyadic.ofOdd (n ^ i) (k * ↑i) ⋯

instance Dyadic.instPowNat : Pow Dyadic Nat

Equations

• Dyadic.instPowNat = { pow := Dyadic.pow }

def Dyadic.neg (x : Dyadic) : Dyadic

Negate a dyadic number.

Equations

• Dyadic.zero.neg = Dyadic.zero
• (Dyadic.ofOdd n k hn).neg = Dyadic.ofOdd (-n) k ⋯

instance Dyadic.instNeg : Neg Dyadic

Equations

• Dyadic.instNeg = { neg := Dyadic.neg }

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

Subtract two dyadic numbers.

Equations

• x.sub y = x + -y

instance Dyadic.instSub : Sub Dyadic

Equations

• Dyadic.instSub = { sub := Dyadic.sub }

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

Shift a dyadic number left by i bits.

Equations

• Dyadic.zero.shiftLeft i = Dyadic.zero
• (Dyadic.ofOdd n k hn).shiftLeft i = Dyadic.ofOdd n (k - i) hn

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

Shift a dyadic number right by i bits.

Equations

• Dyadic.zero.shiftRight i = Dyadic.zero
• (Dyadic.ofOdd n k hn).shiftRight i = Dyadic.ofOdd n (k + i) hn

instance Dyadic.instHShiftLeftInt : HShiftLeft Dyadic Int Dyadic

Equations

• Dyadic.instHShiftLeftInt = { hShiftLeft := Dyadic.shiftLeft }

instance Dyadic.instHShiftRightInt : HShiftRight Dyadic Int Dyadic

Equations

• Dyadic.instHShiftRightInt = { hShiftRight := Dyadic.shiftRight }

instance Dyadic.instHShiftLeftNat : HShiftLeft Dyadic Nat Dyadic

Equations

• Dyadic.instHShiftLeftNat = { hShiftLeft := fun (x : Dyadic) (y : Nat) => x <<< ↑y }

instance Dyadic.instHShiftRightNat : HShiftRight Dyadic Nat Dyadic

Equations

• Dyadic.instHShiftRightNat = { hShiftRight := fun (x : Dyadic) (y : Nat) => x >>> ↑y }

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.

Equations

• Dyadic.zero.toRat = 0
• (Dyadic.ofOdd n (Int.ofNat k) hn).toRat = { num := n, den := 2 ^ k, den_nz := ⋯, reduced := ⋯ }
• (Dyadic.ofOdd n (Int.negSucc k) hn).toRat = ↑(n * ↑(2 ^ (k + 1)))

@[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.

Equations

• Dyadic.zero.precision = none
• (Dyadic.ofOdd n k hn).precision = some k

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.

Equations

• x.toDyadic (Int.ofNat n) = Dyadic.ofIntWithPrec (x.num <<< n / ↑x.den) (Int.ofNat n)
• x.toDyadic (Int.negSucc n) = Dyadic.ofIntWithPrec (x.num / ↑(x.den <<< (n + 1))) (Int.negSucc n)

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.

Equations

• Dyadic.zero.roundDown prec = Dyadic.zero
• (Dyadic.ofOdd n k hn).roundDown prec = match k - prec with | Int.ofNat l => Dyadic.ofIntWithPrec (n >>> l) prec | Int.negSucc a => Dyadic.ofOdd n k hn

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.

Equations

• Dyadic.zero.blt Dyadic.zero = false
• Dyadic.zero.blt (Dyadic.ofOdd n k hn) = decide (0 < n)
• (Dyadic.ofOdd n k hn).blt Dyadic.zero = decide (n < 0)
• (Dyadic.ofOdd a a_1 a_2).blt (Dyadic.ofOdd b b_1 b_2) = match b_1 - a_1 with | Int.ofNat l => decide (a <<< l < b) | Int.negSucc l => decide (a < b <<< (l + 1))

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

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

Equations

• Dyadic.zero.ble Dyadic.zero = true
• Dyadic.zero.ble (Dyadic.ofOdd n k hn) = decide (0 ≤ n)
• (Dyadic.ofOdd n k hn).ble Dyadic.zero = decide (n ≤ 0)
• (Dyadic.ofOdd a a_1 a_2).ble (Dyadic.ofOdd b b_1 b_2) = match b_1 - a_1 with | Int.ofNat l => decide (a <<< l ≤ b) | Int.negSucc l => decide (a ≤ b <<< (l + 1))

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

instance Dyadic.instLT : LT Dyadic

Equations

• Dyadic.instLT = { lt := fun (x y : Dyadic) => x.blt y = true }

instance Dyadic.instLE : LE Dyadic

Equations

• Dyadic.instLE = { le := fun (x y : Dyadic) => x.ble y = true }

instance Dyadic.instDecidableLT : DecidableLT Dyadic

Equations

• x✝¹.instDecidableLT x✝ = inferInstanceAs (Decidable (x✝¹.blt x✝ = true))

instance Dyadic.instDecidableLE : DecidableLE Dyadic

Equations

• x✝¹.instDecidableLE x✝ = inferInstanceAs (Decidable (x✝¹.ble x✝ = true))

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

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

@[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.

Equations

• Dyadic.zero.roundUp prec = Dyadic.zero
• (Dyadic.ofOdd n k hn).roundUp prec = match k - prec with | Int.ofNat l => Dyadic.ofIntWithPrec (-(-n) >>> l) prec | Int.negSucc a => Dyadic.ofOdd n k hn

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