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

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

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

@[simp]

theorem Ordinal.opow_eq_zero {a : Ordinal.{u_1}} {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) : Ordinal.IsNormal fun (x : Ordinal.{u_1}) => a ^ x

@[deprecated Ordinal.isNormal_opow]

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

Alias of Ordinal.isNormal_opow.

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.isLimit_opow {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (a1 : 1 < a) : b.IsLimit → (a ^ b).IsLimit

@[deprecated Ordinal.isLimit_opow]

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

Alias of Ordinal.isLimit_opow.

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

@[deprecated Ordinal.isLimit_opow_left]

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

Alias of Ordinal.isLimit_opow_left.

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.opow_le_opow {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} {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 : Ordinal.{u_1}} {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 : 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

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

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

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_left_le_one {b : Ordinal.{u_1}} (h : b ≤ 1) (x : Ordinal.{u_1}) : Ordinal.log b x = 0

@[deprecated Ordinal.log_of_left_le_one]

theorem Ordinal.log_of_not_one_lt_left {b : Ordinal.{u_1}} (h : ¬1 < b) (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.

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 : Ordinal.{u_1}} {x : Ordinal.{u_1}} {c : Ordinal.{u_1}} (hb : 1 < b) (hc : c ≠ 0) : b ^ c ≤ x ↔ c ≤ Ordinal.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 : Ordinal.{u_1}} {x : Ordinal.{u_1}} {c : Ordinal.{u_1}} (hb : 1 < b) (h : b ^ c ≤ x) : c ≤ Ordinal.log b x

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

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

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 : Ordinal.{u_1}} {x : Ordinal.{u_1}} {c : Ordinal.{u_1}} (hb : 1 < b) (hc : c ≠ 0) : x < b ^ c ↔ Ordinal.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 : Ordinal.{u_1}} {x : Ordinal.{u_1}} {c : Ordinal.{u_1}} (hb : 1 < b) : Ordinal.log b x < c → x < b ^ c

theorem Ordinal.lt_log_of_lt_opow {b : Ordinal.{u_1}} {x : Ordinal.{u_1}} {c : Ordinal.{u_1}} (hc : c ≠ 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) (hbo : b ≤ o) : Ordinal.log b (o % b ^ Ordinal.log b o) < Ordinal.log b o

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

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) (hw : w < b ^ u) : Ordinal.log b (b ^ u * v + w) = u + Ordinal.log b v

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

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)

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

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

theorem Ordinal.lt_omega0_opow_succ {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} : a < Ordinal.omega0 ^ Order.succ b ↔ ∃ (n : ℕ), a < Ordinal.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 ^ Ordinal.omega0

@[deprecated Ordinal.iSup_pow]

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