Surreal exponentiation

We define here the ω-map on games and on surreal numbers, representing exponentials with base ω.

Among other things, we prove that every non-zero surreal number is commensurate to some unique ω^ x. We express this using ArchimedeanClass. There's two important things to note:

• The definition of ArchimedeanClass involves absolute values, such that e.g. -ω is commensurate to ω.
• The order in ArchimedeanClass is defined so that the equivalence class of 0 is the largest equivalence class, rather than the smallest.

Todo

• Define the normal form of a surreal number.

For Mathlib

theorem Set.image2_eq_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (s : Set α) (t : Set β) : image2 f s t = range fun (x : ↑s × ↑t) => f ↑x.1 ↑x.2

theorem ArchimedeanClass.mk_le_mk_iff_dyadic {x y : Surreal} : mk x ≤ mk y ↔ ∃ (q : Dyadic), 0 < q ∧ ↑↑q * |y| ≤ |x|

ω-map on IGame

@[instance_reducible]

noncomputable instance IGame.instWpow : Wpow IGame

Equations

• IGame.instWpow = { wpow := IGame.wpow✝ }

theorem IGame.wpow_def (x : IGame) : ω^ x = !{insert 0 (Set.image2 (fun (r : Dyadic) (y : IGame) => ↑r * ω^ y) (Set.Ioi 0) (moves left x)) | Set.image2 (fun (r : Dyadic) (y : IGame) => ↑r * ω^ y) (Set.Ioi 0) (moves right x)}

theorem IGame.leftMoves_wpow (x : IGame) : moves left (ω^ x) = insert 0 (Set.image2 (fun (r : Dyadic) (y : IGame) => ↑r * ω^ y) (Set.Ioi 0) (moves left x))

theorem IGame.rightMoves_wpow (x : IGame) : moves right (ω^ x) = Set.image2 (fun (r : Dyadic) (y : IGame) => ↑r * ω^ y) (Set.Ioi 0) (moves right x)

@[simp]

theorem IGame.forall_leftMoves_wpow {x : IGame} {P : IGame → Prop} : (∀ y ∈ moves left (ω^ x), P y) ↔ P 0 ∧ ∀ (r : Dyadic), 0 < r → ∀ y ∈ moves left x, P (↑r * ω^ y)

@[simp]

theorem IGame.forall_rightMoves_wpow {x : IGame} {P : IGame → Prop} : (∀ y ∈ moves right (ω^ x), P y) ↔ ∀ (r : Dyadic), 0 < r → ∀ y ∈ moves right x, P (↑r * ω^ y)

@[simp]

theorem IGame.exists_leftMoves_wpow {x : IGame} {P : IGame → Prop} : (∃ y ∈ moves left (ω^ x), P y) ↔ P 0 ∨ ∃ (r : Dyadic), 0 < r ∧ ∃ y ∈ moves left x, P (↑r * ω^ y)

@[simp]

theorem IGame.exists_rightMoves_wpow {x : IGame} {P : IGame → Prop} : (∃ y ∈ moves right (ω^ x), P y) ↔ ∃ (r : Dyadic), 0 < r ∧ ∃ y ∈ moves right x, P (↑r * ω^ y)

@[simp]

theorem IGame.zero_mem_leftMoves_wpow (x : IGame) : 0 ∈ moves left (ω^ x)

theorem IGame.mul_wpow_mem_leftMoves_wpow {x y : IGame} {r : Dyadic} (hr : 0 ≤ r) (hy : y ∈ moves left x) : ↑r * ω^ y ∈ moves left (ω^ x)

theorem IGame.mul_wpow_mem_rightMoves_wpow {x y : IGame} {r : Dyadic} (hr : 0 < r) (hy : y ∈ moves right x) : ↑r * ω^ y ∈ moves right (ω^ x)

theorem IGame.natCast_mul_wpow_mem_leftMoves_wpow {x y : IGame} (n : ℕ) (hy : y ∈ moves left x) : ↑n * ω^ y ∈ moves left (ω^ x)

theorem IGame.natCast_mul_wpow_mem_rightMoves_wpow {x y : IGame} {n : ℕ} (hn : 0 < n) (hy : y ∈ moves right x) : ↑n * ω^ y ∈ moves right (ω^ x)

theorem IGame.wpow_mem_leftMoves_wpow {x y : IGame} (hy : y ∈ moves left x) : ω^ y ∈ moves left (ω^ x)

theorem IGame.wpow_mem_rightMoves_wpow {x y : IGame} (hy : y ∈ moves right x) : ω^ y ∈ moves right (ω^ x)

