Dyadic numbers

A dyadic (rational) number is a rational number whose denominator is a power of two. We define them as a subtype of ℚ, and build the CommRing structure, as well as proving some auxiliary theorems on them.

This material belongs in Mathlib, though we do need to consider if the definition of Dyadic used here is the best one.

For Mathlib

theorem le_of_le_of_lt_of_lt {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] {x y : α} {f : α → β} (h : x < y → f x < f y) (hxy : x ≤ y) : f x ≤ f y

theorem Nat.pow_log_eq_self_iff {b n : ℕ} (hb : b ≠ 0) : b ^ log b n = n ↔ n ∈ Set.range fun (x : ℕ) => b ^ x

theorem Set.range_if {α : Type u_1} {β : Type u_2} {p : α → Prop} [DecidablePred p] {x y : β} (hp : ∃ (a : α), p a) (hn : ∃ (a : α), ¬p a) : (range fun (a : α) => if p a then x else y) = {x, y}

theorem range_zero_pow {M : Type u_1} [MonoidWithZero M] : (Set.range fun (x : ℕ) => 0 ^ x) = {1, 0}

instance instDecidableMemNatSetRangeHPow_combinatorialGames (b n : ℕ) : Decidable (n ∈ Set.range fun (x : ℕ) => b ^ x)

Equations

• instDecidableMemNatSetRangeHPow_combinatorialGames 0 n = decidable_of_iff (n ∈ {1, 0}) ⋯
• instDecidableMemNatSetRangeHPow_combinatorialGames b_2.succ n = decidable_of_iff ((b_2 + 1) ^ Nat.log (b_2 + 1) n = n) ⋯

theorem pos_of_mem_powers {n : ℕ} (h : n ∈ Submonoid.powers 2) : 0 < n

theorem ne_zero_of_mem_powers {n : ℕ} (h : n ∈ Submonoid.powers 2) : n ≠ 0

theorem dvd_iff_le_of_mem_powers {m n : ℕ} (hm : m ∈ Submonoid.powers 2) (hn : n ∈ Submonoid.powers 2) : m ∣ n ↔ m ≤ n

Dyadic numbers

def IsDyadic (x : ℚ) : Prop

A dyadic rational number is one whose denominator is a power of two.

Equations

• IsDyadic x = (x.den ∈ Submonoid.powers 2)

instance instDecidableMemNatSubmonoidPowers_combinatorialGames {m n : ℕ} : Decidable (m ∈ Submonoid.powers n)

Equations

• instDecidableMemNatSubmonoidPowers_combinatorialGames = decidable_of_iff (m ∈ Set.range fun (x : ℕ) => n ^ x) ⋯

instance instDecidablePredRatIsDyadic : DecidablePred IsDyadic

Equations

• instDecidablePredRatIsDyadic x = inferInstanceAs (Decidable (x.den ∈ Submonoid.powers 2))

theorem IsDyadic.mkRat (x : ℤ) {y : ℕ} (hy : y ∈ Submonoid.powers 2) : IsDyadic (_root_.mkRat x y)

theorem IsDyadic.neg {x : ℚ} (hx : IsDyadic x) : IsDyadic (-x)

@[simp]

theorem IsDyadic.neg_iff {x : ℚ} : IsDyadic (-x) ↔ IsDyadic x

theorem IsDyadic.natCast (n : ℕ) : IsDyadic ↑n

theorem IsDyadic.intCast (n : ℤ) : IsDyadic ↑n

theorem IsDyadic.add {x y : ℚ} (hx : IsDyadic x) (hy : IsDyadic y) : IsDyadic (x + y)

theorem IsDyadic.sub {x y : ℚ} (hx : IsDyadic x) (hy : IsDyadic y) : IsDyadic (x - y)

theorem IsDyadic.mul {x y : ℚ} (hx : IsDyadic x) (hy : IsDyadic y) : IsDyadic (x * y)

theorem IsDyadic.nsmul {x : ℚ} (n : ℕ) (hx : IsDyadic x) : IsDyadic (n • x)

theorem IsDyadic.zsmul {x : ℚ} (n : ℤ) (hx : IsDyadic x) : IsDyadic (n • x)

theorem IsDyadic.pow {x : ℚ} (hx : IsDyadic x) (n : ℕ) : IsDyadic (x ^ n)

@[reducible, inline]

abbrev Dyadic : Type

The subtype of IsDyadic numbers.

We don't use Localization.Away 2, as this would not give us any computability, nor would it allow us to talk about numerators and denominators.

Equations

• Dyadic = Subtype IsDyadic

theorem Dyadic.le_def {x y : Dyadic} : x ≤ y ↔ ↑x ≤ ↑y

