# 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 :

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 ^ = 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_natCast (a : Ordinal.{u_1}) (n : ) :
a ^ n = a ^ n
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_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 #

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
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}) :
= (sInf {o : Ordinal.{u_1} | x < b ^ o}).pred
@[simp]
@[simp]
@[simp]
theorem Ordinal.succ_log_def {b : Ordinal.{u_1}} {x : Ordinal.{u_1}} (hb : 1 < b) (hx : x 0) :
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

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 < c
theorem Ordinal.log_pos {b : Ordinal.{u_1}} {o : Ordinal.{u_1}} (hb : 1 < b) (ho : o 0) (hbo : b o) :
0 <
theorem Ordinal.log_eq_zero {b : Ordinal.{u_1}} {o : Ordinal.{u_1}} (hbo : o < b) :
= 0
@[simp]
theorem Ordinal.mod_opow_log_lt_self (b : Ordinal.{u_1}) {o : Ordinal.{u_1}} (ho : o 0) :
o % b ^ < 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 ^ ) <
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 *
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 ^
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 ^
theorem Ordinal.div_opow_log_lt {b : Ordinal.{u_1}} (o : Ordinal.{u_1}) (hb : 1 < b) :
o / b ^ < 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 * 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) =