theorem IGame.zero_lf_wpow (x : IGame) : ¬ω^ x ≤ 0

@[simp]

theorem IGame.wpow_zero : ω^ 0 = 1

@[irreducible]

instance IGame.Numeric.wpow (x : IGame) [x.Numeric] : (ω^ x).Numeric

@[simp]

theorem IGame.Numeric.wpow_pos (x : IGame) [x.Numeric] : 0 < ω^ x

@[simp]

theorem IGame.Numeric.wpow_nonneg (x : IGame) [x.Numeric] : 0 ≤ ω^ x

theorem IGame.Numeric.mul_wpow_lt_wpow {x y : IGame} [x.Numeric] [y.Numeric] (r : ℝ) (h : x < y) : ↑r * ω^ x < ω^ y

theorem IGame.Numeric.mul_wpow_lt_wpow' {x y : IGame} [x.Numeric] [y.Numeric] (r : Dyadic) (h : x < y) : ↑r * ω^ x < ω^ y

A version of mul_wpow_lt_wpow stated using dyadic rationals.

theorem IGame.Numeric.wpow_lt_mul_wpow {x y : IGame} [x.Numeric] [y.Numeric] {r : ℝ} (hr : 0 < r) (h : x < y) : ω^ x < ↑r * ω^ y

theorem IGame.Numeric.wpow_lt_mul_wpow' {x y : IGame} [x.Numeric] [y.Numeric] {r : Dyadic} (hr : 0 < r) (h : x < y) : ω^ x < ↑r * ω^ y

A version of wpow_lt_mul_wpow stated using dyadic rationals.

theorem IGame.Numeric.mul_wpow_lt_mul_wpow {x y : IGame} [x.Numeric] [y.Numeric] (r : ℝ) {s : ℝ} (hs : 0 < s) (h : x < y) : ↑r * ω^ x < ↑s * ω^ y

theorem IGame.Numeric.mul_wpow_lt_mul_wpow' {x y : IGame} [x.Numeric] [y.Numeric] (r : Dyadic) {s : Dyadic} (hs : 0 < s) (h : x < y) : ↑r * ω^ x < ↑s * ω^ y

A version of mul_wpow_lt_mul_wpow stated using dyadic rationals.

theorem IGame.Numeric.mul_wpow_add_mul_wpow_lt_mul_wpow {x y z : IGame} [x.Numeric] [y.Numeric] [z.Numeric] (r s : ℝ) {t : ℝ} (ht : 0 < t) (hx : x < z) (hy : y < z) : ↑r * ω^ x + ↑s * ω^ y < ↑t * ω^ z

theorem IGame.Numeric.mul_wpow_add_mul_wpow_lt_mul_wpow' {x y z : IGame} [x.Numeric] [y.Numeric] [z.Numeric] (r s : Dyadic) {t : Dyadic} (ht : 0 < t) (hx : x < z) (hy : y < z) : ↑r * ω^ x + ↑s * ω^ y < ↑t * ω^ z

A version of mul_wpow_add_mul_wpow_lt_mul_wpow stated using dyadic rationals.

theorem IGame.Numeric.mul_wpow_lt_mul_wpow_add_mul_wpow {x y z : IGame} [x.Numeric] [y.Numeric] [z.Numeric] (r : ℝ) {s t : ℝ} (hs : 0 < s) (ht : 0 < t) (hx : x < y) (hy : x < z) : ↑r * ω^ x < ↑s * ω^ y + ↑t * ω^ z

theorem IGame.Numeric.mul_wpow_lt_mul_wpow_add_mul_wpow' {x y z : IGame} [x.Numeric] [y.Numeric] [z.Numeric] (r : Dyadic) {s t : Dyadic} (hs : 0 < s) (ht : 0 < t) (hx : x < y) (hy : x < z) : ↑r * ω^ x < ↑s * ω^ y + ↑t * ω^ z

A version of mul_wpow_lt_mul_wpow_add_mul_wpow stated using dyadic rationals.

@[simp]

theorem IGame.Numeric.wpow_lt_wpow {x y : IGame} [x.Numeric] [y.Numeric] : ω^ x < ω^ y ↔ x < y

@[simp]

theorem IGame.Numeric.wpow_le_wpow {x y : IGame} [x.Numeric] [y.Numeric] : ω^ x ≤ ω^ y ↔ x ≤ y

theorem IGame.Numeric.wpow_congr {x y : IGame} [x.Numeric] [y.Numeric] (h : x ≈ y) : ω^ x ≈ ω^ y