theorem Dyadic.lt_def {x y : Dyadic} : x < y ↔ ↑x < ↑y

@[reducible, inline]

abbrev Dyadic.num (x : Dyadic) : ℤ

Numerator of a dyadic number.

Equations

• x.num = (↑x).num

@[reducible, inline]

abbrev Dyadic.den (x : Dyadic) : ℕ

Denominator of a dyadic number.

Equations

• x.den = (↑x).den

theorem Dyadic.den_ne_zero (x : Dyadic) : x.den ≠ 0

theorem Dyadic.den_pos (x : Dyadic) : 0 < x.den

theorem Dyadic.den_mem_powers (x : Dyadic) : x.den ∈ Submonoid.powers 2

theorem Dyadic.one_le_den (x : Dyadic) : 1 ≤ x.den

@[simp]

theorem Dyadic.den_le_one_iff_eq_one {x : Dyadic} : x.den ≤ 1 ↔ x.den = 1

@[simp]

theorem Dyadic.one_lt_den_iff_ne_one {x : Dyadic} : 1 < x.den ↔ x.den ≠ 1

theorem Dyadic.den_ne_one_of_den_lt {x y : Dyadic} (h : x.den < y.den) : y.den ≠ 1

theorem Dyadic.ext {x y : Dyadic} (h : ↑x = ↑y) : x = y

theorem Dyadic.ext_iff {x y : Dyadic} : x = y ↔ ↑x = ↑y

instance Dyadic.instNatCast : NatCast Dyadic

Equations

• Dyadic.instNatCast = { natCast := fun (n : ℕ) => ⟨↑n, ⋯⟩ }

@[simp]

theorem Dyadic.val_natCast (n : ℕ) : ↑↑n = ↑n

@[simp]

theorem Dyadic.num_natCast (n : ℕ) : (↑n).num = ↑n

@[simp]

theorem Dyadic.den_natCast (n : ℕ) : (↑n).den = 1

@[simp]

theorem Dyadic.val_ofNat (n : ℕ) [n.AtLeastTwo] : ↑(OfNat.ofNat n) = ↑n

@[simp]

theorem Dyadic.num_ofNat (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).num = ↑n

@[simp]

theorem Dyadic.den_ofNat (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).den = 1

@[simp]

theorem Dyadic.natCast_lt_val {x : ℕ} {y : Dyadic} : ↑x < ↑y ↔ ↑x < y

@[simp]

theorem Dyadic.natCast_le_val {x : ℕ} {y : Dyadic} : ↑x ≤ ↑y ↔ ↑x ≤ y

@[simp]

theorem Dyadic.val_lt_natCast {x : Dyadic} {y : ℕ} : ↑x < ↑y ↔ x < ↑y

@[simp]

theorem Dyadic.val_le_natCast {x : Dyadic} {y : ℕ} : ↑x ≤ ↑y ↔ x ≤ ↑y

@[simp]

theorem Dyadic.val_eq_natCast {x : Dyadic} {y : ℕ} : ↑x = ↑y ↔ x = ↑y

@[simp]

theorem Dyadic.natCast_eq_val {x : ℕ} {y : Dyadic} : ↑x = ↑y ↔ ↑x = y

instance Dyadic.instIntCast : IntCast Dyadic

Equations

• Dyadic.instIntCast = { intCast := fun (n : ℤ) => ⟨↑n, ⋯⟩ }

@[simp]

theorem Dyadic.val_intCast (n : ℤ) : ↑↑n = ↑n

@[simp]

theorem Dyadic.mk_intCast {n : ℤ} (h : IsDyadic ↑n) : ⟨↑n, h⟩ = ↑n

@[simp]

theorem Dyadic.num_intCast (n : ℤ) : (↑n).num = n

@[simp]

theorem Dyadic.den_intCast (n : ℤ) : (↑n).den = 1

@[simp]

theorem Dyadic.intCast_lt_val {x : ℤ} {y : Dyadic} : ↑x < ↑y ↔ ↑x < y

@[simp]

theorem Dyadic.intCast_le_val {x : ℤ} {y : Dyadic} : ↑x ≤ ↑y ↔ ↑x ≤ y

@[simp]

theorem Dyadic.val_lt_intCast {x : Dyadic} {y : ℤ} : ↑x < ↑y ↔ x < ↑y

@[simp]

theorem Dyadic.val_le_intCast {x : Dyadic} {y : ℤ} : ↑x ≤ ↑y ↔ x ≤ ↑y

@[simp]

theorem Dyadic.val_eq_intCast {x : Dyadic} {y : ℤ} : ↑x = ↑y ↔ x = ↑y

