mathlib3 documentation

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.

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

The ordinal exponential, defined by transfinite recursion.

Equations
source
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))
source
theorem ordinal.zero_opow' (a : ordinal) :
0 ^ a = 1 - a
source
@[simp]
theorem ordinal.zero_opow {a : ordinal} (a0 : a ≠ 0) :
0 ^ a = 0
source
@[simp]
theorem ordinal.opow_zero (a : ordinal) :
a ^ 0 = 1
source
@[simp]
theorem ordinal.opow_succ (a b : ordinal) :
a ^ order.succ b = a ^ b * a
source
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)
source
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
source
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'
source
@[simp]
theorem ordinal.opow_one (a : ordinal) :
a ^ 1 = a
source
@[simp]
theorem ordinal.one_opow (a : ordinal) :
1 ^ a = 1
source
theorem ordinal.opow_pos {a : ordinal} (b : ordinal) (a0 : 0 < a) :
0 < a ^ b
source
theorem ordinal.opow_ne_zero {a : ordinal} (b : ordinal) (a0 : a ≠ 0) :
a ^ b ≠ 0
source
theorem ordinal.opow_is_normal {a : ordinal} (h : 1 < a) :
ordinal.is_normal (λ (_y : ordinal), a ^ _y)
source
theorem ordinal.opow_lt_opow_iff_right {a b c : ordinal} (a1 : 1 < a) :
a ^ b < a ^ c ↔ b < c
source
theorem ordinal.opow_le_opow_iff_right {a b c : ordinal} (a1 : 1 < a) :
a ^ b ≤ a ^ c ↔ b ≤ c
source
theorem ordinal.opow_right_inj {a b c : ordinal} (a1 : 1 < a) :
a ^ b = a ^ c ↔ b = c
source
theorem ordinal.opow_is_limit {a b : ordinal} (a1 : 1 < a) :
b.is_limit → (a ^ b).is_limit
source
theorem ordinal.opow_is_limit_left {a b : ordinal} (l : a.is_limit) (hb : b ≠ 0) :
(a ^ b).is_limit
source
theorem ordinal.opow_le_opow_right {a b c : ordinal} (h₁ : 0 < a) (h₂ : b ≤ c) :
a ^ b ≤ a ^ c
source
theorem ordinal.opow_le_opow_left {a b : ordinal} (c : ordinal) (ab : a ≤ b) :
a ^ c ≤ b ^ c
source
theorem ordinal.left_le_opow (a : ordinal) {b : ordinal} (b1 : 0 < b) :
a ≤ a ^ b
source
theorem ordinal.right_le_opow {a : ordinal} (b : ordinal) (a1 : 1 < a) :
b ≤ a ^ b
source
theorem ordinal.opow_lt_opow_left_of_succ {a b c : ordinal} (ab : a < b) :
a ^ order.succ c < b ^ order.succ c
source
theorem ordinal.opow_add (a b c : ordinal) :
a ^ (b + c) = a ^ b * a ^ c
source
theorem ordinal.opow_one_add (a b : ordinal) :
a ^ (1 + b) = a * a ^ b
source
theorem ordinal.opow_dvd_opow (a : ordinal) {b c : ordinal} (h : b ≤ c) :
a ^ b ∣ a ^ c
source
theorem ordinal.opow_dvd_opow_iff {a b c : ordinal} (a1 : 1 < a) :
a ^ b ∣ a ^ c ↔ b ≤ c
source
theorem ordinal.opow_mul (a b c : ordinal) :
a ^ (b * c) = (a ^ b) ^ c

Ordinal logarithm #

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

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

Equations
source
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.

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

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

source
theorem ordinal.lt_opow_iff_log_lt {b x c : ordinal} (hb : 1 < b) (hx : x ≠ 0) :
x < b ^ c ↔ ordinal.log b x < c
source
theorem ordinal.log_pos {b o : ordinal} (hb : 1 < b) (ho : o ≠ 0) (hbo : b ≤ o) :
0 < ordinal.log b o
source
theorem ordinal.log_eq_zero {b o : ordinal} (hbo : o < b) :
ordinal.log b o = 0
source
theorem ordinal.log_mono_right (b : ordinal) {x y : ordinal} (xy : x ≤ y) :
ordinal.log b x ≤ ordinal.log b y
source
theorem ordinal.log_le_self (b x : ordinal) :
ordinal.log b x ≤ x
source
@[simp]
theorem ordinal.log_one_right (b : ordinal) :
ordinal.log b 1 = 0
source
theorem ordinal.mod_opow_log_lt_self (b : ordinal) {o : ordinal} (ho : o ≠ 0) :
o % b ^ ordinal.log b o < o
source
theorem ordinal.log_mod_opow_log_lt_log_self {b o : ordinal} (hb : 1 < b) (ho : o ≠ 0) (hbo : b ≤ o) :
ordinal.log b (o % b ^ ordinal.log b o) < ordinal.log b o
source
theorem ordinal.opow_mul_add_pos {b v : ordinal} (hb : b ≠ 0) (u : ordinal) (hv : v ≠ 0) (w : ordinal) :
0 < b ^ u * v + w
source
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 * order.succ v
source
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 ^ order.succ u
source
theorem ordinal.log_opow_mul_add {b u v w : ordinal} (hb : 1 < b) (hv : v ≠ 0) (hvb : v < b) (hw : w < b ^ u) :
ordinal.log b (b ^ u * v + w) = u
source
theorem ordinal.log_opow {b : ordinal} (hb : 1 < b) (x : ordinal) :
ordinal.log b (b ^ x) = x
source
theorem ordinal.div_opow_log_pos (b : ordinal) {o : ordinal} (ho : o ≠ 0) :
0 < o / b ^ ordinal.log b o
source
theorem ordinal.div_opow_log_lt {b : ordinal} (o : ordinal) (hb : 1 < b) :
o / b ^ ordinal.log b o < b
source
theorem ordinal.add_log_le_log_mul {x y : ordinal} (b : ordinal) (hx : x ≠ 0) (hy : y ≠ 0) :
ordinal.log b x + ordinal.log b y ≤ ordinal.log b (x * y)

Interaction with nat.cast #

source
@[simp, norm_cast]
theorem ordinal.nat_cast_opow (m n : ℕ) :
↑(m ^ n) = ↑m ^ ↑n
source
theorem ordinal.sup_opow_nat {o : ordinal} (ho : 0 < o) :
ordinal.sup (λ (n : ℕ), o ^ ↑n) = o ^ ordinal.omega
source
meta def tactic.positivity_opow  :
expr → tactic tactic.positivity.strictness

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