theorem IGame.Numeric.wpow_add_equiv (x y : IGame) [x.Numeric] [y.Numeric] : ω^ (x + y) ≈ ω^ x * ω^ y

theorem IGame.Numeric.wpow_neg_equiv (x : IGame) [x.Numeric] : ω^ -x ≈ (ω^ x)⁻¹

theorem IGame.Numeric.wpow_sub_equiv (x y : IGame) [x.Numeric] [y.Numeric] : ω^ (x - y) ≈ ω^ x / ω^ y

theorem IGame.toIGame_wpow_equiv (x : NatOrdinal) : NatOrdinal.toIGame (ω^ x) ≈ ω^ NatOrdinal.toIGame x

ω-pow on Surreal

@[instance_reducible]

noncomputable instance Surreal.instWpow : Wpow Surreal

Equations

• Surreal.instWpow = { wpow := Quotient.lift (fun (x : Subtype IGame.Numeric) => Surreal.mk (ω^ ↑x)) Surreal.instWpow._proof_2 }

@[simp]

theorem Surreal.mk_wpow (x : IGame) [x.Numeric] : mk (ω^ x) = ω^ mk x

@[simp]

theorem Surreal.wpow_zero : ω^ 0 = 1

@[simp]

theorem Surreal.wpow_pos (x : Surreal) : 0 < ω^ x

@[simp]

theorem Surreal.wpow_nonneg (x : Surreal) : 0 ≤ ω^ x

@[simp]

theorem Surreal.wpow_ne_zero (x : Surreal) : ω^ x ≠ 0

@[simp]

theorem Surreal.wpow_abs (x : Surreal) : |ω^ x| = ω^ x

theorem Surreal.strictMono_wpow : StrictMono fun (x : Surreal) => ω^ x

@[simp]

theorem Surreal.wpow_lt_wpow {x y : Surreal} : ω^ x < ω^ y ↔ x < y

@[simp]

theorem Surreal.wpow_le_wpow {x y : Surreal} : ω^ x ≤ ω^ y ↔ x ≤ y

@[simp]

theorem Surreal.wpow_inj {x y : Surreal} : ω^ x = ω^ y ↔ x = y

@[simp]

theorem Surreal.wpow_add (x y : Surreal) : ω^ (x + y) = ω^ x * ω^ y

@[simp]

theorem Surreal.wpow_neg (x : Surreal) : ω^ -x = (ω^ x)⁻¹

@[simp]

theorem Surreal.wpow_sub (x y : Surreal) : ω^ (x - y) = ω^ x / ω^ y

theorem Surreal.mul_wpow_lt_wpow {x y : Surreal} (r : ℝ) (h : x < y) : ↑r * ω^ x < ω^ y

theorem Surreal.wpow_lt_mul_wpow {x y : Surreal} {r : ℝ} (hr : 0 < r) (h : x < y) : ω^ x < ↑r * ω^ y

theorem Surreal.mul_wpow_lt_mul_wpow {x y : Surreal} (r : ℝ) {s : ℝ} (hs : 0 < s) (h : x < y) : ↑r * ω^ x < ↑s * ω^ y

Archimedean classes

@[simp]

theorem Surreal.mk_realCast {r : ℝ} (hr : r ≠ 0) : ArchimedeanClass.mk ↑r = 0

@[instance_reducible]

noncomputable instance Surreal.instValuativeRel : ValuativeRel Surreal

We define a ValuativeRel instance on Surreal which is compatible with ArchimedeanClass.addValuation. In particular, you can write x =ᵥ y to mean that x is commensurate with y.

Equations

• Surreal.instValuativeRel = ValuativeRel.ofValuation (ArchimedeanClass.addValuation Surreal)

instance Surreal.instCompatibleMultiplicativeOrderDualArchimedeanClassAddValuation : Valuation.Compatible (ArchimedeanClass.addValuation Surreal)

theorem Surreal.vle_def {x y : Surreal} : x ≤ᵥ y ↔ ArchimedeanClass.mk y ≤ ArchimedeanClass.mk x

theorem Surreal.vlt_def {x y : Surreal} : x <ᵥ y ↔ ArchimedeanClass.mk y < ArchimedeanClass.mk x

theorem Surreal.veq_def {x y : Surreal} : x =ᵥ y ↔ ArchimedeanClass.mk x = ArchimedeanClass.mk y

@[simp]

theorem Surreal.neg_veq {x y : Surreal} : -x =ᵥ y ↔ x =ᵥ y

@[simp]

theorem Surreal.veq_neg {x y : Surreal} : x =ᵥ -y ↔ x =ᵥ y

