Documentation

Mathlib.SetTheory.Surreal.Dyadic

Dyadic numbers #

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 SetTheory.PGame.powHalf :
ℕ → SetTheory.PGame

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

Equations
Instances For
    source
    @[simp]
    theorem SetTheory.PGame.powHalf_zero :
    SetTheory.PGame.powHalf 0 = 1
    source
    theorem SetTheory.PGame.powHalf_leftMoves (n : ℕ) :
    SetTheory.PGame.LeftMoves (SetTheory.PGame.powHalf n) = PUnit.{u_1 + 1}
    source
    theorem SetTheory.PGame.powHalf_zero_rightMoves :
    SetTheory.PGame.RightMoves (SetTheory.PGame.powHalf 0) = PEmpty.{u_1 + 1}
    source
    theorem SetTheory.PGame.powHalf_succ_rightMoves (n : ℕ) :
    SetTheory.PGame.RightMoves (SetTheory.PGame.powHalf (n + 1)) = PUnit.{u_1 + 1}
    source
    @[simp]
    theorem SetTheory.PGame.powHalf_moveLeft (n : ℕ) (i : SetTheory.PGame.LeftMoves (SetTheory.PGame.powHalf n)) :
    SetTheory.PGame.moveLeft (SetTheory.PGame.powHalf n) i = 0
    source
    @[simp]
    theorem SetTheory.PGame.powHalf_succ_moveRight (n : ℕ) (i : SetTheory.PGame.RightMoves (SetTheory.PGame.powHalf (n + 1))) :
    SetTheory.PGame.moveRight (SetTheory.PGame.powHalf (n + 1)) i = SetTheory.PGame.powHalf n
    source
    instance SetTheory.PGame.uniquePowHalfLeftMoves (n : ℕ) :
    Unique (SetTheory.PGame.LeftMoves (SetTheory.PGame.powHalf n))
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance SetTheory.PGame.isEmpty_powHalf_zero_rightMoves :
    IsEmpty (SetTheory.PGame.RightMoves (SetTheory.PGame.powHalf 0))
    Equations
    source
    instance SetTheory.PGame.uniquePowHalfSuccRightMoves (n : ℕ) :
    Unique (SetTheory.PGame.RightMoves (SetTheory.PGame.powHalf (n + 1)))
    Equations
    source
    @[simp]
    theorem SetTheory.PGame.birthday_half :
    SetTheory.PGame.birthday (SetTheory.PGame.powHalf 1) = 2
    source
    theorem SetTheory.PGame.numeric_powHalf (n : ℕ) :
    SetTheory.PGame.Numeric (SetTheory.PGame.powHalf n)

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

    source
    theorem SetTheory.PGame.powHalf_succ_lt_powHalf (n : ℕ) :
    SetTheory.PGame.powHalf (n + 1) < SetTheory.PGame.powHalf n
    source
    theorem SetTheory.PGame.powHalf_succ_le_powHalf (n : ℕ) :
    SetTheory.PGame.powHalf (n + 1) ≤ SetTheory.PGame.powHalf n
    source
    theorem SetTheory.PGame.powHalf_le_one (n : ℕ) :
    SetTheory.PGame.powHalf n ≤ 1
    source
    theorem SetTheory.PGame.powHalf_succ_lt_one (n : ℕ) :
    SetTheory.PGame.powHalf (n + 1) < 1
    source
    theorem SetTheory.PGame.powHalf_pos (n : ℕ) :
    0 < SetTheory.PGame.powHalf n
    source
    theorem SetTheory.PGame.zero_le_powHalf (n : ℕ) :
    0 ≤ SetTheory.PGame.powHalf n
    source
    theorem SetTheory.PGame.add_powHalf_succ_self_eq_powHalf (n : ℕ) :
    SetTheory.PGame.powHalf (n + 1) + SetTheory.PGame.powHalf (n + 1) ≈ SetTheory.PGame.powHalf n
    source
    theorem SetTheory.PGame.half_add_half_equiv_one :
    SetTheory.PGame.powHalf 1 + SetTheory.PGame.powHalf 1 ≈ 1
    source
    def Surreal.powHalf (n : ℕ) :
    Surreal

    Powers of the surreal number half.

    Equations
    Instances For
      source
      @[simp]
      theorem Surreal.powHalf_zero :
      Surreal.powHalf 0 = 1
      source
      @[simp]
      theorem Surreal.double_powHalf_succ_eq_powHalf (n : ℕ) :
      2 • Surreal.powHalf (Nat.succ n) = Surreal.powHalf n
      source
      @[simp]
      theorem Surreal.nsmul_pow_two_powHalf (n : ℕ) :
      2 ^ n • Surreal.powHalf n = 1
      source
      @[simp]
      theorem Surreal.nsmul_pow_two_powHalf' (n : ℕ) (k : ℕ) :
      2 ^ n • Surreal.powHalf (n + k) = Surreal.powHalf k
      source
      theorem Surreal.zsmul_pow_two_powHalf (m : ℤ) (n : ℕ) (k : ℕ) :
      (m * 2 ^ n) • Surreal.powHalf (n + k) = m • Surreal.powHalf k
      source
      theorem Surreal.dyadic_aux {m₁ : ℤ} {m₂ : ℤ} {y₁ : ℕ} {y₂ : ℕ} (h₂ : m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂) :
      m₁ • Surreal.powHalf y₂ = m₂ • Surreal.powHalf y₁
      source
      def Surreal.dyadicMap :
      Localization.Away 2 →+ Surreal

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem Surreal.dyadicMap_apply (m : ℤ) (p : ↥(Submonoid.powers 2)) :
        Surreal.dyadicMap (IsLocalization.mk' (Localization (Submonoid.powers 2)) m p) = m • Surreal.powHalf (Submonoid.log p)
        source
        theorem Surreal.dyadicMap_apply_pow (m : ℤ) (n : ℕ) :
        Surreal.dyadicMap (IsLocalization.mk' (Localization (Submonoid.powers 2)) m (Submonoid.pow 2 n)) = m • Surreal.powHalf n
        source
        @[simp]
        theorem Surreal.dyadicMap_apply_pow' (m : ℤ) (n : ℕ) :
        m • Surreal.powHalf (Submonoid.log (Submonoid.pow 2 n)) = m • Surreal.powHalf n
        source
        def Surreal.dyadic :
        Set Surreal

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

        Equations
        Instances For