@[simp]

theorem Dyadic.intCast_eq_val {x : ℤ} {y : Dyadic} : ↑x = ↑y ↔ ↑x = y

instance Dyadic.instZero : Zero Dyadic

Equations

• Dyadic.instZero = { zero := ↑0 }

instance Dyadic.instInhabited : Inhabited Dyadic

Equations

• Dyadic.instInhabited = { default := 0 }

@[simp]

theorem Dyadic.val_zero : ↑0 = 0

@[simp]

theorem Dyadic.mk_zero (h : IsDyadic 0) : ⟨0, h⟩ = 0

@[simp]

theorem Dyadic.num_zero : num 0 = 0

@[simp]

theorem Dyadic.den_zero : den 0 = 1

@[simp]

theorem Dyadic.zero_lt_val {x : Dyadic} : 0 < ↑x ↔ 0 < x

@[simp]

theorem Dyadic.zero_le_val {x : Dyadic} : 0 ≤ ↑x ↔ 0 ≤ x

@[simp]

theorem Dyadic.val_lt_zero {x : Dyadic} : ↑x < 0 ↔ x < 0

@[simp]

theorem Dyadic.val_le_zero {x : Dyadic} : ↑x ≤ 0 ↔ x ≤ 0

@[simp]

theorem Dyadic.val_eq_zero {x : Dyadic} : ↑x = 0 ↔ x = 0

@[simp]

theorem Dyadic.zero_eq_val {x : Dyadic} : 0 = ↑x ↔ 0 = x

instance Dyadic.instOne : One Dyadic

Equations

• Dyadic.instOne = { one := ↑1 }

@[simp]

theorem Dyadic.val_one : ↑1 = 1

@[simp]

theorem Dyadic.mk_one (h : IsDyadic 1) : ⟨1, h⟩ = 1

@[simp]

theorem Dyadic.num_one : num 1 = 1

@[simp]

theorem Dyadic.den_one : den 1 = 1

@[simp]

theorem Dyadic.one_lt_val {x : Dyadic} : 1 < ↑x ↔ 1 < x

@[simp]

theorem Dyadic.one_le_val {x : Dyadic} : 1 ≤ ↑x ↔ 1 ≤ x

@[simp]

theorem Dyadic.val_lt_one {x : Dyadic} : ↑x < 1 ↔ x < 1

@[simp]

theorem Dyadic.val_le_one {x : Dyadic} : ↑x ≤ 1 ↔ x ≤ 1

@[simp]

theorem Dyadic.val_eq_one {x : Dyadic} : ↑x = 1 ↔ x = 1

@[simp]

theorem Dyadic.one_eq_val {x : Dyadic} : 1 = ↑x ↔ 1 = x

instance Dyadic.instNontrivial : Nontrivial Dyadic

instance Dyadic.instNeg : Neg Dyadic

Equations

• Dyadic.instNeg = { neg := fun (x : Dyadic) => ⟨-↑x, ⋯⟩ }

@[simp]

theorem Dyadic.val_neg (x : Dyadic) : ↑(-x) = -↑x

@[simp]

theorem Dyadic.neg_mk {x : ℚ} (hx : IsDyadic x) : -⟨x, hx⟩ = ⟨-x, ⋯⟩

@[simp]

theorem Dyadic.num_neg (x : Dyadic) : (-x).num = -x.num

@[simp]

theorem Dyadic.den_neg (x : Dyadic) : (-x).den = x.den

instance Dyadic.instAdd : Add Dyadic

Equations

• Dyadic.instAdd = { add := fun (x y : Dyadic) => ⟨↑x + ↑y, ⋯⟩ }

@[simp]

theorem Dyadic.val_add (x y : Dyadic) : ↑(x + y) = ↑x + ↑y

instance Dyadic.instSub : Sub Dyadic

Equations

• Dyadic.instSub = { sub := fun (x y : Dyadic) => ⟨↑x - ↑y, ⋯⟩ }

@[simp]

theorem Dyadic.val_sub (x y : Dyadic) : ↑(x - y) = ↑x - ↑y

instance Dyadic.instMul : Mul Dyadic

Equations

• Dyadic.instMul = { mul := fun (x y : Dyadic) => ⟨↑x * ↑y, ⋯⟩ }

@[simp]

theorem Dyadic.val_mul (x y : Dyadic) : ↑(x * y) = ↑x * ↑y

instance Dyadic.instSMulNat : SMul ℕ Dyadic

Equations

• Dyadic.instSMulNat = { smul := fun (x : ℕ) (y : Dyadic) => ⟨x • ↑y, ⋯⟩ }

