Documentation

CombinatorialGames.SignExpansion.Basic

Sign expansions #

In this repository we define the type of Surreal numbers following Conway's theory of games. A popular alternative is to instead define the surreals as potentially infinite "expansions of signs", setting for instance + = 1, - = -1, +- = ½, etc.

This file defines the type SignExpansion and constructs its basic instances. We do not yet link it to the development of surreal numbers.

For Mathlib #

instance instZeroLEOneClassSignType_combinatorialGames :

ZeroLEOneClass SignType

theorem Set.preimage_neg {α : Type u_1} {ι : Type u_2} [InvolutiveNeg α] (f : ι → α) {s : Set α} :

f ⁻¹' (-s) = (-f) ⁻¹' s

@[simp]

theorem Pi.Lex.neg_apply {α : Type u_1} {β : Type u_2} [Neg β] (x : Lex (α → β)) (i : α) :

(-x) i = -x i

theorem Pi.Lex.neg_lt_neg {α : Type u_1} [LinearOrder α] {x y : Lex (α → SignType)} (h : x < y) :

-y < -x

@[simp]

theorem Pi.Lex.neg_lt_neg_iff {α : Type u_1} [LinearOrder α] {x y : Lex (α → SignType)} :

-x < -y ↔ y < x

@[simp]

theorem Pi.Lex.neg_le_neg_iff {α : Type u_1} [LinearOrder α] [WellFoundedLT α] {x y : Lex (α → SignType)} :

-x ≤ -y ↔ y ≤ x

theorem Pi.Lex.neg_lt_iff {α : Type u_1} [LinearOrder α] {x y : Lex (α → SignType)} :

-x < y ↔ -y < x

theorem Pi.Lex.lt_neg_iff {α : Type u_1} [LinearOrder α] {x y : Lex (α → SignType)} :

x < -y ↔ y < -x

theorem Pi.Lex.neg_le_iff {α : Type u_1} [LinearOrder α] [WellFoundedLT α] {x y : Lex (α → SignType)} :

-x ≤ y ↔ -y ≤ x

theorem Pi.Lex.le_neg_iff {α : Type u_1} [LinearOrder α] [WellFoundedLT α] {x y : Lex (α → SignType)} :

x ≤ -y ↔ y ≤ -x

Sign expansions #

structure SignExpansion :

Type (u + 1)

A sign expansion is a an ordinal indexed sequence of 1s and -1s, followed by 0s.

sign : NatOrdinal → SignType
The sequence defining the sign expansion.
isUpperSet_preimage_singleton_zero' : IsUpperSet (self.sign ⁻¹' {0})
Every sign after the first 0 is also 0.
Do not use directly, use isUpperSet_preimage_singleton_zero instead.

Instances For

@[implicit_reducible]

instance SignExpansion.instFunLikeNatOrdinalSignType :

FunLike SignExpansion NatOrdinal SignType

Equations

SignExpansion.instFunLikeNatOrdinalSignType = { coe := SignExpansion.sign, coe_injective := ⋯ }

theorem SignExpansion.isUpperSet_preimage_singleton_zero (x : SignExpansion) :

