# mathlib3documentation

set_theory.ordinal.exponential

# Ordinal exponential #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

@[protected, instance]
noncomputable def ordinal.has_pow  :

The ordinal exponential, defined by transfinite recursion.

Equations
theorem ordinal.opow_def (a b : ordinal) :
a ^ b = ite (a = 0) (1 - b) (b.limit_rec_on 1 (λ (_x IH : ordinal), IH * a) (λ (b : ordinal) (_x : b.is_limit), b.bsup))
theorem ordinal.zero_opow' (a : ordinal) :
0 ^ a = 1 - a
@[simp]
theorem ordinal.zero_opow {a : ordinal} (a0 : a 0) :
0 ^ a = 0
@[simp]
theorem ordinal.opow_zero (a : ordinal) :
a ^ 0 = 1
@[simp]
theorem ordinal.opow_succ (a b : ordinal) :
a ^ = a ^ b * a
theorem ordinal.opow_limit {a b : ordinal} (a0 : a 0) (h : b.is_limit) :
a ^ b = b.bsup (λ (c : ordinal) (_x : c < b), a ^ c)
theorem ordinal.opow_le_of_limit {a b c : ordinal} (a0 : a 0) (h : b.is_limit) :
a ^ b c (b' : ordinal), b' < b a ^ b' c
theorem ordinal.lt_opow_of_limit {a b c : ordinal} (b0 : b 0) (h : c.is_limit) :
a < b ^ c (c' : ordinal) (H : c' < c), a < b ^ c'
@[simp]
theorem ordinal.opow_one (a : ordinal) :
a ^ 1 = a
@[simp]
theorem ordinal.one_opow (a : ordinal) :
1 ^ a = 1
theorem ordinal.opow_pos {a : ordinal} (b : ordinal) (a0 : 0 < a) :
0 < a ^ b
theorem ordinal.opow_ne_zero {a : ordinal} (b : ordinal) (a0 : a 0) :
a ^ b 0
theorem ordinal.opow_is_normal {a : ordinal} (h : 1 < a) :
ordinal.is_normal (λ (_y : ordinal), a ^ _y)
theorem ordinal.opow_lt_opow_iff_right {a b c : ordinal} (a1 : 1 < a) :
a ^ b < a ^ c b < c
theorem ordinal.opow_le_opow_iff_right {a b c : ordinal} (a1 : 1 < a) :
a ^ b a ^ c b c
theorem ordinal.opow_right_inj {a b c : ordinal} (a1 : 1 < a) :
a ^ b = a ^ c b = c
theorem ordinal.opow_is_limit {a b : ordinal} (a1 : 1 < a) :
theorem ordinal.opow_is_limit_left {a b : ordinal} (l : a.is_limit) (hb : b 0) :
(a ^ b).is_limit
theorem ordinal.opow_le_opow_right {a b c : ordinal} (h₁ : 0 < a) (h₂ : b c) :
a ^ b a ^ c
theorem ordinal.opow_le_opow_left {a b : ordinal} (c : ordinal) (ab : a b) :
a ^ c b ^ c
theorem ordinal.left_le_opow (a : ordinal) {b : ordinal} (b1 : 0 < b) :
a a ^ b
theorem ordinal.right_le_opow {a : ordinal} (b : ordinal) (a1 : 1 < a) :
b a ^ b
theorem ordinal.opow_lt_opow_left_of_succ {a b c : ordinal} (ab : a < b) :
a ^ < b ^
theorem ordinal.opow_add (a b c : ordinal) :
a ^ (b + c) = a ^ b * a ^ c
theorem ordinal.opow_one_add (a b : ordinal) :
a ^ (1 + b) = a * a ^ b
theorem ordinal.opow_dvd_opow (a : ordinal) {b c : ordinal} (h : b c) :
a ^ b a ^ c
theorem ordinal.opow_dvd_opow_iff {a b c : ordinal} (a1 : 1 < a) :
a ^ b a ^ c b c
theorem ordinal.opow_mul (a b c : ordinal) :
a ^ (b * c) = (a ^ b) ^ c

### Ordinal logarithm #

noncomputable def ordinal.log (b x : ordinal) :

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

Equations
theorem ordinal.log_nonempty {b x : ordinal} (h : 1 < b) :
{o : ordinal | x < b ^ o}.nonempty

The set in the definition of log is nonempty.

theorem ordinal.log_def {b : ordinal} (h : 1 < b) (x : ordinal) :
x = (has_Inf.Inf {o : ordinal | x < b ^ o}).pred
theorem ordinal.log_of_not_one_lt_left {b : ordinal} (h : ¬1 < b) (x : ordinal) :
x = 0
theorem ordinal.log_of_left_le_one {b : ordinal} (h : b 1) (x : ordinal) :
x = 0
@[simp]
theorem ordinal.log_zero_left (b : ordinal) :
b = 0
@[simp]
theorem ordinal.log_zero_right (b : ordinal) :
0 = 0
@[simp]
theorem ordinal.log_one_left (b : ordinal) :
b = 0
theorem ordinal.succ_log_def {b x : ordinal} (hb : 1 < b) (hx : x 0) :
order.succ x) = has_Inf.Inf {o : ordinal | x < b ^ o}
theorem ordinal.lt_opow_succ_log_self {b : ordinal} (hb : 1 < b) (x : ordinal) :
x < b ^ order.succ x)
theorem ordinal.opow_log_le_self (b : ordinal) {x : ordinal} (hx : x 0) :
b ^ x x
theorem ordinal.opow_le_iff_le_log {b x c : ordinal} (hb : 1 < b) (hx : x 0) :
b ^ c x c x

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

