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
- 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
@[simp]
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)
:
theorem
Ordinal.lt_opow_of_limit
{a : Ordinal.{u_1}}
{b : Ordinal.{u_1}}
{c : Ordinal.{u_1}}
(b0 : b ≠ 0)
(h : c.IsLimit)
:
theorem
Ordinal.opow_isNormal
{a : Ordinal.{u_1}}
(h : 1 < a)
:
Ordinal.IsNormal fun (x : Ordinal.{u_1}) => a ^ x
theorem
Ordinal.opow_lt_opow_iff_right
{a : Ordinal.{u_1}}
{b : Ordinal.{u_1}}
{c : Ordinal.{u_1}}
(a1 : 1 < a)
:
theorem
Ordinal.opow_le_opow_iff_right
{a : Ordinal.{u_1}}
{b : Ordinal.{u_1}}
{c : Ordinal.{u_1}}
(a1 : 1 < a)
:
theorem
Ordinal.opow_right_inj
{a : Ordinal.{u_1}}
{b : Ordinal.{u_1}}
{c : Ordinal.{u_1}}
(a1 : 1 < a)
:
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)
:
theorem
Ordinal.opow_le_opow_left
{a : Ordinal.{u_1}}
{b : Ordinal.{u_1}}
(c : Ordinal.{u_1})
(ab : 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_dvd_opow
(a : Ordinal.{u_1})
{b : Ordinal.{u_1}}
{c : Ordinal.{u_1}}
(h : b ≤ c)
:
theorem
Ordinal.opow_dvd_opow_iff
{a : Ordinal.{u_1}}
{b : Ordinal.{u_1}}
{c : Ordinal.{u_1}}
(a1 : 1 < a)
:
Ordinal logarithm #
The ordinal logarithm is the solution u
to the equation x = b ^ u * v + w
where v < b
and
w < b ^ u
.
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.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_le_iff_le_log
{b : Ordinal.{u_1}}
{x : Ordinal.{u_1}}
{c : Ordinal.{u_1}}
(hb : 1 < b)
(hx : x ≠ 0)
:
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)
:
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_mono_right
(b : Ordinal.{u_1})
{x : Ordinal.{u_1}}
{y : Ordinal.{u_1}}
(xy : x ≤ y)
:
b.log x ≤ b.log y
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)
:
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})
:
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)
:
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)
:
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)
:
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)
:
theorem
Ordinal.sup_opow_nat
{o : Ordinal.{u_1}}
(ho : 0 < o)
:
(Ordinal.sup fun (n : ℕ) => o ^ ↑n) = o ^ Ordinal.omega