@[simp]

theorem Surreal.vle_neg {x y : Surreal} : x ≤ᵥ -y ↔ x ≤ᵥ y

@[simp]

theorem Surreal.neg_vle {x y : Surreal} : -x ≤ᵥ y ↔ x ≤ᵥ y

@[simp]

theorem Surreal.vlt_neg {x y : Surreal} : x <ᵥ -y ↔ x <ᵥ y

@[simp]

theorem Surreal.neg_vlt {x y : Surreal} : -x <ᵥ y ↔ x <ᵥ y

theorem Surreal.archimedeanClassMk_wpow_strictAnti : StrictAnti fun (x : Surreal) => ArchimedeanClass.mk (ω^ x)

@[simp]

theorem Surreal.wpow_vlt_wpow_iff {x y : Surreal} : ω^ x <ᵥ ω^ y ↔ x < y

@[simp]

theorem Surreal.wpow_vle_wpow_iff {x y : Surreal} : ω^ x ≤ᵥ ω^ y ↔ x ≤ y

@[simp]

theorem Surreal.wpow_veq_wpow_iff {x y : Surreal} : ω^ x =ᵥ ω^ y ↔ x = y

ω^ x and ω^ y are commensurate iff x = y.

theorem Surreal.instNumericValIGameMemSetInterMovesLeftIoiOfNat (x : IGame) [x.Numeric] (y : ↑(IGame.moves Player.left x ∩ Set.Ioi 0)) : (↑y).Numeric

theorem Surreal.exists_wpow_veq {x : Surreal} (h : x ≠ 0) : ∃ (y : Surreal), ω^ y =ᵥ x

Every non-zero surreal is commensurate to some ω^ x.

ω-logarithm

noncomputable def Surreal.wlog (x : Surreal) : Surreal

The ω-logarithm of a positive surreal x is the unique surreal y such that x is commensurate with ω^ y.

As with Real.log, we set junk values wlog 0 = 0 and wlog (-x) = wlog x.

Equations

• x.wlog = if h : x = 0 then 0 else Classical.choose ⋯

noncomputable def IGame.wlog (x : IGame) : IGame

Returns an arbitrary representative for Surreal.wlog.

Equations

• x.wlog = if x_1 : x.Numeric then (Surreal.mk x).wlog.out else 0

instance IGame.Numeric.wlog (x : IGame) : x.wlog.Numeric

@[simp]

theorem Surreal.mk_wlog (x : IGame) [h : x.Numeric] : mk x.wlog = (mk x).wlog

@[simp]

theorem Surreal.wlog_zero : wlog 0 = 0

theorem Surreal.wpow_wlog_veq {x : Surreal} (h : x ≠ 0) : ω^ x.wlog =ᵥ x

@[simp]

theorem Surreal.archimedeanClassMk_wpow_wlog {x : Surreal} (h : x ≠ 0) : ArchimedeanClass.mk (ω^ x.wlog) = ArchimedeanClass.mk x

theorem Surreal.wlog_eq_of_wpow_veq {x y : Surreal} (h : ω^ y =ᵥ x) : x.wlog = y

@[simp]

theorem Surreal.wlog_eq_iff {x y : Surreal} (h : x ≠ 0) : x.wlog = y ↔ ω^ y =ᵥ x

theorem Surreal.wlog_congr {x y : Surreal} (h : x =ᵥ y) : x.wlog = y.wlog

@[simp]

theorem Surreal.wlog_wpow (x : Surreal) : (ω^ x).wlog = x

@[simp]

theorem Surreal.wlog_neg (x : Surreal) : (-x).wlog = x.wlog

@[simp]

theorem Surreal.wlog_abs (x : Surreal) : |x|.wlog = x.wlog

theorem Surreal.wlog_surjective : Function.Surjective wlog

theorem Surreal.wlog_monotoneOn : MonotoneOn wlog (Set.Ioi 0)

theorem Surreal.wlog_antitoneOn : AntitoneOn wlog (Set.Iio 0)

theorem Surreal.wlog_add_eq_left {x y : Surreal} (h : y <ᵥ x) : (x + y).wlog = x.wlog

theorem Surreal.wlog_add_eq_right {x y : Surreal} (h : y <ᵥ x) : (y + x).wlog = x.wlog

theorem Surreal.wlog_sub_eq_left {x y : Surreal} : y <ᵥ x → (x - y).wlog = x.wlog

theorem Surreal.wlog_sub_eq_right {x y : Surreal} : y <ᵥ x → (y - x).wlog = x.wlog

