Surreal Hahn series

Hahn series are a generalization of power series and Puiseux series. A Hahn series R⟦Γ⟧ is defined as a function Γ → R whose support is well-founded. This condition is sufficient to define addition and multiplication as with polynomials, so that under suitable conditions, R⟦Γ⟧ has the structure of an ordered field.

The aphorism goes that surreals are real Hahn series over themselves. However, there are a few technicalities. Hahn series are conventionally defined so that the support has well-founded <, whereas for surreals it's more natural to assume well-founded >. Moreover, the Hahn series that correspond to surreals must have a Small support. Because of this, we often prefer to identify these surreal Hahn series with ordinal-indexed sequences of surreal exponents and their coefficients.

This file provides the translation layer between Hahn series as they're implemented in Mathlib, and the Hahn series relevant to surreal numbers, by defining the type SurrealHahnSeries for the latter.

For Mathlib

theorem Set.IsWF.to_subtype {α : Type u_1} [LT α] {s : Set α} (h : s.IsWF) : WellFoundedLT ↑s

@[simp]

theorem equivShrink_le_equivShrink_iff {α : Type u_1} [Preorder α] [Small.{u, u_1} α] {x y : α} : (equivShrink α) x ≤ (equivShrink α) y ↔ x ≤ y

@[simp]

theorem equivShrink_lt_equivShrink_iff {α : Type u_1} [Preorder α] [Small.{u, u_1} α] {x y : α} : (equivShrink α) x < (equivShrink α) y ↔ x < y

@[simp]

theorem Ordinal.type_lt_Iio (o : Ordinal.{u}) : (type fun (x1 x2 : ↑(Set.Iio o)) => x1 < x2) = lift.{u + 1, u} o

def RelIso.subrel {α : Type u_1} (r : α → α → Prop) {p q : α → Prop} (H : ∀ (x : α), p x ↔ q x) : Subrel r p ≃r Subrel r q

Equations

