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.

Todo

In the time since this file was created, Dyadic got added to Lean core. We've temporarily renamed our implementation to Dyadic'. In the near future, these two implementations will be merged.

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.

TODO: replace this with Dyadic from Lean core.

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'

instance Dyadic'.instArchimedean : Archimedean 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

def Dyadic'.coeRingHom : Dyadic' →+* ℚ

Coercion as a RingHom.

Equations

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

@[simp]

theorem Dyadic'.coeRingHom_apply (self : Subtype IsDyadic) : coeRingHom self = ↑self