mathlibdocumentation

Dyadic numbers are obtained by localizing ℤ away from 2. They are the initial object in the category of rings with no 2-torsion.

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.

def pgame.pow_half  :

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 half. By definition, we have pow_half 0 = 0 and pow_half 1 = half and we prove later on that pow_half (n + 1) + pow_half (n + 1) ≈ pow_half n.

Equations
@[simp]
theorem pgame.pow_half_left_moves {n : } :
@[simp]
theorem pgame.pow_half_move_left {n : } {i : .left_moves} :
i = 0
@[simp]
theorem pgame.numeric_pow_half {n : } :

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

theorem pgame.zero_lt_pow_half {n : } :
theorem pgame.zero_le_pow_half {n : } :

The surreal number half.

Equations

Powers of the surreal number half.

Equations
@[simp]
theorem surreal.pow_half_zero  :
@[simp]
@[simp]
theorem surreal.nsmul_pow_two_pow_half (n : ) :
2 ^ n = 1
theorem surreal.zsmul_pow_two_pow_half (m : ) (n k : ) :
(m * 2 ^ n) surreal.pow_half (n + k) =
theorem surreal.dyadic_aux {m₁ m₂ : } {y₁ y₂ : } (h₂ : m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂) :
m₁ = m₂

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

Equations

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

Equations