• RelIso.subrel r H = { toEquiv := (Equiv.refl α).subtypeEquiv H, map_rel_iff' := ⋯ }

Basic defs and instances

def SurrealHahnSeries : Type (u + 1)

The type of u-small Hahn series over Surrealᵒᵈ, endowed with the lexicographic ordering. We will show that this type is isomorphic as an ordered field to the surreals themselves.

Equations

• SurrealHahnSeries = ↥(HahnSeries.cardSuppLTSubfield Surrealᵒᵈ ℝ Cardinal.univ.{?u.4, ?u.4})

instance SurrealHahnSeries.instField : Field SurrealHahnSeries

Equations

• SurrealHahnSeries.instField = id inferInstance

instance SurrealHahnSeries.instLinearOrder : LinearOrder SurrealHahnSeries

Equations

• SurrealHahnSeries.instLinearOrder = id inferInstance

instance SurrealHahnSeries.instIsStrictOrderedRing : IsStrictOrderedRing SurrealHahnSeries

def SurrealHahnSeries.mk (f : Surreal → ℝ) (small : Small.{u, u + 1} ↑(Function.support f)) (wf : (Function.support f).WellFoundedOn fun (x1 x2 : Surreal) => x1 > x2) : SurrealHahnSeries

A constructor for SurrealHahnSeries which hides various implementation details.

Equations

• SurrealHahnSeries.mk f small wf = ⟨toLex { coeff := f ∘ ⇑OrderDual.ofDual, isPWO_support' := ⋯ }, ⋯⟩

coeff

def SurrealHahnSeries.coeff (x : SurrealHahnSeries) (i : Surreal) : ℝ

Returns the coefficient for X ^ i.

Equations

• x.coeff i = (↑x).coeff (OrderDual.toDual i)

@[simp]

theorem SurrealHahnSeries.coeff_mk (f : Surreal → ℝ) (small : Small.{u_1, u_1 + 1} ↑(Function.support f)) (wf : (Function.support f).WellFoundedOn fun (x1 x2 : Surreal) => x1 > x2) : (mk f small wf).coeff = f

@[simp]

theorem SurrealHahnSeries.coeff_zero : coeff 0 = 0

@[simp]

theorem SurrealHahnSeries.coeff_neg (x : SurrealHahnSeries) : (-x).coeff = -x.coeff

@[simp]

theorem SurrealHahnSeries.coeff_add (x y : SurrealHahnSeries) : (x + y).coeff = x.coeff + y.coeff

@[simp]

theorem SurrealHahnSeries.coeff_sub (x y : SurrealHahnSeries) : (x - y).coeff = x.coeff - y.coeff

theorem SurrealHahnSeries.coeff_add_apply (x y : SurrealHahnSeries) (i : Surreal) : (x + y).coeff i = x.coeff i + y.coeff i

theorem SurrealHahnSeries.coeff_sub_apply (x y : SurrealHahnSeries) (i : Surreal) : (x - y).coeff i = x.coeff i - y.coeff i

theorem SurrealHahnSeries.ext {x y : SurrealHahnSeries} (h : x.coeff = y.coeff) : x = y

theorem SurrealHahnSeries.ext_iff {x y : SurrealHahnSeries} : x = y ↔ x.coeff = y.coeff

support

def SurrealHahnSeries.support (x : SurrealHahnSeries) : Set Surreal

The support of the Hahn series.

Equations

• x.support = Function.support x.coeff

@[simp]

theorem SurrealHahnSeries.support_coeff (x : SurrealHahnSeries) : Function.support x.coeff = x.support

@[simp]

theorem SurrealHahnSeries.support_mk (f : Surreal → ℝ) (small : Small.{u_1, u_1 + 1} ↑(Function.support f)) (wf : (Function.support f).WellFoundedOn fun (x1 x2 : Surreal) => x1 > x2) : (mk f small wf).support = Function.support f

@[simp]

theorem SurrealHahnSeries.mem_support_iff {x : SurrealHahnSeries} {i : Surreal} : i ∈ x.support ↔ x.coeff i ≠ 0

@[simp]

theorem SurrealHahnSeries.support_eq_empty {x : SurrealHahnSeries} : x.support = ∅ ↔ x = 0

@[simp]

theorem SurrealHahnSeries.support_zero : support 0 = ∅

theorem SurrealHahnSeries.support_add_subset {x y : SurrealHahnSeries} : (x + y).support ⊆ x.support ∪ y.support

theorem SurrealHahnSeries.wellFoundedOn_support (x : SurrealHahnSeries) : x.support.WellFoundedOn fun (x1 x2 : Surreal) => x1 > x2

instance SurrealHahnSeries.instWellFoundedGTElemSurrealSupport (x : SurrealHahnSeries) : WellFoundedGT ↑x.support

instance SurrealHahnSeries.instIsWellOrderElemSurrealSupportSubrelGtMemSet (x : SurrealHahnSeries) : IsWellOrder (↑x.support) (Subrel (fun (x1 x2 : Surreal) => x1 > x2) fun (x_1 : Surreal) => x_1 ∈ x.support)

instance SurrealHahnSeries.small_support (x : SurrealHahnSeries) : Small.{u, u + 1} ↑x.support

@[simp]

theorem SurrealHahnSeries.mk_coeff (x : SurrealHahnSeries) : mk x.coeff ⋯ ⋯ = x

theorem SurrealHahnSeries.lt_def {x y : SurrealHahnSeries} : x < y ↔ toColex x.coeff < toColex y.coeff

theorem SurrealHahnSeries.le_def {x y : SurrealHahnSeries} : x ≤ y ↔ toColex x.coeff ≤ toColex y.coeff

single

def SurrealHahnSeries.single (x : Surreal) (r : ℝ) : SurrealHahnSeries

The Hahn series with a single entry.

Equations

• SurrealHahnSeries.single x r = SurrealHahnSeries.mk (Pi.single x r) ⋯ ⋯

theorem SurrealHahnSeries.coeff_single (x : Surreal) (r : ℝ) : (single x r).coeff = Pi.single x r

@[simp]

theorem SurrealHahnSeries.coeff_single_self (x : Surreal) (r : ℝ) : (single x r).coeff x = r

theorem SurrealHahnSeries.coeff_single_of_ne {x y : Surreal} (h : x ≠ y) (r : ℝ) : (single x r).coeff y = 0

@[simp]

theorem SurrealHahnSeries.single_zero (x : Surreal) : single x 0 = 0

theorem SurrealHahnSeries.support_single_subset {x : Surreal} {r : ℝ} : (single x r).support ⊆ {x}

trunc

def SurrealHahnSeries.trunc (x : SurrealHahnSeries) (i : Surreal) : SurrealHahnSeries

Zeroes out any terms of the Hahn series less than or equal to i.

Equations

• x.trunc i = SurrealHahnSeries.mk (fun (j : Surreal) => if i < j then x.coeff j else 0) ⋯ ⋯

theorem SurrealHahnSeries.coeff_trunc (x : SurrealHahnSeries) (i : Surreal) : (x.trunc i).coeff = fun (j : Surreal) => if i < j then x.coeff j else 0

@[simp]

theorem SurrealHahnSeries.support_trunc (x : SurrealHahnSeries) (i : Surreal) : (x.trunc i).support = x.support ∩ Set.Ioi i

theorem SurrealHahnSeries.support_trunc_subset (x : SurrealHahnSeries) (i : Surreal) : (x.trunc i).support ⊆ x.support

theorem SurrealHahnSeries.support_trunc_anti {x : SurrealHahnSeries} : Antitone fun (i : Surreal) => (x.trunc i).support

@[simp]

theorem SurrealHahnSeries.coeff_trunc_of_lt {x : SurrealHahnSeries} {i j : Surreal} (h : i < j) : (x.trunc i).coeff j = x.coeff j

@[simp]

theorem SurrealHahnSeries.coeff_trunc_of_le {x : SurrealHahnSeries} {i j : Surreal} (h : j ≤ i) : (x.trunc i).coeff j = 0

theorem SurrealHahnSeries.coeff_trunc_eq_zero {x : SurrealHahnSeries} {i j : Surreal} (h : x.coeff i = 0) : (x.trunc j).coeff i = 0

theorem SurrealHahnSeries.coeff_trunc_of_mem {x : SurrealHahnSeries} {i j : Surreal} (h : j ∈ (x.trunc i).support) : (x.trunc i).coeff j = x.coeff j

@[simp]

theorem SurrealHahnSeries.trunc_add (x y : SurrealHahnSeries) (i : Surreal) : (x + y).trunc i = x.trunc i + y.trunc i

@[simp]

theorem SurrealHahnSeries.trunc_sub (x y : SurrealHahnSeries) (i : Surreal) : (x - y).trunc i = x.trunc i - y.trunc i

@[simp]

theorem SurrealHahnSeries.trunc_single_of_le {i j : Surreal} {r : ℝ} (h : i ≤ j) : (single i r).trunc j = 0

@[simp]

theorem SurrealHahnSeries.trunc_single_of_lt {i j : Surreal} {r : ℝ} (h : j < i) : (single i r).trunc j = single i r

@[simp]

theorem SurrealHahnSeries.trunc_trunc (x : SurrealHahnSeries) (i j : Surreal) : (x.trunc i).trunc j = x.trunc (max i j)

theorem SurrealHahnSeries.trunc_eq_self_iff {x : SurrealHahnSeries} {i : Surreal} : x.trunc i = x ↔ ∀ j ∈ x.support, i < j

theorem SurrealHahnSeries.trunc_eq_self {x : SurrealHahnSeries} {i : Surreal} : (∀ j ∈ x.support, i < j) → x.trunc i = x

Alias of the reverse direction of SurrealHahnSeries.trunc_eq_self_iff.

theorem SurrealHahnSeries.trunc_eq_trunc {x : SurrealHahnSeries} {i j : Surreal} (h : i ≤ j) (H : ∀ (k : Surreal), i < k → k ≤ j → x.coeff k = 0) : x.trunc i = x.trunc j

theorem SurrealHahnSeries.trunc_add_single {x : SurrealHahnSeries} {i : Surreal} (hi : i ∈ lowerBounds x.support) : x.trunc i + single i (x.coeff i) = x

Indexing the support by ordinals

theorem SurrealHahnSeries.instIsWellOrderShrinkElemSurrealSupportGt (x : SurrealHahnSeries) : IsWellOrder (Shrink.{u, u + 1} ↑x.support) fun (x1 x2 : Shrink.{u, u + 1} ↑x.support) => x1 > x2

length

def SurrealHahnSeries.length (x : SurrealHahnSeries) : Ordinal.{u}

The length of a surreal Hahn series is the order type of its support.

Equations

• x.length = Ordinal.type fun (x1 x2 : Shrink.{?u.9, ?u.9 + 1} ↑x.support) => x1 > x2

@[simp]

theorem SurrealHahnSeries.type_support (x : SurrealHahnSeries) : (Ordinal.type fun (x1 x2 : ↑x.support) => x1 > x2) = Ordinal.lift.{u + 1, u} x.length

@[simp]

theorem SurrealHahnSeries.length_eq_zero {x : SurrealHahnSeries} : x.length = 0 ↔ x = 0

@[simp]

theorem SurrealHahnSeries.length_zero : length 0 = 0

theorem SurrealHahnSeries.length_mono {x y : SurrealHahnSeries} (h : x.support ⊆ y.support) : x.length ≤ y.length

exp

def SurrealHahnSeries.exp (x : SurrealHahnSeries) : (fun (x1 x2 : ↑(Set.Iio x.length)) => x1 < x2) ≃r fun (x1 x2 : ↑x.support) => x1 > x2

Returns the i-th largest exponent with a non-zero coefficient.

This is registered as a RelIso between Iio x.length and x.support, so that x.exp.symm can be used to return the index of an element in the support.

Equations

• x.exp = (Ordinal.enum fun (x1 x2 : Shrink.{?u.38, ?u.38 + 1} ↑x.support) => x1 > x2).trans (orderIsoShrink ↑x.support).dual.toRelIsoLT.symm

@[simp]

theorem SurrealHahnSeries.symm_exp_lt {x : SurrealHahnSeries} (i : ↑x.support) : ↑(x.exp.symm i) < x.length

theorem SurrealHahnSeries.exp_strictAnti {x : SurrealHahnSeries} : StrictAnti ⇑x.exp

theorem SurrealHahnSeries.exp_anti {x : SurrealHahnSeries} : Antitone ⇑x.exp

@[simp]

theorem SurrealHahnSeries.exp_lt_exp_iff {x : SurrealHahnSeries} {i j : ↑(Set.Iio x.length)} : x.exp i < x.exp j ↔ j < i

@[simp]

theorem SurrealHahnSeries.exp_le_exp_iff {x : SurrealHahnSeries} {i j : ↑(Set.Iio x.length)} : x.exp i ≤ x.exp j ↔ j ≤ i

@[simp]

theorem SurrealHahnSeries.symm_exp_lt_symm_exp_iff {x : SurrealHahnSeries} {i j : ↑x.support} : x.exp.symm i < x.exp.symm j ↔ j < i

@[simp]

theorem SurrealHahnSeries.symm_exp_le_symm_exp_iff {x : SurrealHahnSeries} {i j : ↑x.support} : x.exp.symm i ≤ x.exp.symm j ↔ j ≤ i

theorem SurrealHahnSeries.eq_exp_of_mem_support {x : SurrealHahnSeries} {i : Surreal} (h : i ∈ x.support) : ∃ (j : ↑(Set.Iio x.length)), ↑(x.exp j) = i

theorem SurrealHahnSeries.exp_congr {x y : SurrealHahnSeries} (h : x = y) (i : ↑(Set.Iio x.length)) : ↑(x.exp i) = ↑(y.exp ⟨↑i, ⋯⟩)

This lemma is useful for rewriting.

@[simp]

theorem SurrealHahnSeries.typein_support {x : SurrealHahnSeries} (i : ↑x.support) : (Ordinal.typein fun (x1 x2 : ↑x.support) => x1 > x2).toRelEmbedding i = Ordinal.lift.{u + 1, u} ↑(x.exp.symm i)

coeffIdx

def SurrealHahnSeries.coeffIdx (x : SurrealHahnSeries) (i : Ordinal.{u_1}) : ℝ

Returns the coefficient which corresponds to the i-th largest exponent, or 0 if no such coefficient exists.

Equations

• x.coeffIdx i = if h : i < x.length then x.coeff ↑(x.exp ⟨i, h⟩) else 0

theorem SurrealHahnSeries.coeffIdx_of_lt {x : SurrealHahnSeries} {i : Ordinal.{u_1}} (h : i < x.length) : x.coeffIdx i = x.coeff ↑(x.exp ⟨i, h⟩)

theorem SurrealHahnSeries.coeffIdx_of_le {x : SurrealHahnSeries} {i : Ordinal.{u_1}} (h : x.length ≤ i) : x.coeffIdx i = 0

@[simp]

theorem SurrealHahnSeries.coeffIdx_zero : coeffIdx 0 = 0

@[simp]

theorem SurrealHahnSeries.coeff_exp (x : SurrealHahnSeries) (i : ↑(Set.Iio x.length)) : x.coeff ↑(x.exp i) = x.coeffIdx ↑i

@[simp]

theorem SurrealHahnSeries.coeffIdx_symm_exp (x : SurrealHahnSeries) (i : ↑x.support) : x.coeffIdx ↑(x.exp.symm i) = x.coeff ↑i

@[simp]

theorem SurrealHahnSeries.coeffIdx_eq_zero_iff {x : SurrealHahnSeries} {i : Ordinal.{u_1}} : x.coeffIdx i = 0 ↔ x.length ≤ i

truncIdx

def SurrealHahnSeries.truncIdx (x : SurrealHahnSeries) (i : Ordinal.{u}) : SurrealHahnSeries

Truncates the series at the i-th largest exponent, or returns it unchanged if no such coefficient exists.

Equations

• x.truncIdx i = if h : i < x.length then x.trunc ↑(x.exp ⟨i, h⟩) else x

theorem SurrealHahnSeries.support_truncIdx (x : SurrealHahnSeries) (i : Ordinal.{u_1}) : (x.truncIdx i).support = if hi : i < x.length then x.support ∩ Set.Ioi ↑(x.exp ⟨i, hi⟩) else x.support

theorem SurrealHahnSeries.truncIdx_of_lt {x : SurrealHahnSeries} {i : Ordinal.{u_1}} (h : i < x.length) : x.truncIdx i = x.trunc ↑(x.exp ⟨i, h⟩)

theorem SurrealHahnSeries.truncIdx_of_le {x : SurrealHahnSeries} {i : Ordinal.{u_1}} (h : x.length ≤ i) : x.truncIdx i = x

@[simp]

theorem SurrealHahnSeries.truncIdx_zero : truncIdx 0 = 0

@[simp]

theorem SurrealHahnSeries.trunc_exp (x : SurrealHahnSeries) (i : ↑(Set.Iio x.length)) : x.trunc ↑(x.exp i) = x.truncIdx ↑i

@[simp]

theorem SurrealHahnSeries.truncIdx_symm_exp (x : SurrealHahnSeries) (i : ↑x.support) : x.truncIdx ↑(x.exp.symm i) = x.trunc ↑i

theorem SurrealHahnSeries.support_truncIdx_ssubset {x : SurrealHahnSeries} {i : Ordinal.{u_1}} (h : i < x.length) : (x.truncIdx i).support ⊂ x.support

theorem SurrealHahnSeries.support_truncIdx_subset (x : SurrealHahnSeries) (i : Ordinal.{u_1}) : (x.truncIdx i).support ⊆ x.support

@[simp]

theorem SurrealHahnSeries.length_truncIdx (x : SurrealHahnSeries) (i : Ordinal.{u_1}) : (x.truncIdx i).length = min i x.length

theorem SurrealHahnSeries.length_trunc_lt {x : SurrealHahnSeries} {i : Surreal} (h : i ∈ x.support) : (x.trunc i).length < x.length

theorem SurrealHahnSeries.truncIdx_ne {x : SurrealHahnSeries} {i : Ordinal.{u_1}} (h : i < x.length) : x.truncIdx i ≠ x

theorem SurrealHahnSeries.coeff_truncIdx_of_mem {x : SurrealHahnSeries} {i : Ordinal.{u_1}} {j k : Surreal} (hjk : j ≤ k) (h : j ∈ (x.truncIdx i).support) : (x.truncIdx i).coeff k = x.coeff k

theorem SurrealHahnSeries.trunc_truncIdx_of_mem {x : SurrealHahnSeries} {i : Ordinal.{u_1}} {a b : Surreal} (hab : a ≤ b) (ha : a ∈ (x.truncIdx i).support) : (x.truncIdx i).trunc b = x.trunc b

term

def SurrealHahnSeries.term (x : SurrealHahnSeries) (i : Ordinal.{u_1}) : Surreal

Returns the i-th largest term of the sum, or 0 if it doesn't exist.

Equations

• x.term i = if hi : i < x.length then ↑(x.coeffIdx i) * ω^ ↑(x.exp ⟨i, hi⟩) else 0

theorem SurrealHahnSeries.term_of_lt {x : SurrealHahnSeries} {i : Ordinal.{u_1}} (hi : i < x.length) : x.term i = ↑(x.coeffIdx i) * ω^ ↑(x.exp ⟨i, hi⟩)

@[simp]

theorem SurrealHahnSeries.term_eq_zero {x : SurrealHahnSeries} {i : Ordinal.{u_1}} : x.term i = 0 ↔ x.length ≤ i

theorem SurrealHahnSeries.term_of_le {x : SurrealHahnSeries} {i : Ordinal.{u_1}} : x.length ≤ i → x.term i = 0

Alias of the reverse direction of SurrealHahnSeries.term_eq_zero.