mathlib3 documentation

set_theory.surreal.basic

Surreal numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The basic theory of surreal numbers, built on top of the theory of combinatorial (pre-)games.

A pregame is numeric if all the Left options are strictly smaller than all the Right options, and all those options are themselves numeric. In terms of combinatorial games, the numeric games have "frozen"; you can only make your position worse by playing, and Left is some definite "number" of moves ahead (or behind) Right.

A surreal number is an equivalence class of numeric pregames.

In fact, the surreals form a complete ordered field, containing a copy of the reals (and much else besides!) but we do not yet have a complete development.

Order properties #

Surreal numbers inherit the relations ≤ and < from games (surreal.has_le and surreal.has_lt), and these relations satisfy the axioms of a partial order.

Algebraic operations #

We show that the surreals form a linear ordered commutative group.

One can also map all the ordinals into the surreals!

Multiplication of surreal numbers #

The proof that multiplication lifts to surreal numbers is surprisingly difficult and is currently missing in the library. A sample proof can be found in Theorem 3.8 in the second reference below. The difficulty lies in the length of the proof and the number of theorems that need to proven simultaneously. This will make for a fun and challenging project.

The branch surreal_mul contains some progress on this proof.

Todo #

Define the field structure on the surreals.

References #

def pgame.numeric :

A pre-game is numeric if everything in the L set is less than everything in the R set, and all the elements of L and R are also numeric.

Equations

(pgame.mk l r L R).numeric = ((∀ (i : l) (j : r), L i < R j) ∧ (∀ (i : l), (L i).numeric) ∧ ∀ (j : r), (R j).numeric)

theorem pgame.numeric_def {x : pgame} :

x.numeric ↔ (∀ (i : x.left_moves) (j : x.right_moves), x.move_left i < x.move_right j) ∧ (∀ (i : x.left_moves), (x.move_left i).numeric) ∧ ∀ (j : x.right_moves), (x.move_right j).numeric

theorem pgame.numeric.mk {x : pgame} (h₁ : ∀ (i : x.left_moves) (j : x.right_moves), x.move_left i < x.move_right j) (h₂ : ∀ (i : x.left_moves), (x.move_left i).numeric) (h₃ : ∀ (j : x.right_moves), (x.move_right j).numeric) :

theorem pgame.numeric.left_lt_right {x : pgame} (o : x.numeric) (i : x.left_moves) (j : x.right_moves) :

x.move_left i < x.move_right j

theorem pgame.numeric.move_left {x : pgame} (o : x.numeric) (i : x.left_moves) :

(x.move_left i).numeric

theorem pgame.numeric.move_right {x : pgame} (o : x.numeric) (j : x.right_moves) :

(x.move_right j).numeric

theorem pgame.numeric_rec {C : pgame → Prop} (H : ∀ (l r : Type u_1) (L : l → pgame) (R : r → pgame), (∀ (i : l) (j : r), L i < R j) → (∀ (i : l), (L i).numeric) → (∀ (i : r), (R i).numeric) → (∀ (i : l), C (L i)) → (∀ (i : r), C (R i)) → C (pgame.mk l r L R)) (x : pgame) :

x.numeric → C x

theorem pgame.relabelling.numeric_imp {x y : pgame} (r : x.relabelling y) (ox : x.numeric) :

theorem pgame.relabelling.numeric_congr {x y : pgame} (r : x.relabelling y) :

x.numeric ↔ y.numeric

Relabellings preserve being numeric.

theorem pgame.lf_asymm {x y : pgame} (ox : x.numeric) (oy : y.numeric) :

x.lf y → ¬y.lf x

theorem pgame.le_of_lf {x y : pgame} (h : x.lf y) (ox : x.numeric) (oy : y.numeric) :

x ≤ y

theorem pgame.lf.le {x y : pgame} (h : x.lf y) (ox : x.numeric) (oy : y.numeric) :

x ≤ y

Alias of pgame.le_of_lf.

theorem pgame.lt_of_lf {x y : pgame} (h : x.lf y) (ox : x.numeric) (oy : y.numeric) :

x < y

theorem pgame.lf.lt {x y : pgame} (h : x.lf y) (ox : x.numeric) (oy : y.numeric) :

x < y

Alias of pgame.lt_of_lf.

theorem pgame.lf_iff_lt {x y : pgame} (ox : x.numeric) (oy : y.numeric) :

x.lf y ↔ x < y

theorem pgame.le_iff_forall_lt {x y : pgame} (ox : x.numeric) (oy : y.numeric) :

