Birthday of dyadic rationals

We prove that a surreal number has a finite birthday iff it's a dyadic number, and give an explicit formula for the birthday of a dyadic number.

theorem Nat.div_lt_div_iff_exists {a b c : ℕ} : a / c < b / c ↔ ∃ (d : ℕ), a < d ∧ d ≤ b ∧ c ∣ d

@[simp]

theorem Game.birthday_ratCast (x : ℚ) : (↑x).birthday = (↑x).birthday

theorem Surreal.birthday_dyadic_lt_omega0 (x : Dyadic) : (↑↑x).birthday < NatOrdinal.of Ordinal.omega0

theorem Surreal.birthday_lt_omega0_iff {x : Surreal} : x.birthday < NatOrdinal.of Ordinal.omega0 ↔ x ∈ Set.range fun (x : Dyadic) => ↑↑x

def Dyadic.birthday (x : Dyadic) : ℕ

The birthday of a dyadic number can be computed explicitly.

Equations

• x.birthday = if h : x.den = 1 then x.num.natAbs else (x.precision.get ⋯).toNat + x.num.natAbs / x.den + 1

@[simp]

theorem Dyadic.birthday_intCast (n : ℤ) : (↑n).birthday = n.natAbs

@[simp]

theorem Dyadic.birthday_natCast (n : ℕ) : (↑n).birthday = n

theorem Dyadic.birthday_of_den_eq_one {x : Dyadic} (hx : x.den = 1) : x.birthday = x.num.natAbs

theorem Dyadic.birthday_of_den_ne_one {x : Dyadic} (hx : x.den ≠ 1) : x.birthday = (x.precision.get ⋯).toNat + x.num.natAbs / x.den + 1

theorem Dyadic.natAbs_num_div_den_lower_eq_natAbs_num_div_den {x : Dyadic} (hxl : x.lower.den ≠ 1) : x.lower.num.natAbs / x.lower.den = x.num.natAbs / x.den

theorem Dyadic.natAbs_num_div_den_upper_eq_natAbs_num_div_den {x : Dyadic} (hxl : x.upper.den ≠ 1) : x.upper.num.natAbs / x.upper.den = x.num.natAbs / x.den

theorem Dyadic.max_birthday_lower_birthday_upper_add_one_of_den_ne_one {x : Dyadic} (hx : x.den ≠ 1) : max x.lower.birthday x.upper.birthday + 1 = x.birthday

@[simp]

theorem IGame.birthday_dyadic (x : Dyadic) : (↑x).birthday = ↑x.birthday