@[simp]

theorem Dyadic.val_nsmul (x : ℕ) (y : Dyadic) : ↑(x • y) = x • ↑y

instance Dyadic.instSMulInt : SMul ℤ Dyadic

Equations

• Dyadic.instSMulInt = { smul := fun (x : ℤ) (y : Dyadic) => ⟨x • ↑y, ⋯⟩ }

@[simp]

theorem Dyadic.val_zsmul (x : ℤ) (y : Dyadic) : ↑(x • y) = x • ↑y

instance Dyadic.instNatPow : NatPow Dyadic

Equations

• Dyadic.instNatPow = { pow := fun (x : Dyadic) (y : ℕ) => ⟨↑x ^ y, ⋯⟩ }

@[simp]

theorem Dyadic.val_pow (x : Dyadic) (y : ℕ) : ↑(x ^ y) = ↑x ^ y

def Dyadic.half : Dyadic

The dyadic number ½.

Equations

• Dyadic.half = ⟨2⁻¹, Dyadic.half._proof_1⟩

@[simp]

theorem Dyadic.val_half : ↑half = 2⁻¹

@[simp]

theorem Dyadic.num_half : half.num = 1

@[simp]

theorem Dyadic.num_den : half.den = 2

def Dyadic.mkRat (m : ℤ) {n : ℕ} (h : n ∈ Submonoid.powers 2) : Dyadic

Constructor for the fraction m / n.

Equations

• Dyadic.mkRat m h = ⟨mkRat m n, ⋯⟩

@[simp]

theorem Dyadic.val_mkRat (m : ℤ) {n : ℕ} (h : n ∈ Submonoid.powers 2) : ↑(Dyadic.mkRat m h) = mkRat m n

@[simp]

theorem Dyadic.mkRat_self (x : Dyadic) : Dyadic.mkRat x.num ⋯ = x

@[simp]

theorem Dyadic.mkRat_one (m : ℤ) (h : 1 ∈ Submonoid.powers 2) : Dyadic.mkRat m h = ↑m

@[simp]

theorem Dyadic.mkRat_lt_mkRat {m n : ℤ} {k : ℕ} (h₁ h₂ : k ∈ Submonoid.powers 2) : Dyadic.mkRat m h₁ < Dyadic.mkRat n h₂ ↔ m < n

@[simp]

theorem Dyadic.mkRat_le_mkRat {m n : ℤ} {k : ℕ} (h₁ h₂ : k ∈ Submonoid.powers 2) : Dyadic.mkRat m h₁ ≤ Dyadic.mkRat n h₂ ↔ m ≤ n

theorem Dyadic.mkRat_add_mkRat_self {m n : ℤ} {k : ℕ} (h₁ h₂ : k ∈ Submonoid.powers 2) : Dyadic.mkRat m h₁ + Dyadic.mkRat n h₂ = Dyadic.mkRat (m + n) h₁

instance Dyadic.instCommRing : CommRing Dyadic

Equations

• One or more equations did not get rendered due to their size.

instance Dyadic.instIsStrictOrderedRing : IsStrictOrderedRing Dyadic

instance Dyadic.instDenselyOrdered : DenselyOrdered Dyadic

theorem Dyadic.even_den {x : Dyadic} (hx : x.den ≠ 1) : Even x.den

theorem Dyadic.odd_num {x : Dyadic} (hx : x.den ≠ 1) : Odd x.num

theorem Dyadic.intCast_num_eq_self_of_den_eq_one {x : Dyadic} (hx : x.den = 1) : ↑x.num = x

theorem Dyadic.den_mkRat_le (x : ℤ) {n : ℕ} (hn : n ≠ 0) : (mkRat x n).den ≤ n

theorem Dyadic.den_mkRat_lt {x : Dyadic} {n : ℤ} (hn : 2 ∣ n) (hd : x.den ≠ 1) : (mkRat n x.den).den < x.den

theorem Dyadic.den_add_self_lt {x : Dyadic} (hx : x.den ≠ 1) : (x + x).den < x.den

theorem Dyadic.eq_mkRat_of_den_le {x : Dyadic} {n : ℕ} (h : x.den ≤ n) (hn : n ∈ Submonoid.powers 2) : ∃ (m : ℤ), x = Dyadic.mkRat m hn

instance Dyadic.instCanLiftIntCastEqNatDenValRatIsDyadicOfNat : CanLift Dyadic ℤ Int.cast fun (x : Dyadic) => (↑x).den = 1

theorem Dyadic.den_add_le_den_right {x y : Dyadic} (h : x.den ≤ y.den) : (x + y).den ≤ y.den