theorem Surreal.wlog_le_wlog_iff {x y : Surreal} (hx : x ≠ 0) (hy : y ≠ 0) : x.wlog ≤ y.wlog ↔ x ≤ᵥ y

theorem Surreal.wlog_le_wlog_of_vle {x y : Surreal} (hx : x ≠ 0) (h : x ≤ᵥ y) : x.wlog ≤ y.wlog

theorem Surreal.wlog_lt_wlog_iff {x y : Surreal} (hx : x ≠ 0) (hy : y ≠ 0) : x.wlog < y.wlog ↔ x <ᵥ y

theorem Surreal.wlog_lt_wlog_of_vlt {x y : Surreal} (hx : x ≠ 0) (h : x <ᵥ y) : x.wlog < y.wlog

@[simp]

theorem Surreal.wlog_mul {x y : Surreal} (hx : x ≠ 0) (hy : y ≠ 0) : (x * y).wlog = x.wlog + y.wlog

@[simp]

theorem Surreal.wlog_realCast (r : ℝ) : (↑r).wlog = 0

@[simp]

theorem Surreal.wlog_ratCast (q : ℚ) : (↑q).wlog = 0

@[simp]

theorem Surreal.wlog_intCast (n : ℤ) : (↑n).wlog = 0

@[simp]

theorem Surreal.wlog_natCast (n : ℕ) : (↑n).wlog = 0

@[simp]

theorem Surreal.wlog_one : wlog 1 = 0

@[simp]

theorem Surreal.wlog_inv (x : Surreal) : x⁻¹.wlog = -x.wlog

@[simp]

theorem Surreal.wlog_pow (x : Surreal) (n : ℕ) : (x ^ n).wlog = ↑n * x.wlog

@[simp]

theorem Surreal.wlog_zpow (x : Surreal) (n : ℤ) : (x ^ n).wlog = ↑n * x.wlog

@[simp]

theorem Surreal.archimedeanClassMk_div_wpow_wlog (x : Surreal) : ArchimedeanClass.mk (x / ω^ x.wlog) = ArchimedeanClass.mk x - ArchimedeanClass.mk x

theorem Surreal.mk_div_wpow_wlog_of_ne_zero {x : Surreal} (hx : x ≠ 0) : ArchimedeanClass.mk (x / ω^ x.wlog) = 0

theorem Surreal.numeric_of_forall_mk_ne_mk {x : IGame} [x.Numeric] (h : 0 < x) (Hl : ∀ (y : IGame) (hy : y ∈ IGame.moves Player.left x), 0 < y → ArchimedeanClass.mk (mk y) ≠ ArchimedeanClass.mk (mk x)) (Hr : ∀ (y : IGame) (hy : y ∈ IGame.moves Player.right x), ArchimedeanClass.mk (mk y) ≠ ArchimedeanClass.mk (mk x)) : !{IGame.wlog '' {y : IGame | y ∈ IGame.moves Player.left x ∧ 0 < y} | IGame.wlog '' IGame.moves Player.right x}.Numeric

theorem Surreal.wpow_equiv_of_forall_mk_ne_mk {x : IGame} [x.Numeric] (h : 0 < x) (Hl : ∀ (y : IGame) (hy : y ∈ IGame.moves Player.left x), 0 < y → ArchimedeanClass.mk (mk y) ≠ ArchimedeanClass.mk (mk x)) (Hr : ∀ (y : IGame) (hy : y ∈ IGame.moves Player.right x), ArchimedeanClass.mk (mk y) ≠ ArchimedeanClass.mk (mk x)) : ω^ !{IGame.wlog '' {y : IGame | y ∈ IGame.moves Player.left x ∧ 0 < y} | IGame.wlog '' IGame.moves Player.right x} ≈ x

theorem Surreal.mem_range_wpow_of_forall_mk_ne_mk {x : IGame} [x.Numeric] (h : 0 < x) (Hl : ∀ (y : IGame) (hy : y ∈ IGame.moves Player.left x), 0 < y → ArchimedeanClass.mk (mk y) ≠ ArchimedeanClass.mk (mk x)) (Hr : ∀ (y : IGame) (hy : y ∈ IGame.moves Player.right x), ArchimedeanClass.mk (mk y) ≠ ArchimedeanClass.mk (mk x)) : mk x ∈ Set.range fun (x : Surreal) => ω^ x

A game not commensurate with its positive options is a power of ω.

@[simp]

theorem Surreal.toSurreal_wpow (x : NatOrdinal) : NatOrdinal.toSurreal (ω^ x) = ω^ NatOrdinal.toSurreal x