Ordinal exponential

In this file we define the power function and the logarithm function on ordinals. The two are related by the lemma Ordinal.opow_le_iff_le_log : b ^ c ≤ x ↔ c ≤ log b x for nontrivial inputs b, c.

instance Ordinal.pow : Pow Ordinal.{u} Ordinal.{u}

The ordinal exponential, defined by transfinite recursion.

Equations

• Ordinal.pow = { pow := fun (a b : Ordinal.{u}) => if a = 0 then 1 - b else b.limitRecOn 1 (fun (x IH : Ordinal.{u}) => IH * a) fun (b : Ordinal.{u}) (x : b.IsLimit) => b.bsup }

theorem Ordinal.opow_def (a : Ordinal.{u}) (b : Ordinal.{u}) : a ^ b = if a = 0 then 1 - b else b.limitRecOn 1 (fun (x IH : Ordinal.{u}) => IH * a) fun (b : Ordinal.{u}) (x : b.IsLimit) => b.bsup

theorem Ordinal.zero_opow' (a : Ordinal.{u_1}) : 0 ^ a = 1 - a

@[simp]

theorem Ordinal.zero_opow {a : Ordinal.{u_1}} (a0 : a ≠ 0) : 0 ^ a = 0

@[simp]

theorem Ordinal.opow_zero (a : Ordinal.{u_1}) : a ^ 0 = 1

@[simp]

theorem Ordinal.opow_succ (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) : a ^ Order.succ b = a ^ b * a

theorem Ordinal.opow_limit {a : Ordinal.{u}} {b : Ordinal.{u}} (a0 : a ≠ 0) (h : b.IsLimit) : a ^ b = b.bsup fun (c : Ordinal.{u}) (x : c < b) => a ^ c

theorem Ordinal.opow_le_of_limit {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} (a0 : a ≠ 0) (h : b.IsLimit) : a ^ b ≤ c ↔ ∀ b' < b, a ^ b' ≤ c

theorem Ordinal.lt_opow_of_limit {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} (b0 : b ≠ 0) (h : c.IsLimit) : a < b ^ c ↔ ∃ c' < c, a < b ^ c'

@[simp]

theorem Ordinal.opow_one (a : Ordinal.{u_1}) : a ^ 1 = a

@[simp]

theorem Ordinal.one_opow (a : Ordinal.{u_1}) : 1 ^ a = 1

theorem Ordinal.opow_pos {a : Ordinal.{u_1}} (b : Ordinal.{u_1}) (a0 : 0 < a) : 0 < a ^ b

theorem Ordinal.opow_ne_zero {a : Ordinal.{u_1}} (b : Ordinal.{u_1}) (a0 : a ≠ 0) : a ^ b ≠ 0

theorem Ordinal.opow_isNormal {a : Ordinal.{u_1}} (h : 1 < a) : Ordinal.IsNormal fun (x : Ordinal.{u_1}) => a ^ x

theorem Ordinal.opow_lt_opow_iff_right {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} (a1 : 1 < a) : a ^ b < a ^ c ↔ b < c

theorem Ordinal.opow_le_opow_iff_right {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} (a1 : 1 < a) : a ^ b ≤ a ^ c ↔ b ≤ c

theorem Ordinal.opow_right_inj {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} (a1 : 1 < a) : a ^ b = a ^ c ↔ b = c

