Surreal exponentiation #

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

Todo #

Prove that ω^ x matches ordinal exponentiation for ordinal x.
Define commensurate surreals and prove properties relating to ω^ x.
Define the normal form of a surreal number.

source

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

source

class Wpow (α : Type u_1) :

Type u_1

A typeclass for the the ω^ notation.

wpow : α → α

Instances

source

def «termω^_» :

Lean.ParserDescr

Equations

«termω^_» = Lean.ParserDescr.node `«termω^_» 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ω^ ") (Lean.ParserDescr.cat `term 75))

Instances For

source

instance IGame.instWpow :

Wpow IGame

Equations

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

source

theorem IGame.wpow_def (x : IGame) :

ω^ x = {insert 0 (Set.image2 (fun (r : Dyadic) (y : IGame) => ↑r * ω^ y) (Set.Ioi 0) x.leftMoves) | Set.image2 (fun (r : Dyadic) (y : IGame) => ↑r * ω^ y) (Set.Ioi 0) x.rightMoves}ᴵ

source

theorem IGame.leftMoves_wpow (x : IGame) :

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

source

theorem IGame.rightMoves_wpow (x : IGame) :

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

source

@[simp]

theorem IGame.forall_leftMoves_wpow {x : IGame} {P : IGame → Prop} :

(∀ y ∈ (ω^ x).leftMoves, P y) ↔ P 0 ∧ ∀ (r : Dyadic), 0 < r → ∀ y ∈ x.leftMoves, P (↑r * ω^ y)

source

@[simp]

theorem IGame.forall_rightMoves_wpow {x : IGame} {P : IGame → Prop} :

(∀ y ∈ (ω^ x).rightMoves, P y) ↔ ∀ (r : Dyadic), 0 < r → ∀ y ∈ x.rightMoves, P (↑r * ω^ y)

source

@[simp]

theorem IGame.exists_leftMoves_wpow {x : IGame} {P : IGame → Prop} :

(∃ y ∈ (ω^ x).leftMoves, P y) ↔ P 0 ∨ ∃ (r : Dyadic), 0 < r ∧ ∃ y ∈ x.leftMoves, P (↑r * ω^ y)

source

@[simp]

theorem IGame.exists_rightMoves_wpow {x : IGame} {P : IGame → Prop} :

(∃ y ∈ (ω^ x).rightMoves, P y) ↔ ∃ (r : Dyadic), 0 < r ∧ ∃ y ∈ x.rightMoves, P (↑r * ω^ y)

source

@[simp]

theorem IGame.zero_mem_leftMoves_wpow (x : IGame) :

0 ∈ (ω^ x).leftMoves

source

theorem IGame.mul_wpow_mem_leftMoves_wpow {x y : IGame} {r : Dyadic} (hr : 0 ≤ r) (hy : y ∈ x.leftMoves) :

↑r * ω^ y ∈ (ω^ x).leftMoves

source

theorem IGame.mul_wpow_mem_rightMoves_wpow {x y : IGame} {r : Dyadic} (hr : 0 < r) (hy : y ∈ x.rightMoves) :

↑r * ω^ y ∈ (ω^ x).rightMoves

source

theorem IGame.natCast_mul_wpow_mem_leftMoves_wpow {x y : IGame} (n : ℕ) (hy : y ∈ x.leftMoves) :

↑n * ω^ y ∈ (ω^ x).leftMoves

source

theorem IGame.natCast_mul_wpow_mem_rightMoves_wpow {x y : IGame} {n : ℕ} (hn : 0 < n) (hy : y ∈ x.rightMoves) :

↑n * ω^ y ∈ (ω^ x).rightMoves

source

theorem IGame.wpow_mem_leftMoves_wpow {x y : IGame} (hy : y ∈ x.leftMoves) :

ω^ y ∈ (ω^ x).leftMoves

source

theorem IGame.wpow_mem_rightMoves_wpow {x y : IGame} (hy : y ∈ x.rightMoves) :

ω^ y ∈ (ω^ x).rightMoves

source

theorem IGame.zero_lf_wpow (x : IGame) :

¬ω^ x ≤ 0

source

@[simp]

theorem IGame.wpow_zero :

ω^ 0 = 1

source

@[irreducible]

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

(ω^ x).Numeric

source

@[simp]

theorem IGame.Numeric.wpow_pos (x : IGame) [x.Numeric] :

0 < ω^ x

source

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

↑r * ω^ x < ω^ y

source

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.

source

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

ω^ x < ↑r * ω^ y

source

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.

source

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

source

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.

source

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

source

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.

source

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

source

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.

source

@[simp]

theorem IGame.Numeric.wpow_lt_wpow {x y : IGame} [x.Numeric] [y.Numeric] :

ω^ x < ω^ y ↔ x < y

source

@[simp]

theorem IGame.Numeric.wpow_le_wpow {x y : IGame} [x.Numeric] [y.Numeric] :

ω^ x ≤ ω^ y ↔ x ≤ y

source

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

ω^ x ≈ ω^ y

source

@[irreducible]

theorem IGame.Numeric.wpow_add_equiv (x y : IGame) [x.Numeric] [y.Numeric] :

ω^ (x + y) ≈ ω^ x * ω^ y

source

theorem IGame.Numeric.wpow_neg_equiv (x : IGame) [x.Numeric] :

ω^ -x ≈ (ω^ x)⁻¹

source

theorem IGame.Numeric.wpow_sub_equiv (x y : IGame) [x.Numeric] [y.Numeric] :

ω^ (x - y) ≈ ω^ x / ω^ y

source

instance Surreal.instWpow :

Wpow Surreal

Equations

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

source

@[simp]

theorem Surreal.mk_wpow (x : IGame) [x.Numeric] :

mk (ω^ x) = ω^ mk x

source

@[simp]

theorem Surreal.wpow_zero :

ω^ 0 = 1

source

@[simp]

theorem Surreal.wpow_pos (x : Surreal) :

0 < ω^ x

source

theorem Surreal.strictMono_wpow :

StrictMono fun (x : Surreal) => ω^ x

source

@[simp]

theorem Surreal.wpow_lt_wpow {x y : Surreal} :

ω^ x < ω^ y ↔ x < y

source

@[simp]

theorem Surreal.wpow_le_wpow {x y : Surreal} :

ω^ x ≤ ω^ y ↔ x ≤ y

source

@[simp]

theorem Surreal.wpow_inj {x y : Surreal} :

ω^ x = ω^ y ↔ x = y

source

@[simp]

theorem Surreal.wpow_add (x y : Surreal) :

ω^ (x + y) = ω^ x * ω^ y

source

@[simp]

theorem Surreal.wpow_neg (x : Surreal) :

ω^ -x = (ω^ x)⁻¹

source

@[simp]

theorem Surreal.wpow_sub (x y : Surreal) :

ω^ (x - y) = ω^ x / ω^ y

Documentation

CombinatorialGames.Surreal.Pow

Surreal exponentiation #

Todo #