Omnific integers

We define the omnific integers, as the subring of surreals such that x = {x - 1 | x + 1}.

Todo

Prove the characterization of omnific integers, as surreals whose Hahn series x have the following form:

• x.support ⊆ Ici 0
• x.coeff 0 is an integer

Rounding operation

noncomputable def Surreal.round (x r : Surreal) : Surreal

We define x.round r = {x - r | x + r} whenever 0 < r. For r ≤ 0, we set the junk value x.round r = x.

If r = 1, this operation truncates the fractional part of x, rounding up or down to whichever omnific integer is simplest.

Equations

• x.round r = if hr : 0 < r then !{{x - r} | {x + r}} else x

theorem Surreal.round_of_pos {x r : Surreal} (hr : 0 < r) : x.round r = !{{x - r} | {x + r}}

theorem Surreal.round_of_nonpos {x r : Surreal} (hr : r ≤ 0) : x.round r = x

theorem Surreal.round_mk_of_pos {x r : IGame} (hr : 0 < r) [x.Numeric] [r.Numeric] : (mk x).round (mk r) = mk !{{x - r} | {x + r}}

theorem Surreal.round_of_zero_mem {x r : Surreal} (h : 0 ∈ Set.Ioo (x - r) (x + r)) : x.round r = 0

@[simp]

theorem Surreal.round_zero (r : Surreal) : round 0 r = 0

@[simp]

theorem Surreal.round_neg {x r : Surreal} : (-x).round r = -x.round r

theorem Surreal.round_add_of_eq {x y r : Surreal} (hx : x.round r = x) (hy : y.round r = y) : (x + y).round r = x + y

theorem Surreal.round_sub_of_eq {x y r : Surreal} (hx : x.round r = x) (hy : y.round r = y) : (x - y).round r = x - y

theorem Surreal.round_mul_of_eq {x y r : Surreal} (h : 0 < r) (hx : x.round r = x) (hy : y.round r = y) : (x * y).round (r * r) = x * y

Omnific integers

def Surreal.IsOmnific (x : Surreal) : Prop

An omnific integer is one such that x = {x - 1 | x + 1}. These are an analog of the integers to the surreals.

Equations

• x.IsOmnific = (x.round 1 = x)

theorem Surreal.IsOmnific.eq {x : Surreal} (h : x.IsOmnific) : x.round 1 = x

@[simp]

theorem Surreal.IsOmnific.zero : IsOmnific 0

@[simp]

theorem Surreal.IsOmnific.one : IsOmnific 1

theorem Surreal.IsOmnific.neg {x : Surreal} (hx : x.IsOmnific) : (-x).IsOmnific

@[simp]

theorem Surreal.isOmnific_neg_iff {x : Surreal} : (-x).IsOmnific ↔ x.IsOmnific

theorem Surreal.IsOmnific.add {x y : Surreal} (hx : x.IsOmnific) (hy : y.IsOmnific) : (x + y).IsOmnific

theorem Surreal.IsOmnific.sub {x y : Surreal} (hx : x.IsOmnific) (hy : y.IsOmnific) : (x - y).IsOmnific

theorem Surreal.IsOmnific.mul {x y : Surreal} (hx : x.IsOmnific) (hy : y.IsOmnific) : (x * y).IsOmnific

theorem Surreal.IsOmnific.one_le_iff_pos {x : Surreal} (h : x.IsOmnific) : 1 ≤ x ↔ 0 < x

theorem Surreal.IsOmnific.lt_one_iff_nonpos {x : Surreal} (h : x.IsOmnific) : x < 1 ↔ x ≤ 0

def Surreal.omnific : Subring Surreal

The subring of IsOmnific surreal numbers.

Equations

• Surreal.omnific = { carrier := {x : Surreal | x.IsOmnific}, mul_mem' := ⋯, one_mem' := Surreal.IsOmnific.one, add_mem' := ⋯, zero_mem' := Surreal.IsOmnific.zero, neg_mem' := ⋯ }

@[simp]

theorem Surreal.mem_omnific_iff {x : Surreal} : x ∈ omnific ↔ x.IsOmnific

@[simp]

theorem Surreal.IsOmnific.natCast (n : ℕ) : (↑n).IsOmnific

@[simp]

theorem Surreal.IsOmnific.intCast (n : ℤ) : (↑n).IsOmnific

@[simp]

theorem Surreal.isOmnific_realCast_iff {r : ℝ} : (↑r).IsOmnific ↔ r ∈ Set.range Int.cast

@[simp]

theorem Surreal.isOmnific_ratCast_iff {q : ℚ} : (↑q).IsOmnific ↔ q ∈ Set.range Int.cast