mathlib3 documentation

set_theory.surreal.dyadic

Dyadic numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. Dyadic numbers are obtained by localizing ℤ away from 2. They are the initial object in the category of rings with no 2-torsion.

Dyadic surreal numbers #

We construct dyadic surreal numbers using the canonical map from ℤ[2 ^ {-1}] to surreals. As we currently do not have a ring structure on surreal we construct this map explicitly. Once we have the ring structure, this map can be constructed directly by sending 2 ^ {-1} to half.

Embeddings #

The above construction gives us an abelian group embedding of ℤ into surreal. The goal is to extend this to an embedding of dyadic rationals into surreal and use Cauchy sequences of dyadic rational numbers to construct an ordered field embedding of ℝ into surreal.

source
def pgame.pow_half  :
ℕ → pgame

For a natural number n, the pre-game pow_half (n + 1) is recursively defined as {0 | pow_half n}. These are the explicit expressions of powers of 1 / 2. By definition, we have pow_half 0 = 1 and pow_half 1 ≈ 1 / 2 and we prove later on that pow_half (n + 1) + pow_half (n + 1) ≈ pow_half n.

Equations
source
@[simp]
theorem pgame.pow_half_zero  :
pgame.pow_half 0 = 1
source
theorem pgame.pow_half_left_moves (n : ℕ) :
(pgame.pow_half n).left_moves = punit
source
theorem pgame.pow_half_zero_right_moves  :
(pgame.pow_half 0).right_moves = pempty
source
theorem pgame.pow_half_succ_right_moves (n : ℕ) :
(pgame.pow_half (n + 1)).right_moves = punit
source
@[simp]
theorem pgame.pow_half_move_left (n : ℕ) (i : (pgame.pow_half n).left_moves) :
(pgame.pow_half n).move_left i = 0
source
@[simp]
theorem pgame.pow_half_succ_move_right (n : ℕ) (i : (pgame.pow_half (n + 1)).right_moves) :
(pgame.pow_half (n + 1)).move_right i = pgame.pow_half n
source
@[protected, instance]
def pgame.unique_pow_half_left_moves (n : ℕ) :
unique (pgame.pow_half n).left_moves
Equations
source
@[protected, instance]
def pgame.is_empty_pow_half_zero_right_moves  :
is_empty (pgame.pow_half 0).right_moves
source
@[protected, instance]
def pgame.unique_pow_half_succ_right_moves (n : ℕ) :
unique (pgame.pow_half (n + 1)).right_moves
Equations
source
@[simp]
theorem pgame.birthday_half  :
(pgame.pow_half 1).birthday = 2
source
theorem pgame.numeric_pow_half (n : ℕ) :
(pgame.pow_half n).numeric

For all natural numbers n, the pre-games pow_half n are numeric.

source
theorem pgame.pow_half_succ_lt_pow_half (n : ℕ) :
pgame.pow_half (n + 1) < pgame.pow_half n
source
theorem pgame.pow_half_succ_le_pow_half (n : ℕ) :
pgame.pow_half (n + 1) ≤ pgame.pow_half n
source
theorem pgame.pow_half_le_one (n : ℕ) :
pgame.pow_half n ≤ 1
source
theorem pgame.pow_half_succ_lt_one (n : ℕ) :
pgame.pow_half (n + 1) < 1
source
theorem pgame.pow_half_pos (n : ℕ) :
0 < pgame.pow_half n
source
theorem pgame.zero_le_pow_half (n : ℕ) :
0 ≤ pgame.pow_half n
source
theorem pgame.add_pow_half_succ_self_eq_pow_half (n : ℕ) :
(pgame.pow_half (n + 1) + pgame.pow_half (n + 1)).equiv (pgame.pow_half n)
source
theorem pgame.half_add_half_equiv_one  :
(pgame.pow_half 1 + pgame.pow_half 1).equiv 1
source
def surreal.pow_half (n : ℕ) :
surreal

Powers of the surreal number half.

Equations
source
@[simp]
theorem surreal.pow_half_zero  :
surreal.pow_half 0 = 1
source
@[simp]
theorem surreal.double_pow_half_succ_eq_pow_half (n : ℕ) :
2 • surreal.pow_half n.succ = surreal.pow_half n
source
@[simp]
theorem surreal.nsmul_pow_two_pow_half (n : ℕ) :
2 ^ n • surreal.pow_half n = 1
source
@[simp]
theorem surreal.nsmul_pow_two_pow_half' (n k : ℕ) :
2 ^ n • surreal.pow_half (n + k) = surreal.pow_half k
source
theorem surreal.zsmul_pow_two_pow_half (m : ℤ) (n k : ℕ) :
(m * 2 ^ n) • surreal.pow_half (n + k) = m • surreal.pow_half k
source
theorem surreal.dyadic_aux {m₁ m₂ : ℤ} {y₁ y₂ : ℕ} (h₂ : m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂) :
m₁ • surreal.pow_half y₂ = m₂ • surreal.pow_half y₁
source
def surreal.dyadic_map  :
localization.away 2 →+ surreal

The additive monoid morphism dyadic_map sends ⟦⟨m, 2^n⟩⟧ to m • half ^ n.

Equations
source
@[simp]
theorem surreal.dyadic_map_apply (m : ℤ) (p : ↥(submonoid.powers 2)) :
⇑surreal.dyadic_map (is_localization.mk' (localization (submonoid.powers 2)) m p) = m • surreal.pow_half (submonoid.log p)
source
@[simp]
theorem surreal.dyadic_map_apply_pow (m : ℤ) (n : ℕ) :
⇑surreal.dyadic_map (is_localization.mk' (localization (submonoid.powers 2)) m (submonoid.pow 2 n)) = m • surreal.pow_half n
source
def surreal.dyadic  :
set surreal

We define dyadic surreals as the range of the map dyadic_map.

Equations