Documentation

Mathlib.SetTheory.Ordinal.Exponential

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.

The ordinal exponential, defined by transfinite recursion.

Equations
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
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}) :
    b.log x = (sInf {o : Ordinal.{u_1} | x < b ^ o}).pred
    theorem Ordinal.log_of_not_one_lt_left {b : Ordinal.{u_1}} (h : ¬1 < b) (x : Ordinal.{u_1}) :
    b.log x = 0
    theorem Ordinal.log_of_left_le_one {b : Ordinal.{u_1}} (h : b 1) (x : Ordinal.{u_1}) :
    b.log x = 0
    @[simp]
    theorem Ordinal.log_zero_right (b : Ordinal.{u_1}) :
    b.log 0 = 0
    theorem Ordinal.succ_log_def {b : Ordinal.{u_1}} {x : Ordinal.{u_1}} (hb : 1 < b) (hx : x 0) :
    Order.succ (b.log 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 (b.log x)
    theorem Ordinal.opow_log_le_self (b : Ordinal.{u_1}) {x : Ordinal.{u_1}} (hx : x 0) :
    b ^ b.log 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 b.log x

    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 b.log x < c
    theorem Ordinal.log_pos {b : Ordinal.{u_1}} {o : Ordinal.{u_1}} (hb : 1 < b) (ho : o 0) (hbo : b o) :
    0 < b.log o
    theorem Ordinal.log_eq_zero {b : Ordinal.{u_1}} {o : Ordinal.{u_1}} (hbo : o < b) :
    b.log o = 0
    theorem Ordinal.log_mono_right (b : Ordinal.{u_1}) {x : Ordinal.{u_1}} {y : Ordinal.{u_1}} (xy : x y) :
    b.log x b.log y
    @[simp]
    theorem Ordinal.log_one_right (b : Ordinal.{u_1}) :
    b.log 1 = 0
    theorem Ordinal.mod_opow_log_lt_self (b : Ordinal.{u_1}) {o : Ordinal.{u_1}} (ho : o 0) :
    o % b ^ b.log o < 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) :
    b.log (o % b ^ b.log o) < b.log o
    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_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
    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) :
    b.log (b ^ u * v + w) = u
    theorem Ordinal.log_opow {b : Ordinal.{u_1}} (hb : 1 < b) (x : Ordinal.{u_1}) :
    b.log (b ^ x) = x
    theorem Ordinal.div_opow_log_pos (b : Ordinal.{u_1}) {o : Ordinal.{u_1}} (ho : o 0) :
    0 < o / b ^ b.log o
    theorem Ordinal.div_opow_log_lt {b : Ordinal.{u_1}} (o : Ordinal.{u_1}) (hb : 1 < b) :
    o / b ^ b.log 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) :
    b.log x + b.log y b.log (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) = o ^ Ordinal.omega