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.

source

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

source

theorem Ordinal.zero_opow' (a : Ordinal.{u_1}) :

0 ^ a = 1 - a

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

source

theorem Ordinal.zero_opow_le (a : Ordinal.{u_1}) :

0 ^ a ≤ 1

source

@[simp]

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

0 ^ a = 0

source

@[simp]

theorem Ordinal.opow_zero (a : Ordinal.{u_1}) :

a ^ 0 = 1

source

@[simp]

theorem Ordinal.opow_succ (a b : Ordinal.{u_1}) :

a ^ Order.succ b = a ^ b * a

source

theorem Ordinal.opow_limit {a b : Ordinal.{u_1}} (ha : a ≠ 0) (hb : Order.IsSuccLimit b) :

a ^ b = ⨆ (x : ↑(Set.Iio b)), a ^ ↑x

source

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

source

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

source

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'

source

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

source

@[simp]

theorem Ordinal.opow_one (a : Ordinal.{u_1}) :

a ^ 1 = a

source

@[simp]

theorem Ordinal.one_opow (a : Ordinal.{u_1}) :

1 ^ a = 1

source

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

0 < a ^ b

source

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

a ^ b ≠ 0

source

@[simp]

theorem Ordinal.opow_eq_zero {a b : Ordinal.{u_1}} :

a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

source

@[simp]

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

a ^ ↑n = a ^ n

source

theorem Ordinal.isNormal_opow {a : Ordinal.{u_1}} (h : 1 < a) :

IsNormal fun (x : Ordinal.{u_1}) => a ^ x

source

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

a ^ b < a ^ c ↔ b < c

source

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

a ^ b ≤ a ^ c ↔ b ≤ c

source

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

a ^ b = a ^ c ↔ b = c

source

theorem Ordinal.isSuccLimit_opow {a b : Ordinal.{u_1}} (a1 : 1 < a) :

Order.IsSuccLimit b → Order.IsSuccLimit (a ^ b)

source

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

source

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

Order.IsSuccLimit (a ^ b)

source

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

source

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

a ^ b ≤ a ^ c

source

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

a ^ c ≤ b ^ c

source

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

source

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

a ≤ a ^ b

source

theorem Ordinal.left_lt_opow {a b : Ordinal.{u_1}} (ha : 1 < a) (hb : 1 < b) :

a < a ^ b

source

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

b ≤ a ^ b

source

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

source

theorem Ordinal.opow_add (a b c : Ordinal.{u_1}) :

a ^ (b + c) = a ^ b * a ^ c

source

theorem Ordinal.opow_one_add (a b : Ordinal.{u_1}) :

a ^ (1 + b) = a * a ^ b

source

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

a ^ b ∣ a ^ c

source

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

a ^ b ∣ a ^ c ↔ b ≤ c

source

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

a ^ (b * c) = (a ^ b) ^ c

source

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

source

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

source

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 #

source

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

Instances For

source

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

source

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

log b x = 0

source

@[simp]

theorem Ordinal.log_zero_left (b : Ordinal.{u_1}) :

log 0 b = 0

source

@[simp]

theorem Ordinal.log_zero_right (b : Ordinal.{u_1}) :

log b 0 = 0

source

@[simp]

theorem Ordinal.log_one_left (b : Ordinal.{u_1}) :

log 1 b = 0

source

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}

source

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)

source

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

b ^ log b x ≤ x

source

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.

source

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.

source

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

c ≤ log b x

source

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

b ^ c ≤ x

source

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.

source

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.

source