x ≤ y ↔ (∀ (i : x.left_moves), x.move_left i < y) ∧ ∀ (j : y.right_moves), x < y.move_right j

Definition of x ≤ y on numeric pre-games, in terms of <

theorem pgame.lt_iff_exists_le {x y : pgame} (ox : x.numeric) (oy : y.numeric) :

x < y ↔ (∃ (i : y.left_moves), x ≤ y.move_left i) ∨ ∃ (j : x.right_moves), x.move_right j ≤ y

Definition of x < y on numeric pre-games, in terms of ≤

theorem pgame.lt_of_exists_le {x y : pgame} (ox : x.numeric) (oy : y.numeric) :

((∃ (i : y.left_moves), x ≤ y.move_left i) ∨ ∃ (j : x.right_moves), x.move_right j ≤ y) → x < y

theorem pgame.lt_def {x y : pgame} (ox : x.numeric) (oy : y.numeric) :

x < y ↔ (∃ (i : y.left_moves), (∀ (i' : x.left_moves), x.move_left i' < y.move_left i) ∧ ∀ (j : (y.move_left i).right_moves), x < (y.move_left i).move_right j) ∨ ∃ (j : x.right_moves), (∀ (i : (x.move_right j).left_moves), (x.move_right j).move_left i < y) ∧ ∀ (j' : y.right_moves), x.move_right j < y.move_right j'

The definition of x < y on numeric pre-games, in terms of < two moves later.

theorem pgame.not_fuzzy {x y : pgame} (ox : x.numeric) (oy : y.numeric) :

theorem pgame.lt_or_equiv_or_gt {x y : pgame} (ox : x.numeric) (oy : y.numeric) :

x < y ∨ x.equiv y ∨ y < x

theorem pgame.numeric_of_is_empty (x : pgame) [is_empty x.left_moves] [is_empty x.right_moves] :

theorem pgame.numeric_of_is_empty_left_moves (x : pgame) [is_empty x.left_moves] :

(∀ (j : x.right_moves), (x.move_right j).numeric) → x.numeric

theorem pgame.numeric_of_is_empty_right_moves (x : pgame) [is_empty x.right_moves] (H : ∀ (i : x.left_moves), (x.move_left i).numeric) :

theorem pgame.numeric_zero :

theorem pgame.numeric_one :

theorem pgame.numeric.neg {x : pgame} (o : x.numeric) :

theorem pgame.numeric.move_left_lt {x : pgame} (o : x.numeric) (i : x.left_moves) :

x.move_left i < x

theorem pgame.numeric.move_left_le {x : pgame} (o : x.numeric) (i : x.left_moves) :

x.move_left i ≤ x

theorem pgame.numeric.lt_move_right {x : pgame} (o : x.numeric) (j : x.right_moves) :

x < x.move_right j

theorem pgame.numeric.le_move_right {x : pgame} (o : x.numeric) (j : x.right_moves) :

x ≤ x.move_right j

theorem pgame.numeric.add {x y : pgame} (ox : x.numeric) (oy : y.numeric) :

(x + y).numeric

theorem pgame.numeric.sub {x y : pgame} (ox : x.numeric) (oy : y.numeric) :

(x - y).numeric

theorem pgame.numeric_nat (n : ℕ) :

Pre-games defined by natural numbers are numeric.

theorem pgame.numeric_to_pgame (o : ordinal) :

o.to_pgame.numeric

Ordinal games are numeric.

def surreal :

Type (u_1+1)

The type of surreal numbers. These are the numeric pre-games quotiented by the equivalence relation x ≈ y ↔ x ≤ y ∧ y ≤ x. In the quotient, the order becomes a total order.

Equations

surreal = quotient (subtype.setoid pgame.numeric)

Instances for surreal

def surreal.mk (x : pgame) (h : x.numeric) :

Construct a surreal number from a numeric pre-game.

Equations

surreal.mk x h = ⟦⟨x, h⟩⟧

@[protected, instance]

def surreal.has_zero :

has_zero surreal

Equations

surreal.has_zero = {zero := surreal.mk 0 pgame.numeric_zero}

@[protected, instance]

def surreal.has_one :

has_one surreal

Equations

surreal.has_one = {one := surreal.mk 1 pgame.numeric_one}

@[protected, instance]

def surreal.inhabited :

inhabited surreal

Equations

surreal.inhabited = {default := 0}

def surreal.lift {α : Sort u_1} (f : Π (x : pgame), x.numeric → α) (H : ∀ {x y : pgame} (hx : x.numeric) (hy : y.numeric), x.equiv y → f x hx = f y hy) :

Lift an equivalence-respecting function on pre-games to surreals.

Equations

surreal.lift f H = quotient.lift (λ (x : {x // x.numeric}), f x.val _) _

def surreal.lift₂ {α : Sort u_1} (f : Π (x : pgame) (y : pgame), x.numeric → y.numeric → α) (H : ∀ {x₁ : pgame} {y₁ : pgame} {x₂ : pgame} {y₂ : pgame} (ox₁ : x₁.numeric) (oy₁ : y₁.numeric) (ox₂ : x₂.numeric) (oy₂ : y₂.numeric), x₁.equiv x₂ → y₁.equiv y₂ → f x₁ y₁ ox₁ oy₁ = f x₂ y₂ ox₂ oy₂) :

surreal → surreal → α

Lift a binary equivalence-respecting function on pre-games to surreals.

Equations

surreal.lift₂ f H = surreal.lift (λ (x : pgame) (ox : x.numeric), surreal.lift (λ (y : pgame) (oy : y.numeric), f x y ox oy) _) _

@[protected, instance]

def surreal.has_le :

Equations

surreal.has_le = {le := surreal.lift₂ (λ (x y : pgame) (_x : x.numeric) (_x : y.numeric), x ≤ y) surreal.has_le._proof_1}

@[protected, instance]

def surreal.has_lt :

Equations

surreal.has_lt = {lt := surreal.lift₂ (λ (x y : pgame) (_x : x.numeric) (_x : y.numeric), x < y) surreal.has_lt._proof_1}

@[protected, instance]

def surreal.has_add :

has_add surreal

Addition on surreals is inherited from pre-game addition: the sum of x = {xL | xR} and y = {yL | yR} is {xL + y, x + yL | xR + y, x + yR}.

Equations

surreal.has_add = {add := surreal.lift₂ (λ (x y : pgame) (ox : x.numeric) (oy : y.numeric), ⟦⟨x + y, _⟩⟧) surreal.has_add._proof_1}

@[protected, instance]

def surreal.has_neg :

has_neg surreal

Negation for surreal numbers is inherited from pre-game negation: the negation of {L | R} is {-R | -L}.

Equations

surreal.has_neg = {neg := surreal.lift (λ (x : pgame) (ox : x.numeric), ⟦⟨-x, _⟩⟧) surreal.has_neg._proof_1}

@[protected, instance]

def surreal.ordered_add_comm_group :

ordered_add_comm_group surreal

Equations

surreal.ordered_add_comm_group = {add := has_add.add surreal.has_add, add_assoc := surreal.ordered_add_comm_group._proof_1, zero := 0, zero_add := surreal.ordered_add_comm_group._proof_2, add_zero := surreal.ordered_add_comm_group._proof_3, nsmul := add_comm_group.nsmul._default 0 has_add.add surreal.ordered_add_comm_group._proof_4 surreal.ordered_add_comm_group._proof_5, nsmul_zero' := surreal.ordered_add_comm_group._proof_6, nsmul_succ' := surreal.ordered_add_comm_group._proof_7, neg := has_neg.neg surreal.has_neg, sub := add_comm_group.sub._default has_add.add surreal.ordered_add_comm_group._proof_8 0 surreal.ordered_add_comm_group._proof_9 surreal.ordered_add_comm_group._proof_10 (add_comm_group.nsmul._default 0 has_add.add surreal.ordered_add_comm_group._proof_4 surreal.ordered_add_comm_group._proof_5) surreal.ordered_add_comm_group._proof_11 surreal.ordered_add_comm_group._proof_12 has_neg.neg, sub_eq_add_neg := surreal.ordered_add_comm_group._proof_13, zsmul := add_comm_group.zsmul._default has_add.add surreal.ordered_add_comm_group._proof_14 0 surreal.ordered_add_comm_group._proof_15 surreal.ordered_add_comm_group._proof_16 (add_comm_group.nsmul._default 0 has_add.add surreal.ordered_add_comm_group._proof_4 surreal.ordered_add_comm_group._proof_5) surreal.ordered_add_comm_group._proof_17 surreal.ordered_add_comm_group._proof_18 has_neg.neg, zsmul_zero' := surreal.ordered_add_comm_group._proof_19, zsmul_succ' := surreal.ordered_add_comm_group._proof_20, zsmul_neg' := surreal.ordered_add_comm_group._proof_21, add_left_neg := surreal.ordered_add_comm_group._proof_22, add_comm := surreal.ordered_add_comm_group._proof_23, le := has_le.le surreal.has_le, lt := has_lt.lt surreal.has_lt, le_refl := surreal.ordered_add_comm_group._proof_24, le_trans := surreal.ordered_add_comm_group._proof_25, lt_iff_le_not_le := surreal.ordered_add_comm_group._proof_26, le_antisymm := surreal.ordered_add_comm_group._proof_27, add_le_add_left := surreal.ordered_add_comm_group._proof_28}

@[protected, instance]

noncomputable def surreal.linear_ordered_add_comm_group :

linear_ordered_add_comm_group surreal

Equations

surreal.linear_ordered_add_comm_group = {add := ordered_add_comm_group.add surreal.ordered_add_comm_group, add_assoc := _, zero := ordered_add_comm_group.zero surreal.ordered_add_comm_group, zero_add := _, add_zero := _, nsmul := ordered_add_comm_group.nsmul surreal.ordered_add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := ordered_add_comm_group.neg surreal.ordered_add_comm_group, sub := ordered_add_comm_group.sub surreal.ordered_add_comm_group, sub_eq_add_neg := _, zsmul := ordered_add_comm_group.zsmul surreal.ordered_add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, le := ordered_add_comm_group.le surreal.ordered_add_comm_group, lt := ordered_add_comm_group.lt surreal.ordered_add_comm_group, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_total := surreal.linear_ordered_add_comm_group._proof_1, decidable_le := classical.dec_rel has_le.le, decidable_eq := linear_order.decidable_eq._default ordered_add_comm_group.le ordered_add_comm_group.lt ordered_add_comm_group.le_refl ordered_add_comm_group.le_trans ordered_add_comm_group.lt_iff_le_not_le ordered_add_comm_group.le_antisymm (classical.dec_rel has_le.le), decidable_lt := linear_order.decidable_lt._default ordered_add_comm_group.le ordered_add_comm_group.lt ordered_add_comm_group.le_refl ordered_add_comm_group.le_trans ordered_add_comm_group.lt_iff_le_not_le ordered_add_comm_group.le_antisymm (classical.dec_rel has_le.le), max := linear_order.max._default ordered_add_comm_group.le ordered_add_comm_group.lt ordered_add_comm_group.le_refl ordered_add_comm_group.le_trans ordered_add_comm_group.lt_iff_le_not_le ordered_add_comm_group.le_antisymm (classical.dec_rel has_le.le), max_def := surreal.linear_ordered_add_comm_group._proof_2, min := linear_order.min._default ordered_add_comm_group.le ordered_add_comm_group.lt ordered_add_comm_group.le_refl ordered_add_comm_group.le_trans ordered_add_comm_group.lt_iff_le_not_le ordered_add_comm_group.le_antisymm (classical.dec_rel has_le.le), min_def := surreal.linear_ordered_add_comm_group._proof_3}

@[protected, instance]

def surreal.add_monoid_with_one :

add_monoid_with_one surreal

Equations

surreal.add_monoid_with_one = add_monoid_with_one.unary

def surreal.to_game :

surreal →+o game

Casts a surreal number into a game.

Equations

surreal.to_game = {to_add_monoid_hom := {to_fun := surreal.lift (λ (x : pgame) (_x : x.numeric), ⟦x⟧) surreal.to_game._proof_1, map_zero' := surreal.to_game._proof_2, map_add' := surreal.to_game._proof_3}, monotone' := surreal.to_game._proof_4}

theorem surreal.zero_to_game :

⇑surreal.to_game 0 = 0

@[simp]

theorem surreal.one_to_game :

⇑surreal.to_game 1 = 1

@[simp]

theorem surreal.nat_to_game (n : ℕ) :

⇑surreal.to_game ↑n = ↑n

theorem surreal.upper_bound_numeric {ι : Type u} {f : ι → pgame} (H : ∀ (i : ι), (f i).numeric) :

(pgame.upper_bound f).numeric

theorem surreal.lower_bound_numeric {ι : Type u} {f : ι → pgame} (H : ∀ (i : ι), (f i).numeric) :

(pgame.lower_bound f).numeric

theorem surreal.bdd_above_of_small (s : set surreal) [small ↥s] :

A small set s of surreals is bounded above.

theorem surreal.bdd_below_of_small (s : set surreal) [small ↥s] :

A small set s of surreals is bounded below.

noncomputable def ordinal.to_surreal :

ordinal ↪o surreal

Converts an ordinal into the corresponding surreal.

Equations

ordinal.to_surreal = {to_embedding := {to_fun := λ (o : ordinal), surreal.mk o.to_pgame _, inj' := ordinal.to_surreal._proof_1}, map_rel_iff' := ordinal.to_pgame_le_iff}