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.instPow : Pow Ordinal.{u_1} Ordinal.{u_1}

The ordinal exponential, defined by transfinite recursion.

We call this opow in theorems in order to disambiguate from other exponentials.

Equations

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

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

0 ^ a = 1 if a = 0 and 0 ^ a = 0 otherwise.

theorem Ordinal.zero_opow_le (a : Ordinal.{u_1}) : 0 ^ a ≤ 1

@[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 b : Ordinal.{u_1}) : a ^ Order.succ b = a ^ b * a

theorem Ordinal.opow_limit {a b : Ordinal.{u_1}} (ha : a ≠ 0) (hb : Order.IsSuccLimit b) : a ^ b = ⨆ (x : ↑(Set.Iio b)), a ^ ↑x

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

@[deprecated Ordinal.opow_le_of_isSuccLimit (since := "2025-07-08")]

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

Alias of Ordinal.opow_le_of_isSuccLimit.

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

@[deprecated Ordinal.lt_opow_of_isSuccLimit (since := "2025-07-08")]

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

Alias of Ordinal.lt_opow_of_isSuccLimit.

@[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

@[simp]

theorem Ordinal.opow_eq_zero {a b : Ordinal.{u_1}} : a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

@[simp]

theorem Ordinal.opow_natCast (a : Ordinal.{u_1}) (n : ℕ) : a ^ ↑n = a ^ n

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Ordinal.isSuccLimit_opow {a b : Ordinal.{u_1}} (a1 : 1 < a) : Order.IsSuccLimit b → Order.IsSuccLimit (a ^ b)

@[deprecated Ordinal.isSuccLimit_opow (since := "2025-07-08")]

theorem Ordinal.isLimit_opow {a b : Ordinal.{u_1}} (a1 : 1 < a) : Order.IsSuccLimit b → Order.IsSuccLimit (a ^ b)

Alias of Ordinal.isSuccLimit_opow.

theorem Ordinal.isSuccLimit_opow_left {a b : Ordinal.{u_1}} (l : Order.IsSuccLimit a) (hb : b ≠ 0) : Order.IsSuccLimit (a ^ b)

@[deprecated Ordinal.isSuccLimit_opow_left (since := "2025-07-08")]

theorem Ordinal.isLimit_opow_left {a b : Ordinal.{u_1}} (l : Order.IsSuccLimit a) (hb : b ≠ 0) : Order.IsSuccLimit (a ^ b)

Alias of Ordinal.isSuccLimit_opow_left.

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

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

theorem Ordinal.opow_le_opow {a b c d : Ordinal.{u_1}} (hac : a ≤ c) (hbd : b ≤ d) (hc : 0 < c) : a ^ b ≤ c ^ d

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

theorem Ordinal.left_lt_opow {a b : Ordinal.{u_1}} (ha : 1 < a) (hb : 1 < 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 b c : Ordinal.{u_1}} (ab : a < b) : a ^ Order.succ c < b ^ Order.succ c

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

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

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

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

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

theorem Ordinal.opow_mul_add_pos {b 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 {b u w x v : Ordinal.{u_1}} (hw : w < b ^ u) (hv : v < x) : b ^ u * v + w < b ^ u * x

@[deprecated Ordinal.opow_mul_add_lt_opow_mul (since := "2025-08-27")]

theorem Ordinal.opow_mul_add_lt_opow_mul_succ {b u 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 {b u v w x : Ordinal.{u_1}} (hv : v < b) (hw : w < b ^ u) (hu : u < x) : b ^ u * v + w < b ^ x

@[deprecated Ordinal.opow_mul_add_lt_opow_succ (since := "2025-08-27")]

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

Ordinal logarithm

def Ordinal.log (b 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 1 < b then (sInf {o : Ordinal.{?u.11} | x < b ^ o}).pred else 0

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

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Ordinal.succ_log_def {b x : Ordinal.{u_1}} (hb : 1 < b) (hx : x ≠ 0) : Order.succ (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 (log b x)

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

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

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

See opow_le_iff_le_log' for a variant assuming c ≠ 0 rather than x ≠ 0. See also le_log_of_opow_le and opow_le_of_le_log, which are both separate implications under weaker assumptions.

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

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

See opow_le_iff_le_log for a variant assuming x ≠ 0 rather than c ≠ 0. See also le_log_of_opow_le and opow_le_of_le_log, which are both separate implications under weaker assumptions.

theorem Ordinal.le_log_of_opow_le {b x c : Ordinal.{u_1}} (hb : 1 < b) (h : b ^ c ≤ x) : c ≤ log b x

theorem Ordinal.opow_le_of_le_log {b x c : Ordinal.{u_1}} (hc : c ≠ 0) (h : c ≤ log b x) : b ^ c ≤ x

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

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

See lt_opow_iff_log_lt' for a variant assuming c ≠ 0 rather than x ≠ 0. See also lt_opow_of_log_lt and lt_log_of_lt_opow, which are both separate implications under weaker assumptions.

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

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

See lt_opow_iff_log_lt for a variant assuming x ≠ 0 rather than c ≠ 0. See also lt_opow_of_log_lt and lt_log_of_lt_opow, which are both separate implications under weaker assumptions.

theorem Ordinal.lt_opow_of_log_lt {b x c : Ordinal.{u_1}} (hb : 1 < b) : log b x < c → x < b ^ c

theorem Ordinal.lt_log_of_lt_opow {b x c : Ordinal.{u_1}} (hc : c ≠ 0) : x < b ^ c → log b x < c

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

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

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

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

@[simp]

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

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

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

theorem Ordinal.log_eq_iff {b x : Ordinal.{u_1}} (hb : 1 < b) (hx : x ≠ 0) (y : Ordinal.{u_1}) : log b x = y ↔ b ^ y ≤ x ∧ x < b ^ Order.succ y

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

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

theorem Ordinal.log_opow {b : Ordinal.{u_1}} (hb : 1 < b) (x : Ordinal.{u_1}) : 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 ^ log b o

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

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

theorem Ordinal.omega0_opow_mul_nat_lt {a b : Ordinal.{u_1}} (h : a < b) (n : ℕ) : omega0 ^ a * ↑n < omega0 ^ b

theorem Ordinal.lt_omega0_opow {a b : Ordinal.{u_1}} (hb : b ≠ 0) : a < omega0 ^ b ↔ ∃ c < b, ∃ (n : ℕ), a < omega0 ^ c * ↑n

theorem Ordinal.lt_omega0_opow_succ {a b : Ordinal.{u_1}} : a < omega0 ^ Order.succ b ↔ ∃ (n : ℕ), a < omega0 ^ b * ↑n

Interaction with Nat.cast

@[simp]

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

theorem Ordinal.iSup_pow {o : Ordinal.{u_1}} (ho : 0 < o) : ⨆ (n : ℕ), o ^ n = o ^ omega0