Documentation

CombinatorialGames.Surreal.Leading

Leading term and coefficient #

We define Surreal.leadingCoeff and Surreal.leadingTerm for the leading coefficient/term of a surreal's Hahn series.

We don't yet prove this characterization; rather, these functions are a key ingredient in defining the map from surreals into Hahn series.

Leading coefficient #

source
noncomputable def Surreal.leadingCoeff (x : Surreal) :
ℝ

The leading coefficient of a surreal's Hahn series.

Equations
Instances For
    source
    @[simp]
    theorem Surreal.leadingCoeff_realCast (r : ℝ) :
    (↑r).leadingCoeff = r
    source
    @[simp]
    theorem Surreal.leadingCoeff_ratCast (q : ℚ) :
    (↑q).leadingCoeff = ↑q
    source
    @[simp]
    theorem Surreal.leadingCoeff_intCast (n : ℤ) :
    (↑n).leadingCoeff = ↑n
    source
    @[simp]
    theorem Surreal.leadingCoeff_natCast (n : ℕ) :
    (↑n).leadingCoeff = ↑n
    source
    @[simp]
    theorem Surreal.leadingCoeff_zero :
    leadingCoeff 0 = 0
    source
    @[simp]
    theorem Surreal.leadingCoeff_one :
    leadingCoeff 1 = 1
    source
    @[simp]
    theorem Surreal.leadingCoeff_neg (x : Surreal) :
    (-x).leadingCoeff = -x.leadingCoeff
    source
    @[simp]
    theorem Surreal.leadingCoeff_mul (x y : Surreal) :
    (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff
    source
    @[simp]
    theorem Surreal.leadingCoeff_inv (x : Surreal) :
    x⁻¹.leadingCoeff = x.leadingCoeff⁻¹
    source
    @[simp]
    theorem Surreal.leadingCoeff_div (x y : Surreal) :
    (x / y).leadingCoeff = x.leadingCoeff / y.leadingCoeff
    source
    @[simp]
    theorem Surreal.leadingCoeff_wpow (x : Surreal) :
    (ω^ x).leadingCoeff = 1
    source
    @[simp]
    theorem Surreal.leadingCoeff_eq_zero {x : Surreal} :
    x.leadingCoeff = 0 ↔ x = 0
    source
    @[simp]
    theorem Surreal.leadingCoeff_nonneg_iff {x : Surreal} :
    0 ≤ x.leadingCoeff ↔ 0 ≤ x
    source
    @[simp]
    theorem Surreal.leadingCoeff_nonpos_iff {x : Surreal} :
    x.leadingCoeff ≤ 0 ↔ x ≤ 0
    source
    @[simp]
    theorem Surreal.leadingCoeff_pos_iff {x : Surreal} :
    0 < x.leadingCoeff ↔ 0 < x
    source
    @[simp]
    theorem Surreal.leadingCoeff_neg_iff {x : Surreal} :
    x.leadingCoeff < 0 ↔ x < 0
    source
    theorem Surreal.leadingCoeff_monotoneOn (x : Surreal) :
    MonotoneOn leadingCoeff (wlog ⁻¹' {x})
    source
    theorem Surreal.wlog_eq {x y : Surreal} {r : ℝ} (hr : r ≠ 0) (hL : ∀ s < r, ↑s * ω^ y ≤ x) (hR : ∀ s > r, x ≤ ↑s * ω^ y) :
    x.wlog = y
    source
    theorem Surreal.leadingCoeff_eq {x y : Surreal} {r : ℝ} (hr : r ≠ 0) (hL : ∀ s < r, ↑s * ω^ y ≤ x) (hR : ∀ s > r, x ≤ ↑s * ω^ y) :
    x.leadingCoeff = r
    source
    theorem Surreal.leadingCoeff_add_eq_left {x y : Surreal} (h : y <ᵥ x) :
    (x + y).leadingCoeff = x.leadingCoeff
    source
    theorem Surreal.leadingCoeff_add_eq_right {x y : Surreal} (h : y <ᵥ x) :
    (y + x).leadingCoeff = x.leadingCoeff
    source
    theorem Surreal.leadingCoeff_sub_eq_left {x y : Surreal} :
    y <ᵥ x → (x - y).leadingCoeff = x.leadingCoeff
    source
    theorem Surreal.leadingCoeff_sub_eq_right {x y : Surreal} :
    y <ᵥ x → (y - x).leadingCoeff = -x.leadingCoeff

    Leading term #

    source
    noncomputable def Surreal.leadingTerm (x : Surreal) :
    Surreal

    The leading term of a surreal's Hahn series.

    Equations
    Instances For
      source
      @[simp]
      theorem Surreal.leadingTerm_realCast (r : ℝ) :
      (↑r).leadingTerm = ↑r
      source
      @[simp]
      theorem Surreal.leadingTerm_ratCast (q : ℚ) :
      (↑q).leadingTerm = ↑q
      source
      @[simp]
      theorem Surreal.leadingTerm_intCast (n : ℤ) :
      (↑n).leadingTerm = ↑n
      source
      @[simp]
      theorem Surreal.leadingTerm_natCast (n : ℕ) :
      (↑n).leadingTerm = ↑n
      source
      @[simp]
      theorem Surreal.leadingTerm_zero :
      leadingTerm 0 = 0
      source
      @[simp]
      theorem Surreal.leadingTerm_one :
      leadingTerm 1 = 1
      source
      @[simp]
      theorem Surreal.leadingTerm_neg (x : Surreal) :
      (-x).leadingTerm = -x.leadingTerm
      source
      @[simp]
      theorem Surreal.leadingTerm_mul (x y : Surreal) :
      (x * y).leadingTerm = x.leadingTerm * y.leadingTerm
      source
      @[simp]
      theorem Surreal.leadingTerm_inv (x : Surreal) :
      x⁻¹.leadingTerm = x.leadingTerm⁻¹
      source
      @[simp]
      theorem Surreal.leadingTerm_div (x y : Surreal) :
      (x / y).leadingTerm = x.leadingTerm / y.leadingTerm
      source
      @[simp]
      theorem Surreal.leadingTerm_wpow (x : Surreal) :
      (ω^ x).leadingTerm = ω^ x
      source
      @[simp]
      theorem Surreal.leadingTerm_eq_zero {x : Surreal} :
      x.leadingTerm = 0 ↔ x = 0
      source
      @[simp]
      theorem Surreal.leadingTerm_nonneg_iff {x : Surreal} :
      0 ≤ x.leadingTerm ↔ 0 ≤ x
      source
      @[simp]
      theorem Surreal.leadingTerm_nonpos_iff {x : Surreal} :
      x.leadingTerm ≤ 0 ↔ x ≤ 0
      source
      @[simp]
      theorem Surreal.leadingTerm_pos_iff {x : Surreal} :
      0 < x.leadingTerm ↔ 0 < x
      source
      @[simp]
      theorem Surreal.leadingTerm_neg_iff {x : Surreal} :
      x.leadingTerm < 0 ↔ x < 0
      source
      theorem Surreal.mk_lt_mk_sub_leadingTerm {x : Surreal} (hx : x ≠ 0) :
      ArchimedeanClass.mk x < ArchimedeanClass.mk (x - x.leadingTerm)
      source
      @[simp]
      theorem Surreal.mk_leadingTerm (x : Surreal) :
      ArchimedeanClass.mk x.leadingTerm = ArchimedeanClass.mk x
      source
      theorem Surreal.leadingTerm_veq (x : Surreal) :
      x.leadingTerm =ᵥ x
      source
      @[simp]
      theorem Surreal.wlog_leadingTerm (x : Surreal) :
      x.leadingTerm.wlog = x.wlog
      source
      @[simp]
      theorem Surreal.leadingCoeff_leadingTerm (x : Surreal) :
      x.leadingTerm.leadingCoeff = x.leadingCoeff
      source
      @[simp]
      theorem Surreal.leadingTerm_leadingTerm (x : Surreal) :
      x.leadingTerm.leadingTerm = x.leadingTerm
      source
      theorem Surreal.leadingTerm_mono :
      Monotone leadingTerm
      source
      theorem Surreal.leadingTerm_eq {x y : Surreal} {r : ℝ} (hr : r ≠ 0) (hL : ∀ s < r, ↑s * ω^ y ≤ x) (hR : ∀ s > r, x ≤ ↑s * ω^ y) :
      x.leadingTerm = ↑r * ω^ y
      source
      theorem Surreal.leadingTerm_add_eq_left {x y : Surreal} (h : y <ᵥ x) :
      (x + y).leadingTerm = x.leadingTerm
      source
      theorem Surreal.leadingTerm_add_eq_right {x y : Surreal} (h : y <ᵥ x) :
      (y + x).leadingTerm = x.leadingTerm
      source
      theorem Surreal.leadingTerm_sub_eq_left {x y : Surreal} :
      y <ᵥ x → (x - y).leadingTerm = x.leadingTerm
      source
      theorem Surreal.leadingTerm_sub_eq_right {x y : Surreal} :
      y <ᵥ x → (y - x).leadingTerm = -x.leadingTerm