theorem Ordinal.opow_isLimit {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (a1 : 1 < a) : b.IsLimit → (a ^ b).IsLimit

theorem Ordinal.opow_isLimit_left {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (l : a.IsLimit) (hb : b ≠ 0) : (a ^ b).IsLimit

theorem Ordinal.opow_le_opow_right {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} (h₁ : 0 < a) (h₂ : b ≤ c) : a ^ b ≤ a ^ c

theorem Ordinal.opow_le_opow_left {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (c : Ordinal.{u_1}) (ab : a ≤ b) : a ^ c ≤ b ^ c

theorem Ordinal.left_le_opow (a : Ordinal.{u_1}) {b : Ordinal.{u_1}} (b1 : 0 < b) : a ≤ a ^ b

theorem Ordinal.right_le_opow {a : Ordinal.{u_1}} (b : Ordinal.{u_1}) (a1 : 1 < a) : b ≤ a ^ b

theorem Ordinal.opow_lt_opow_left_of_succ {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} (ab : a < b) : a ^ Order.succ c < b ^ Order.succ c

theorem Ordinal.opow_add (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) (c : Ordinal.{u_1}) : a ^ (b + c) = a ^ b * a ^ c

theorem Ordinal.opow_one_add (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) : a ^ (1 + b) = a * a ^ b

theorem Ordinal.opow_dvd_opow (a : Ordinal.{u_1}) {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} (h : b ≤ c) : a ^ b ∣ a ^ c

theorem Ordinal.opow_dvd_opow_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} (a1 : 1 < a) : a ^ b ∣ a ^ c ↔ b ≤ c

theorem Ordinal.opow_mul (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) (c : Ordinal.{u_1}) : a ^ (b * c) = (a ^ b) ^ c

Ordinal logarithm

def Ordinal.log (b : Ordinal.{u_1}) (x : Ordinal.{u_1}) : Ordinal.{u_1}

The ordinal logarithm is the solution u to the equation x = b ^ u * v + w where v < b and w < b ^ u.

Equations

• Ordinal.log b x = if _h : 1 < b then (sInf {o : Ordinal.{u_1} | x < b ^ o}).pred else 0

theorem Ordinal.log_nonempty {b : Ordinal.{u_1}} {x : Ordinal.{u_1}} (h : 1 < b) : {o : Ordinal.{u_1} | x < b ^ o}.Nonempty

The set in the definition of log is nonempty.

theorem Ordinal.log_def {b : Ordinal.{u_1}} (h : 1 < b) (x : Ordinal.{u_1}) : Ordinal.log b x = (sInf {o : Ordinal.{u_1} | x < b ^ o}).pred

theorem Ordinal.log_of_not_one_lt_left {b : Ordinal.{u_1}} (h : ¬1 < b) (x : Ordinal.{u_1}) : Ordinal.log b x = 0

theorem Ordinal.log_of_left_le_one {b : Ordinal.{u_1}} (h : b ≤ 1) (x : Ordinal.{u_1}) : Ordinal.log b x = 0

@[simp]

theorem Ordinal.log_zero_left (b : Ordinal.{u_1}) : Ordinal.log 0 b = 0

@[simp]

theorem Ordinal.log_zero_right (b : Ordinal.{u_1}) : Ordinal.log b 0 = 0

@[simp]

theorem Ordinal.log_one_left (b : Ordinal.{u_1}) : Ordinal.log 1 b = 0

theorem Ordinal.succ_log_def {b : Ordinal.{u_1}} {x : Ordinal.{u_1}} (hb : 1 < b) (hx : x ≠ 0) : Order.succ (Ordinal.log b x) = sInf {o : Ordinal.{u_1} | x < b ^ o}

theorem Ordinal.lt_opow_succ_log_self {b : Ordinal.{u_1}} (hb : 1 < b) (x : Ordinal.{u_1}) : x < b ^ Order.succ (Ordinal.log b x)

theorem Ordinal.opow_log_le_self (b : Ordinal.{u_1}) {x : Ordinal.{u_1}} (hx : x ≠ 0) : b ^ Ordinal.log b x ≤ x

theorem Ordinal.opow_le_iff_le_log {b : Ordinal.{u_1}} {x : Ordinal.{u_1}} {c : Ordinal.{u_1}} (hb : 1 < b) (hx : x ≠ 0) : b ^ c ≤ x ↔ c ≤ Ordinal.log b x

opow b and log b (almost) form a Galois connection.

theorem Ordinal.lt_opow_iff_log_lt {b : Ordinal.{u_1}} {x : Ordinal.{u_1}} {c : Ordinal.{u_1}} (hb : 1 < b) (hx : x ≠ 0) : x < b ^ c ↔ Ordinal.log b x < c

theorem Ordinal.log_pos {b : Ordinal.{u_1}} {o : Ordinal.{u_1}} (hb : 1 < b) (ho : o ≠ 0) (hbo : b ≤ o) : 0 < Ordinal.log b o

theorem Ordinal.log_eq_zero {b : Ordinal.{u_1}} {o : Ordinal.{u_1}} (hbo : o < b) : Ordinal.log b o = 0

theorem Ordinal.log_mono_right (b : Ordinal.{u_1}) {x : Ordinal.{u_1}} {y : Ordinal.{u_1}} (xy : x ≤ y) : Ordinal.log b x ≤ Ordinal.log b y

theorem Ordinal.log_le_self (b : Ordinal.{u_1}) (x : Ordinal.{u_1}) : Ordinal.log b x ≤ x

@[simp]

theorem Ordinal.log_one_right (b : Ordinal.{u_1}) : Ordinal.log b 1 = 0

theorem Ordinal.mod_opow_log_lt_self (b : Ordinal.{u_1}) {o : Ordinal.{u_1}} (ho : o ≠ 0) : o % b ^ Ordinal.log b o < o

theorem Ordinal.log_mod_opow_log_lt_log_self {b : Ordinal.{u_1}} {o : Ordinal.{u_1}} (hb : 1 < b) (ho : o ≠ 0) (hbo : b ≤ o) : Ordinal.log b (o % b ^ Ordinal.log b o) < Ordinal.log b o

theorem Ordinal.opow_mul_add_pos {b : Ordinal.{u_1}} {v : Ordinal.{u_1}} (hb : b ≠ 0) (u : Ordinal.{u_1}) (hv : v ≠ 0) (w : Ordinal.{u_1}) : 0 < b ^ u * v + w

theorem Ordinal.opow_mul_add_lt_opow_mul_succ {b : Ordinal.{u_1}} {u : Ordinal.{u_1}} {w : Ordinal.{u_1}} (v : Ordinal.{u_1}) (hw : w < b ^ u) : b ^ u * v + w < b ^ u * Order.succ v

theorem Ordinal.opow_mul_add_lt_opow_succ {b : Ordinal.{u_1}} {u : Ordinal.{u_1}} {v : Ordinal.{u_1}} {w : Ordinal.{u_1}} (hvb : v < b) (hw : w < b ^ u) : b ^ u * v + w < b ^ Order.succ u

theorem Ordinal.log_opow_mul_add {b : Ordinal.{u_1}} {u : Ordinal.{u_1}} {v : Ordinal.{u_1}} {w : Ordinal.{u_1}} (hb : 1 < b) (hv : v ≠ 0) (hvb : v < b) (hw : w < b ^ u) : Ordinal.log b (b ^ u * v + w) = u

theorem Ordinal.log_opow {b : Ordinal.{u_1}} (hb : 1 < b) (x : Ordinal.{u_1}) : Ordinal.log b (b ^ x) = x

theorem Ordinal.div_opow_log_pos (b : Ordinal.{u_1}) {o : Ordinal.{u_1}} (ho : o ≠ 0) : 0 < o / b ^ Ordinal.log b o

theorem Ordinal.div_opow_log_lt {b : Ordinal.{u_1}} (o : Ordinal.{u_1}) (hb : 1 < b) : o / b ^ Ordinal.log b o < b

theorem Ordinal.add_log_le_log_mul {x : Ordinal.{u_1}} {y : Ordinal.{u_1}} (b : Ordinal.{u_1}) (hx : x ≠ 0) (hy : y ≠ 0) : Ordinal.log b x + Ordinal.log b y ≤ Ordinal.log b (x * y)

Interaction with Nat.cast

@[simp]

theorem Ordinal.natCast_opow (m : ℕ) (n : ℕ) : ↑(m ^ n) = ↑m ^ ↑n

@[deprecated Ordinal.natCast_opow]

theorem Ordinal.nat_cast_opow (m : ℕ) (n : ℕ) : ↑(m ^ n) = ↑m ^ ↑n

Alias of Ordinal.natCast_opow.

theorem Ordinal.sup_opow_nat {o : Ordinal.{u_1}} (ho : 0 < o) : (Ordinal.sup fun (n : ℕ) => o ^ ↑n) = o ^ Ordinal.omega