Documentation

CombinatorialGames.Mathlib.Dyadic

Dyadic numbers #

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

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 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

theorem Dyadic.le_def {x y : Dyadic} :

x ≤ y ↔ x.toRat ≤ y.toRat

theorem Dyadic.lt_def {x y : Dyadic} :

x < y ↔ x.toRat < y.toRat

@[reducible, inline]

abbrev Dyadic.num (x : Dyadic) :

Numerator of a dyadic number.

Equations

x.num = x.toRat.num

Instances For

@[reducible, inline]

abbrev Dyadic.den (x : Dyadic) :

Denominator of a dyadic number.

Equations

x.den = x.toRat.den

Instances For

theorem Dyadic.den_ne_zero (x : Dyadic) :

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) :

@[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) :

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

x = y

theorem Dyadic.ext_iff {x y : Dyadic} :

x = y ↔ x.toRat = y.toRat

@[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).toRat = ↑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.toRat ↔ ↑x < y

@[simp]

theorem Dyadic.natCast_le_val {x : ℕ} {y : Dyadic} :

↑x ≤ y.toRat ↔ ↑x ≤ y

@[simp]

theorem Dyadic.val_lt_natCast {x : Dyadic} {y : ℕ} :

x.toRat < ↑y ↔ x < ↑y

@[simp]

theorem Dyadic.val_le_natCast {x : Dyadic} {y : ℕ} :

x.toRat ≤ ↑y ↔ x ≤ ↑y

@[simp]

theorem Dyadic.val_eq_natCast {x : Dyadic} {y : ℕ} :

x.toRat = ↑y ↔ x = ↑y

@[simp]

theorem Dyadic.natCast_eq_val {x : ℕ} {y : Dyadic} :

↑x = y.toRat ↔ ↑x = y

@[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.toRat ↔ ↑x < y

@[simp]

theorem Dyadic.intCast_le_val {x : ℤ} {y : Dyadic} :

↑x ≤ y.toRat ↔ ↑x ≤ y

@[simp]

theorem Dyadic.val_lt_intCast {x : Dyadic} {y : ℤ} :

x.toRat < ↑y ↔ x < ↑y

@[simp]

theorem Dyadic.val_le_intCast {x : Dyadic} {y : ℤ} :

x.toRat ≤ ↑y ↔ x ≤ ↑y

@[simp]

theorem Dyadic.val_eq_intCast {x : Dyadic} {y : ℤ} :

x.toRat = ↑y ↔ x = ↑y

@[simp]

theorem Dyadic.intCast_eq_val {x : ℤ} {y : Dyadic} :

↑x = y.toRat ↔ ↑x = y

instance Dyadic.instInhabited_combinatorialGames :

Inhabited Dyadic

Equations

Dyadic.instInhabited_combinatorialGames = { default := 0 }

@[simp]

theorem Dyadic.val_zero :

@[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.toRat ↔ 0 < x

@[simp]

theorem Dyadic.zero_le_val {x : Dyadic} :

0 ≤ x.toRat ↔ 0 ≤ x

@[simp]

theorem Dyadic.val_lt_zero {x : Dyadic} :

x.toRat < 0 ↔ x < 0

@[simp]

theorem Dyadic.val_le_zero {x : Dyadic} :

x.toRat ≤ 0 ↔ x ≤ 0

@[simp]

theorem Dyadic.val_eq_zero {x : Dyadic} :

x.toRat = 0 ↔ x = 0

@[simp]

theorem Dyadic.zero_eq_val {x : Dyadic} :

0 = x.toRat ↔ 0 = x

@[simp]

theorem Dyadic.val_one :

@[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.toRat ↔ 1 < x

@[simp]

theorem Dyadic.one_le_val {x : Dyadic} :

1 ≤ x.toRat ↔ 1 ≤ x

@[simp]

theorem Dyadic.val_lt_one {x : Dyadic} :

x.toRat < 1 ↔ x < 1

@[simp]

theorem Dyadic.val_le_one {x : Dyadic} :

x.toRat ≤ 1 ↔ x ≤ 1

@[simp]

theorem Dyadic.val_eq_one {x : Dyadic} :

x.toRat = 1 ↔ x = 1

@[simp]

theorem Dyadic.one_eq_val {x : Dyadic} :

1 = x.toRat ↔ 1 = x

instance Dyadic.instNontrivial_combinatorialGames :

Nontrivial Dyadic

@[simp]

theorem Dyadic.num_neg (x : Dyadic) :

(-x).num = -x.num

@[simp]

theorem Dyadic.den_neg (x : Dyadic) :

(-x).den = x.den

instance Dyadic.instSMulNat_combinatorialGames :

SMul ℕ Dyadic

Equations

Dyadic.instSMulNat_combinatorialGames = { smul := fun (x : ℕ) (y : Dyadic) => ↑x * y }

@[simp]

theorem Dyadic.val_nsmul (x : ℕ) (y : Dyadic) :

(x • y).toRat = x • y.toRat

instance Dyadic.instSMulInt_combinatorialGames :

SMul ℤ Dyadic

Equations

Dyadic.instSMulInt_combinatorialGames = { smul := fun (x : ℤ) (y : Dyadic) => ↑x * y }

@[simp]

theorem Dyadic.val_zsmul (x : ℤ) (y : Dyadic) :

(x • y).toRat = x • y.toRat

def Dyadic.half :

The dyadic number ½.

Equations

Dyadic.half = 1 >>> 1

Instances For

@[simp]

theorem Dyadic.val_half :

half.toRat = 2⁻¹

@[simp]

theorem Dyadic.num_half :

@[simp]

theorem Dyadic.num_den :

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

Constructor for the fraction m / n.

Equations

Dyadic.mkRat m h = Dyadic.ofIntWithPrec m ↑(Submonoid.log ⟨n, h⟩)

Instances For

@[simp]

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

(Dyadic.mkRat m h).toRat = 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

instance Dyadic.instLinearOrder_combinatorialGames :

LinearOrder Dyadic

Equations

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

@[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_combinatorialGames :

CommRing Dyadic

Equations

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

instance Dyadic.instIsStrictOrderedRing_combinatorialGames :

IsStrictOrderedRing Dyadic

instance Dyadic.instDenselyOrdered_combinatorialGames :

DenselyOrdered Dyadic

instance Dyadic.instArchimedean_combinatorialGames :

Archimedean Dyadic

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

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

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.instCanLiftIntCastEqNatDenOfNat :

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

Dyadic.coeRingHom = { toFun := Dyadic.toRat, map_one' := Dyadic.coeRingHom._proof_1, map_mul' := Dyadic.toRat_mul, map_zero' := Dyadic.coeRingHom._proof_2, map_add' := Dyadic.toRat_add }

Instances For

@[simp]

theorem Dyadic.coeRingHom_apply (x : Dyadic) :

coeRingHom x = x.toRat