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

@[instance_reducible]

instance Dyadic.instCoeRat_combinatorialGames :

Equations

Dyadic.instCoeRat_combinatorialGames = { coe := Dyadic.toRat }

theorem Dyadic.coe_le_coe {x y : Dyadic} :

↑x ≤ ↑y ↔ x ≤ y

Alias of Dyadic.toRat_le_toRat_iff.

theorem Dyadic.coe_lt_coe {x y : Dyadic} :

↑x < ↑y ↔ x < y

Alias of Dyadic.toRat_lt_toRat_iff.

theorem Dyadic.coe_inj {x y : Dyadic} :

↑x = ↑y ↔ x = y

Alias of Dyadic.toRat_inj.

@[reducible, inline]

abbrev Dyadic.num (x : Dyadic) :

Numerator of a dyadic number.

Equations

x.num = (↑x).num

Instances For

@[reducible, inline]

abbrev Dyadic.den (x : Dyadic) :

Denominator of a dyadic number.

Equations

x.den = (↑x).den

Instances For

theorem Dyadic.den_ne_zero (x : Dyadic) :

theorem Dyadic.den_pos (x : Dyadic) :

0 < x.den

theorem Dyadic.one_le_den (x : Dyadic) :

theorem Dyadic.den_mem_powers (x : Dyadic) :

x.den ∈ Submonoid.powers 2

theorem Dyadic.den_eq_two_pow_toNat_precision (x : Dyadic) :

x.den = 2 ^ (x.precision.getD 0).toNat

theorem Dyadic.precision_eq_none {x : Dyadic} :

x.precision = none ↔ x = 0

theorem Dyadic.isSome_precision_eq_true {x : Dyadic} :

x.precision.isSome = true ↔ x ≠ 0

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

x.precision.isSome = true

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

x = y

theorem Dyadic.ext_iff {x y : Dyadic} :

x = y ↔ ↑x = ↑y

theorem Dyadic.coe_natCast (x : ℕ) :

↑↑x = ↑x

Alias of Dyadic.toRat_natCast.

@[simp]

theorem Dyadic.num_natCast (n : ℕ) :

(↑n).num = ↑n

@[simp]

theorem Dyadic.den_natCast (n : ℕ) :

(↑n).den = 1

@[simp]

theorem Dyadic.coe_ofNat (n : ℕ) :

↑(OfNat.ofNat n) = ↑n

@[simp]

theorem Dyadic.num_ofNat (n : ℕ) :

(OfNat.ofNat n).num = ↑n

@[simp]

theorem Dyadic.den_ofNat (n : ℕ) :

(OfNat.ofNat n).den = 1

@[simp]

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

↑x < ↑y ↔ ↑x < y

@[simp]

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

↑x ≤ ↑y ↔ ↑x ≤ y

@[simp]

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

↑x < ↑y ↔ x < ↑y

@[simp]

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

↑x ≤ ↑y ↔ x ≤ ↑y

@[simp]

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

↑x = ↑y ↔ x = ↑y

@[simp]

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

↑x = ↑y ↔ ↑x = y

theorem Dyadic.coe_intCast (x : ℤ) :

↑↑x = ↑x

Alias of Dyadic.toRat_intCast.

@[simp]

theorem Dyadic.num_intCast (n : ℤ) :

(↑n).num = n

@[simp]

theorem Dyadic.den_intCast (n : ℤ) :

(↑n).den = 1

@[simp]

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

↑x < ↑y ↔ ↑x < y

@[simp]

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

↑x ≤ ↑y ↔ ↑x ≤ y

@[simp]

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

↑x < ↑y ↔ x < ↑y

@[simp]

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

↑x ≤ ↑y ↔ x ≤ ↑y

@[simp]

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

↑x = ↑y ↔ x = ↑y

@[simp]

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

↑x = ↑y ↔ ↑x = y

@[instance_reducible]

instance Dyadic.instInhabited_combinatorialGames :

Inhabited Dyadic

Equations

Dyadic.instInhabited_combinatorialGames = { default := 0 }

@[simp]

theorem Dyadic.coe_zero :

↑0 = 0

@[simp]

theorem Dyadic.num_zero :

num 0 = 0

@[simp]

theorem Dyadic.den_zero :

den 0 = 1

@[simp]

theorem Dyadic.zero_lt_coe {x : Dyadic} :

0 < ↑x ↔ 0 < x

@[simp]

theorem Dyadic.zero_le_coe {x : Dyadic} :

0 ≤ ↑x ↔ 0 ≤ x

@[simp]

theorem Dyadic.coe_lt_zero {x : Dyadic} :

↑x < 0 ↔ x < 0

@[simp]

theorem Dyadic.coe_le_zero {x : Dyadic} :

↑x ≤ 0 ↔ x ≤ 0

theorem Dyadic.coe_eq_zero {x : Dyadic} :

↑x = 0 ↔ x = 0

Alias of Dyadic.toRat_eq_zero_iff.

@[simp]

theorem Dyadic.zero_eq_coe {x : Dyadic} :

0 = ↑x ↔ 0 = x

@[simp]

theorem Dyadic.coe_one :

↑1 = 1

@[simp]

theorem Dyadic.num_one :

num 1 = 1

@[simp]

theorem Dyadic.den_one :

den 1 = 1

@[simp]

theorem Dyadic.one_lt_coe {x : Dyadic} :

1 < ↑x ↔ 1 < x

@[simp]

theorem Dyadic.one_le_coe {x : Dyadic} :

1 ≤ ↑x ↔ 1 ≤ x

@[simp]

theorem Dyadic.coe_lt_one {x : Dyadic} :

↑x < 1 ↔ x < 1

@[simp]

theorem Dyadic.coe_le_one {x : Dyadic} :

↑x ≤ 1 ↔ x ≤ 1

@[simp]

theorem Dyadic.coe_eq_one {x : Dyadic} :

↑x = 1 ↔ x = 1

@[simp]

theorem Dyadic.one_eq_coe {x : Dyadic} :

1 = ↑x ↔ 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

theorem Dyadic.coe_neg (x : Dyadic) :

↑(-x) = -↑x

Alias of Dyadic.toRat_neg.

theorem Dyadic.coe_add (x y : Dyadic) :

↑(x + y) = ↑x + ↑y

Alias of Dyadic.toRat_add.

theorem Dyadic.coe_sub (x y : Dyadic) :

↑(x - y) = ↑x - ↑y

Alias of Dyadic.toRat_sub.

theorem Dyadic.coe_mul (x y : Dyadic) :

↑(x * y) = ↑x * ↑y

Alias of Dyadic.toRat_mul.

theorem Dyadic.coe_pow (x : Dyadic) (n : ℕ) :

↑(x ^ n) = ↑x ^ n

Alias of Dyadic.toRat_pow.

@[instance_reducible]

instance Dyadic.instSMulNat_combinatorialGames :

SMul ℕ Dyadic

Equations

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

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

↑(x • y) = x • ↑y

@[instance_reducible]

instance Dyadic.instSMulInt_combinatorialGames :

SMul ℤ Dyadic

Equations

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

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

↑(x • y) = x • ↑y

def Dyadic.half :

The dyadic number ½.

Equations

Dyadic.half = 1 >>> 1

Instances For

@[simp]

theorem Dyadic.coe_half :

↑half = 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.coe_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

@[instance_reducible]

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

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.coe_mul, map_zero' := Dyadic.coeRingHom._proof_2, map_add' := Dyadic.coe_add }

Instances For

@[simp]

theorem Dyadic.coeRingHom_apply (x : Dyadic) :

coeRingHom x = ↑x