theorem ordinal.lt_opow_iff_log_lt {b x c : ordinal} (hb : 1 < b) (hx : x 0) :
x < b ^ c x < c
theorem ordinal.log_pos {b o : ordinal} (hb : 1 < b) (ho : o 0) (hbo : b o) :
0 < o
theorem ordinal.log_eq_zero {b o : ordinal} (hbo : o < b) :
o = 0
theorem ordinal.log_mono_right (b : ordinal) {x y : ordinal} (xy : x y) :
x y
theorem ordinal.log_le_self (b x : ordinal) :
x x
@[simp]
theorem ordinal.log_one_right (b : ordinal) :
1 = 0
theorem ordinal.mod_opow_log_lt_self (b : ordinal) {o : ordinal} (ho : o 0) :
o % b ^ o < o
theorem ordinal.log_mod_opow_log_lt_log_self {b o : ordinal} (hb : 1 < b) (ho : o 0) (hbo : b o) :
(o % b ^ o) < o
theorem ordinal.opow_mul_add_pos {b v : ordinal} (hb : b 0) (u : ordinal) (hv : v 0) (w : ordinal) :
0 < b ^ u * v + w
theorem ordinal.opow_mul_add_lt_opow_mul_succ {b u w : ordinal} (v : ordinal) (hw : w < b ^ u) :
b ^ u * v + w < b ^ u *
theorem ordinal.opow_mul_add_lt_opow_succ {b u v w : ordinal} (hvb : v < b) (hw : w < b ^ u) :
b ^ u * v + w < b ^
theorem ordinal.log_opow_mul_add {b u v w : ordinal} (hb : 1 < b) (hv : v 0) (hvb : v < b) (hw : w < b ^ u) :
(b ^ u * v + w) = u
theorem ordinal.log_opow {b : ordinal} (hb : 1 < b) (x : ordinal) :
(b ^ x) = x
theorem ordinal.div_opow_log_pos (b : ordinal) {o : ordinal} (ho : o 0) :
0 < o / b ^ o
theorem ordinal.div_opow_log_lt {b : ordinal} (o : ordinal) (hb : 1 < b) :
o / b ^ o < b
theorem ordinal.add_log_le_log_mul {x y : ordinal} (b : ordinal) (hx : x 0) (hy : y 0) :
x + y (x * y)

### Interaction with nat.cast#

@[simp, norm_cast]
theorem ordinal.nat_cast_opow (m n : ) :
(m ^ n) = m ^ n
theorem ordinal.sup_opow_nat {o : ordinal} (ho : 0 < o) :
ordinal.sup (λ (n : ), o ^ n) =

Extension for the positivity tactic: ordinal.opow takes positive values on positive inputs.