Documentation

CombinatorialGames.Surreal.Pow

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_dyadic {r : Dyadic'} (h : r ≠ 0) :

mk ↑↑r = 0

@[simp]

theorem ArchimedeanClass.mk_realCast {r : ℝ} (h : r ≠ 0) :

mk ↑r = 0

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 IGame.instWpow :

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) :

@[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

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

@[irreducible]

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

@[irreducible]

theorem IGame.toIGame_wpow_equiv (x : NatOrdinal) :

NatOrdinal.toIGame (ω^ x) ≈ ω^ NatOrdinal.toIGame x

ω-pow on `Surreal` #

instance Surreal.instWpow :

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_ne_zero (x : Surreal) :

@[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 #

theorem Surreal.mk_wpow_strictAnti :

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

@[simp]

theorem Surreal.mk_wpow_lt_mk_wpow_iff {x y : Surreal} :

ArchimedeanClass.mk (ω^ x) < ArchimedeanClass.mk (ω^ y) ↔ y < x

@[simp]

theorem Surreal.mk_wpow_le_mk_wpow_iff {x y : Surreal} :

ArchimedeanClass.mk (ω^ x) ≤ ArchimedeanClass.mk (ω^ y) ↔ y ≤ x

@[simp]

theorem Surreal.mk_wpow_inj {x y : Surreal} :

ArchimedeanClass.mk (ω^ x) = ArchimedeanClass.mk (ω^ 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_mk_wpow_eq {x : Surreal} (h : x ≠ 0) :

∃ (y : Surreal), ArchimedeanClass.mk (ω^ y) = ArchimedeanClass.mk x

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

ω-logarithm #

def Surreal.wlog (x : 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 ⋯

Instances For

def IGame.wlog (x : IGame) :

Returns an arbitrary representative for Surreal.wlog.

Equations

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

Instances For

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

@[simp]

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

mk x.wlog = (mk x).wlog

@[simp]

theorem Surreal.wlog_zero :

wlog 0 = 0

@[simp]

theorem Surreal.mk_wpow_wlog {x : Surreal} (h : x ≠ 0) :

ArchimedeanClass.mk (ω^ x.wlog) = ArchimedeanClass.mk x

theorem Surreal.wlog_eq_of_mk_eq_mk {x y : Surreal} (h : ArchimedeanClass.mk (ω^ y) = ArchimedeanClass.mk x) :

x.wlog = y

@[simp]

theorem Surreal.wlog_eq_iff {x y : Surreal} (h : x ≠ 0) :

x.wlog = y ↔ ArchimedeanClass.mk (ω^ y) = ArchimedeanClass.mk x

@[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)

@[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

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