IsUpperSet (⇑x ⁻¹' {0})

Every sign after the first 0 is also 0.

def SignExpansion.copy (x : SignExpansion) (sign : NatOrdinal → SignType) (h : sign = ⇑x) :

Adjust definitional equalities of a sign expansion.

Equations

x.copy sign h = { sign := sign, isUpperSet_preimage_singleton_zero' := ⋯ }

Instances For

@[simp]

theorem SignExpansion.copy_eq (x : SignExpansion) (sign : NatOrdinal → SignType) (h : sign = ⇑x) :

x.copy sign h = x

@[simp]

theorem SignExpansion.coe_mk (f : NatOrdinal → SignType) (h : IsUpperSet (f ⁻¹' {0})) :

⇑{ sign := f, isUpperSet_preimage_singleton_zero' := h } = f

@[simp]

theorem SignExpansion.sign_eq_coe (x : SignExpansion) :

x.sign = ⇑x

theorem SignExpansion.ext {x y : SignExpansion} (hxy : ∀ (o : NatOrdinal), x o = y o) :

x = y

theorem SignExpansion.ext_iff {x y : SignExpansion} :

x = y ↔ ∀ (o : NatOrdinal), x o = y o

theorem SignExpansion.mk_eq_mk {f g : NatOrdinal → SignType} {h₁ : IsUpperSet (f ⁻¹' {0})} {h₂ : IsUpperSet (g ⁻¹' {0})} :

{ sign := f, isUpperSet_preimage_singleton_zero' := h₁ } = { sign := g, isUpperSet_preimage_singleton_zero' := h₂ } ↔ f = g

theorem SignExpansion.apply_eq_zero_of_le {x : SignExpansion} {o o' : NatOrdinal} (hoo' : o ≤ o') (ho : x o = 0) :

x o' = 0

noncomputable def SignExpansion.length (x : SignExpansion) :

WithTop NatOrdinal

The length of a sign expansion is the smallest ordinal at which it equals zero, or ⊤ is no such ordinal exists.

Equations

x.length = sInf (WithTop.some '' ⇑x ⁻¹' {0})

Instances For

theorem SignExpansion.apply_of_length_le {x : SignExpansion} {o : NatOrdinal} (h : x.length ≤ ↑o) :

x o = 0

theorem SignExpansion.apply_eq_zero {x : SignExpansion} {o : NatOrdinal} :

x o = 0 ↔ x.length ≤ ↑o

theorem SignExpansion.apply_ne_zero {x : SignExpansion} {o : NatOrdinal} :

x o ≠ 0 ↔ ↑o < x.length

theorem SignExpansion.length_eq_top {x : SignExpansion} :

x.length = ⊤ ↔ ∀ (o : NatOrdinal), x o ≠ 0

Basic sign expansions #

def SignExpansion.const (s : SignType) :

The constant sign expansion sss...

Equations

SignExpansion.const s = { sign := fun (x : NatOrdinal) => s, isUpperSet_preimage_singleton_zero' := ⋯ }

Instances For

@[implicit_reducible]

instance SignExpansion.instZero :

Zero SignExpansion

Equations

SignExpansion.instZero = { zero := SignExpansion.const 0 }

@[implicit_reducible]

instance SignExpansion.instInhabited :

Inhabited SignExpansion

Equations

SignExpansion.instInhabited = { default := 0 }

@[simp]

theorem SignExpansion.coe_zero :

⇑0 = 0

theorem SignExpansion.zero_apply (o : NatOrdinal) :

0 o = 0

@[simp]

theorem SignExpansion.length_zero :

@[implicit_reducible]

instance SignExpansion.instBot :

Bot SignExpansion

Equations

SignExpansion.instBot = { bot := SignExpansion.const (-1) }

@[simp]

theorem SignExpansion.coe_bot :

⇑⊥ = -1

theorem SignExpansion.bot_apply (o : NatOrdinal) :

⊥ o = -1

@[simp]

theorem SignExpansion.length_bot :

⊥.length = ⊤

@[implicit_reducible]

instance SignExpansion.instTop :

Top SignExpansion

Equations

SignExpansion.instTop = { top := SignExpansion.const 1 }

@[simp]

theorem SignExpansion.coe_top :

⇑⊤ = 1

theorem SignExpansion.top_apply (o : NatOrdinal) :

⊤ o = 1

@[simp]

theorem SignExpansion.length_top :

⊤.length = ⊤

def SignExpansion.Small (x : SignExpansion) :

We say a sign expansion is "small" when it has length < ⊤. Equivalently, it contains at least one (and thus infinitely many) zeros.

Equations

x.Small = (x.length ≠ ⊤)

Instances For

theorem SignExpansion.small_iff_length_ne_top {x : SignExpansion} :

x.Small ↔ x.length ≠ ⊤

theorem SignExpansion.small_iff_length_lt_top {x : SignExpansion} :

x.Small ↔ x.length < ⊤

theorem SignExpansion.Small.length_ne_top {x : SignExpansion} :

x.Small → x.length ≠ ⊤

Alias of the forward direction of SignExpansion.small_iff_length_ne_top.

theorem SignExpansion.Small.length_lt_top {x : SignExpansion} :

x.Small → x.length < ⊤

Alias of the forward direction of SignExpansion.small_iff_length_lt_top.

@[simp]

theorem SignExpansion.Small.zero :

theorem SignExpansion.small_iff_exists_eq_zero {x : SignExpansion} :

x.Small ↔ ∃ (o : NatOrdinal), x o = 0

@[implicit_reducible]

instance SignExpansion.instNeg :

Neg SignExpansion

Equations

SignExpansion.instNeg = { neg := fun (e : SignExpansion) => { sign := -⇑e, isUpperSet_preimage_singleton_zero' := ⋯ } }

@[simp]

theorem SignExpansion.coe_neg (x : SignExpansion) :

⇑(-x) = -⇑x

theorem SignExpansion.neg_apply (x : SignExpansion) (o : NatOrdinal) :

(-x) o = -x o

@[simp]

theorem SignExpansion.neg_mk (f : NatOrdinal → SignType) (h : IsUpperSet (f ⁻¹' {0})) :

-{ sign := f, isUpperSet_preimage_singleton_zero' := h } = { sign := -f, isUpperSet_preimage_singleton_zero' := ⋯ }

@[simp]

theorem SignExpansion.neg_zero :

-0 = 0

@[simp]

theorem SignExpansion.neg_bot :

@[simp]

theorem SignExpansion.neg_top :

@[simp]

theorem SignExpansion.length_neg (x : SignExpansion) :

(-x).length = x.length

@[simp]

theorem SignExpansion.small_neg_iff {x : SignExpansion} :

(-x).Small ↔ x.Small

theorem SignExpansion.Small.neg {x : SignExpansion} :

x.Small → (-x).Small

Alias of the reverse direction of SignExpansion.small_neg_iff.

@[implicit_reducible]

instance SignExpansion.instInvolutiveNeg :

InvolutiveNeg SignExpansion

Equations

SignExpansion.instInvolutiveNeg = { toNeg := SignExpansion.instNeg, neg_neg := ⋯ }

noncomputable def SignExpansion.restrict (x : SignExpansion) (o : WithTop NatOrdinal) :

Cut off the part of a sign expansion after an ordinal o, by filling it in with zeros.

Equations

x.restrict o = { sign := fun (i : NatOrdinal) => if ↑i < o then x i else 0, isUpperSet_preimage_singleton_zero' := ⋯ }

Instances For

def SignExpansion.«term_↾_» :

Lean.TrailingParserDescr

Cut off the part of a sign expansion after an ordinal o, by filling it in with zeros.

Conventions for notations in identifiers:

The recommended spelling of ↾ in identifiers is restrict.

Equations

SignExpansion.«term_↾_» = Lean.ParserDescr.trailingNode `SignExpansion.«term_↾_» 1022 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↾ ") (Lean.ParserDescr.cat `term 70))

Instances For

theorem SignExpansion.coe_restrict (x : SignExpansion) (o : WithTop NatOrdinal) :

⇑(x.restrict o) = fun (i : NatOrdinal) => if ↑i < o then x i else 0

@[simp]

theorem SignExpansion.neg_restrict (x : SignExpansion) (o : WithTop NatOrdinal) :

-x.restrict o = (-x).restrict o

theorem SignExpansion.restrict_apply_of_coe_lt {x : SignExpansion} {o₁ : WithTop NatOrdinal} {o₂ : NatOrdinal} (h : ↑o₂ < o₁) :

(x.restrict o₁) o₂ = x o₂

theorem SignExpansion.restrict_apply_of_le_coe {x : SignExpansion} {o₁ : WithTop NatOrdinal} {o₂ : NatOrdinal} (h : o₁ ≤ ↑o₂) :

(x.restrict o₁) o₂ = 0

@[simp]

theorem SignExpansion.length_restrict (x : SignExpansion) (o : WithTop NatOrdinal) :

(x.restrict o).length = min x.length o

@[simp]

theorem SignExpansion.small_restrict (x : SignExpansion) (o : NatOrdinal) :

(x.restrict ↑o).Small

@[simp]

theorem SignExpansion.restrict_of_length_le {x : SignExpansion} {o : WithTop NatOrdinal} (ho : x.length ≤ o) :

x.restrict o = x

@[simp]

theorem SignExpansion.restrict_restrict_eq {x : SignExpansion} {o₁ o₂ : WithTop NatOrdinal} :

(x.restrict o₁).restrict o₂ = x.restrict (min o₁ o₂)

theorem SignExpansion.restrict_zero_left (o : WithTop NatOrdinal) :

restrict 0 o = 0

@[simp]

theorem SignExpansion.restrict_zero_right (x : SignExpansion) :

x.restrict 0 = 0

theorem SignExpansion.restrict_top_right {x : SignExpansion} :

x.restrict ⊤ = x

Order structure #

@[implicit_reducible]

noncomputable instance SignExpansion.instCompleteLinearOrderSignType :

CompleteLinearOrder SignType

Equations

SignExpansion.instCompleteLinearOrderSignType = Fintype.toCompleteLinearOrder SignType

@[implicit_reducible]

noncomputable instance SignExpansion.instLinearOrder :

LinearOrder SignExpansion

Equations

SignExpansion.instLinearOrder = LinearOrder.lift' (fun (x : SignExpansion) => toLex ⇑x) SignExpansion.instLinearOrder._proof_1

theorem SignExpansion.le_iff_toLex {x y : SignExpansion} :

x ≤ y ↔ toLex ⇑x ≤ toLex ⇑y

theorem SignExpansion.lt_iff_toLex {x y : SignExpansion} :

x < y ↔ toLex ⇑x < toLex ⇑y

@[implicit_reducible]

instance SignExpansion.instBoundedOrder :

BoundedOrder SignExpansion

Equations

One or more equations did not get rendered due to their size.

theorem SignExpansion.neg_lt_neg {x y : SignExpansion} (h : x < y) :

-y < -x

@[simp]

theorem SignExpansion.neg_lt_neg_iff {x y : SignExpansion} :

-x < -y ↔ y < x

@[simp]

theorem SignExpansion.neg_le_neg_iff {x y : SignExpansion} :

-x ≤ -y ↔ y ≤ x

theorem SignExpansion.neg_le {x y : SignExpansion} :

-x ≤ y ↔ -y ≤ x

theorem SignExpansion.le_neg {x y : SignExpansion} :

x ≤ -y ↔ y ≤ -x

theorem SignExpansion.neg_lt {x y : SignExpansion} :

-x < y ↔ -y < x

theorem SignExpansion.lt_neg {x y : SignExpansion} :

x < -y ↔ y < -x

Floor function #

noncomputable def SignExpansion.floor (f : NatOrdinal → SignType) :

The floor function on a function NatOrdinal → SignType "rounds" it downwards to the nearest valid SignExpansion.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem SignExpansion.floor_of_isUpperSet {f : NatOrdinal → SignType} (hf : IsUpperSet (f ⁻¹' {0})) :

floor f = { sign := f, isUpperSet_preimage_singleton_zero' := hf }

@[simp]

theorem SignExpansion.floor_coe (x : SignExpansion) :

floor ⇑x = x

theorem SignExpansion.floor_apply_of_lt_sInf {f : NatOrdinal → SignType} {a : NatOrdinal} (hf : a < sInf (f ⁻¹' {0})) :

(floor f) a = f a

theorem SignExpansion.floor_lt_of_not_isUpperSet {f : NatOrdinal → SignType} (hf : ¬IsUpperSet (f ⁻¹' {0})) :

toLex ⇑(floor f) < toLex f

theorem SignExpansion.floor_le (f : NatOrdinal → SignType) :

toLex ⇑(floor f) ≤ toLex f

theorem SignExpansion.floor_lt {f : NatOrdinal → SignType} {x : SignExpansion} :

floor f < x ↔ toLex f < toLex ⇑x

theorem SignExpansion.le_floor {f : NatOrdinal → SignType} {x : SignExpansion} :

x ≤ floor f ↔ toLex ⇑x ≤ toLex f

theorem SignExpansion.gc_coe_floor :

GaloisConnection (⇑toLex ∘ fun (x : SignExpansion) => ⇑x) (floor ∘ ⇑ofLex)

noncomputable def SignExpansion.gciFloor :

GaloisCoinsertion (⇑toLex ∘ fun (x : SignExpansion) => ⇑x) (floor ∘ ⇑ofLex)

floor as a Galois coinsertion.

Equations

One or more equations did not get rendered due to their size.

Instances For

Ceiling function #

noncomputable def SignExpansion.ceil (f : NatOrdinal → SignType) :

The ceiling function on a function NatOrdinal → SignType "rounds" it upwards to the nearest valid SignExpansion.

Equations

SignExpansion.ceil f = -SignExpansion.floor (-f)

Instances For

theorem SignExpansion.ceil_of_isUpperSet {f : NatOrdinal → SignType} (hf : IsUpperSet (f ⁻¹' {0})) :

ceil f = { sign := f, isUpperSet_preimage_singleton_zero' := hf }

@[simp]

theorem SignExpansion.ceil_coe (x : SignExpansion) :

ceil ⇑x = x

theorem SignExpansion.ceil_apply_of_lt_sInf {f : NatOrdinal → SignType} {a : NatOrdinal} (hf : a < sInf (f ⁻¹' {0})) :

(ceil f) a = f a

theorem SignExpansion.lt_ceil_of_not_isUpperSet {f : NatOrdinal → SignType} (h : ¬IsUpperSet (f ⁻¹' {0})) :

toLex f < toLex ⇑(ceil f)

theorem SignExpansion.le_ceil (f : NatOrdinal → SignType) :

toLex f ≤ toLex ⇑(ceil f)

theorem SignExpansion.lt_ceil {f : NatOrdinal → SignType} {x : SignExpansion} :

x < ceil f ↔ toLex ⇑x < toLex f

theorem SignExpansion.ceil_le {f : NatOrdinal → SignType} {x : SignExpansion} :

ceil f ≤ x ↔ toLex f ≤ toLex ⇑x

theorem SignExpansion.gc_ceil_coe :

GaloisConnection (ceil ∘ ⇑ofLex) (⇑toLex ∘ fun (x : SignExpansion) => ⇑x)

noncomputable def SignExpansion.giCeil :

GaloisInsertion (ceil ∘ ⇑ofLex) (⇑toLex ∘ fun (x : SignExpansion) => ⇑x)

ceil as a Galois insertion.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem SignExpansion.floor_neg (f : NatOrdinal → SignType) :

floor (-f) = -ceil f

@[simp]

theorem SignExpansion.ceil_neg (f : NatOrdinal → SignType) :

ceil (-f) = -floor f

theorem SignExpansion.floor_le_ceil (f : NatOrdinal → SignType) :

floor f ≤ ceil f

theorem SignExpansion.floor_lt_ceil_of_not_isUpperSet {f : NatOrdinal → SignType} (h : ¬IsUpperSet (f ⁻¹' {0})) :

floor f < ceil f

Complete linear order instance #

@[implicit_reducible]

noncomputable instance SignExpansion.instCompleteLattice :

CompleteLattice SignExpansion

Equations

One or more equations did not get rendered due to their size.

@[implicit_reducible]

noncomputable instance SignExpansion.instCompleteLinearOrder :

CompleteLinearOrder SignExpansion

Equations

One or more equations did not get rendered due to their size.

theorem SignExpansion.coe_sInf (s : Set SignExpansion) :

⇑(sInf s) = ofLex (sInf ((fun (x : SignExpansion) => toLex ⇑x) '' s))

theorem SignExpansion.coe_iInf {ι : Sort u_1} (f : ι → SignExpansion) :

⇑(⨅ (i : ι), f i) = ofLex (⨅ (i : ι), toLex ⇑(f i))

theorem SignExpansion.sInf_apply (s : Set SignExpansion) (i : NatOrdinal) :

(sInf s) i = ⨅ (x : { x : SignExpansion // x ∈ s ∧ ∀ j < i, x j = (sInf s) j }), ↑x i

theorem SignExpansion.coe_sSup (s : Set SignExpansion) :

⇑(sSup s) = ofLex (sSup ((fun (x : SignExpansion) => toLex ⇑x) '' s))

theorem SignExpansion.coe_iSup {ι : Sort u_1} (f : ι → SignExpansion) :

⇑(⨆ (i : ι), f i) = ofLex (⨆ (i : ι), toLex ⇑(f i))

theorem SignExpansion.sSup_apply (s : Set SignExpansion) (i : NatOrdinal) :

(sSup s) i = ⨆ (x : { x : SignExpansion // x ∈ s ∧ ∀ j < i, x j = (sSup s) j }), ↑x i

Cast from ordinals #

noncomputable def NatOrdinal.toSignExpansion :

NatOrdinal ↪o SignExpansion

Returns the sign expansion with the corresponding number of 1s.

Equations

NatOrdinal.toSignExpansion = OrderEmbedding.ofStrictMono (fun (x : NatOrdinal) => ⊤.restrict ↑x) ⋯

Instances For

@[implicit_reducible]

noncomputable instance NatOrdinal.instCoeSignExpansion :

Coe NatOrdinal SignExpansion

Equations

NatOrdinal.instCoeSignExpansion = { coe := fun (x : NatOrdinal) => NatOrdinal.toSignExpansion x }

theorem NatOrdinal.coe_toSignExpansion (o : NatOrdinal) :

⇑(toSignExpansion o) = fun (i : NatOrdinal) => if i < o then 1 else 0

@[simp]

theorem NatOrdinal.top_restrict (o : NatOrdinal) :

⊤.restrict ↑o = toSignExpansion o

@[simp]

theorem NatOrdinal.bot_restrict (o : NatOrdinal) :

⊥.restrict ↑o = -toSignExpansion o

@[simp]

theorem NatOrdinal.length_toSignExpansion (o : NatOrdinal) :

(toSignExpansion o).length = ↑o

theorem NatOrdinal.toSignExpansion_apply_of_lt {o₁ o₂ : NatOrdinal} (h : o₂ < o₁) :

(toSignExpansion o₁) o₂ = 1

theorem NatOrdinal.toSignExpansion_apply_of_le {o₁ o₂ : NatOrdinal} (h : o₁ ≤ o₂) :

(toSignExpansion o₁) o₂ = 0