Mathlib.SetTheory.Ordinal.Exponential

Ordinal.instPow instance

: Pow Ordinal Ordinal

Full source

/-- The ordinal exponential, defined by transfinite recursion.

We call this `opow` in theorems in order to disambiguate from other exponentials. -/
instance instPow : Pow Ordinal Ordinal :=
  ⟨fun a b ↦ if a = 0 then 1 - b else
    limitRecOn b 1 (fun _ x ↦ x * a) fun o _ f ↦ ⨆ x : Iio o, f x.1 x.2⟩

Ordinal Exponentiation Operation

Informal description

The type of ordinals `Ordinal` is equipped with a power operation $a^b$ defined by transfinite recursion, where $a$ and $b$ are ordinals. This operation satisfies the properties of ordinal exponentiation, including: 1. $a^0 = 1$ for any ordinal $a$ 2. $a^{b+1} = a^b \cdot a$ for successor ordinals $b+1$ 3. $a^b = \bigsqcup_{c < b} a^c$ for limit ordinals $b$ The power operation is related to the logarithm function via the property $b^c \leq x \leftrightarrow c \leq \log_b x$ for nontrivial inputs $b$ and $c$.

Ordinal.zero_opow' theorem

(a : Ordinal) : 0 ^ a = 1 - a

Full source

/-- `0 ^ a = 1` if `a = 0` and `0 ^ a = 0` otherwise. -/
theorem zero_opow' (a : Ordinal) : 0 ^ a = 1 - a :=
  if_pos rfl

Exponentiation of Zero Ordinal: $0^a = 1 - a$

Informal description

For any ordinal $a$, the ordinal exponentiation $0^a$ equals $1 - a$, where $1$ is the ordinal one and $-$ denotes ordinal subtraction.

Ordinal.zero_opow_le theorem

(a : Ordinal) : (0 : Ordinal) ^ a ≤ 1

Full source

theorem zero_opow_le (a : Ordinal) : (0 : Ordinal) ^ a ≤ 1 := by
  rw [zero_opow']
  exact sub_le_self 1 a

Inequality for Zero Exponentiation: $0^a \leq 1$

Informal description

For any ordinal $a$, the ordinal exponentiation $0^a$ is less than or equal to $1$.

Ordinal.zero_opow theorem

{a : Ordinal} (a0 : a ≠ 0) : (0 : Ordinal) ^ a = 0

Full source

@[simp]
theorem zero_opow {a : Ordinal} (a0 : a ≠ 0) : (0 : Ordinal) ^ a = 0 := by
  rwa [zero_opow', Ordinal.sub_eq_zero_iff_le, one_le_iff_ne_zero]

Zero to a Nonzero Ordinal Power is Zero: $0^a = 0$ for $a \neq 0$

Informal description

For any nonzero ordinal $a$, the ordinal exponentiation $0^a$ equals $0$.

Ordinal.opow_zero theorem

(a : Ordinal) : a ^ (0 : Ordinal) = 1

Full source

@[simp]
theorem opow_zero (a : Ordinal) : a ^ (0 : Ordinal) = 1 := by
  obtain rfl | h := eq_or_ne a 0
  · rw [zero_opow', Ordinal.sub_zero]
  · rw [opow_of_ne_zero h, limitRecOn_zero]

Exponentiation of Ordinals: $a^0 = 1$

Informal description

For any ordinal $a$, the exponentiation $a^0$ equals the ordinal $1$.

Ordinal.opow_succ theorem

(a b : Ordinal) : a ^ succ b = a ^ b * a

Full source

@[simp]
theorem opow_succ (a b : Ordinal) : a ^ succ b = a ^ b * a := by
  obtain rfl | h := eq_or_ne a 0
  · rw [zero_opow (succ_ne_zero b), mul_zero]
  · rw [opow_of_ne_zero h, opow_of_ne_zero h, limitRecOn_succ]

Successor Ordinal Exponentiation: $a^{b+1} = a^b \cdot a$

Informal description

For any ordinals $a$ and $b$, the exponentiation $a^{\mathrm{succ}(b)}$ equals $a^b \cdot a$, where $\mathrm{succ}(b)$ denotes the successor ordinal of $b$.

Ordinal.opow_limit theorem

{a b : Ordinal} (ha : a ≠ 0) (hb : IsLimit b) : a ^ b = ⨆ x : Iio b, a ^ x.1

Full source

theorem opow_limit {a b : Ordinal} (ha : a ≠ 0) (hb : IsLimit b) :
    a ^ b = ⨆ x : Iio b, a ^ x.1 := by
  simp_rw [opow_of_ne_zero ha, limitRecOn_limit _ _ _ _ hb]

Limit Ordinal Exponentiation as Supremum of Smaller Exponents

Informal description

For any nonzero ordinal $a$ and any limit ordinal $b$, the ordinal exponentiation $a^b$ equals the supremum of $a^{b'}$ for all $b' < b$. That is, \[ a^b = \bigsqcup_{b' < b} a^{b'}. \]

Ordinal.opow_le_of_limit theorem

{a b c : Ordinal} (a0 : a ≠ 0) (h : IsLimit b) : a ^ b ≤ c ↔ ∀ b' < b, a ^ b' ≤ c

Full source

theorem opow_le_of_limit {a b c : Ordinal} (a0 : a ≠ 0) (h : IsLimit b) :
    a ^ b ≤ c ↔ ∀ b' < b, a ^ b' ≤ c := by
  rw [opow_limit a0 h, Ordinal.iSup_le_iff, Subtype.forall]
  rfl

Limit Ordinal Exponentiation Inequality Characterization: $a^b \leq c \leftrightarrow \forall b' < b, a^{b'} \leq c$

Informal description

For any nonzero ordinal $a$, limit ordinal $b$, and ordinal $c$, the inequality $a^b \leq c$ holds if and only if for every ordinal $b' < b$, we have $a^{b'} \leq c$.

Ordinal.lt_opow_of_limit theorem

{a b c : Ordinal} (b0 : b ≠ 0) (h : IsLimit c) : a < b ^ c ↔ ∃ c' < c, a < b ^ c'

Full source

theorem lt_opow_of_limit {a b c : Ordinal} (b0 : b ≠ 0) (h : IsLimit c) :
    a < b ^ c ↔ ∃ c' < c, a < b ^ c' := by
  rw [← not_iff_not, not_exists]
  simp only [not_lt, opow_le_of_limit b0 h, exists_prop, not_and]

Characterization of Inequality under Limit Ordinal Exponentiation: $a < b^c \leftrightarrow \exists c' < c, a < b^{c'}$

Informal description

For any ordinals $a$, $b \neq 0$, and limit ordinal $c$, the inequality $a < b^c$ holds if and only if there exists an ordinal $c' < c$ such that $a < b^{c'}$.

Ordinal.opow_one theorem

(a : Ordinal) : a ^ (1 : Ordinal) = a

Full source

@[simp]
theorem opow_one (a : Ordinal) : a ^ (1 : Ordinal) = a := by
  rw [← succ_zero, opow_succ]
  simp only [opow_zero, one_mul]

Exponentiation of Ordinals: $a^1 = a$

Informal description

For any ordinal $a$, the exponentiation $a^1$ equals $a$.

Ordinal.one_opow theorem

(a : Ordinal) : (1 : Ordinal) ^ a = 1

Full source

@[simp]
theorem one_opow (a : Ordinal) : (1 : Ordinal) ^ a = 1 := by
  induction a using limitRecOn with
  | zero => simp only [opow_zero]
  | succ _ ih =>
    simp only [opow_succ, ih, mul_one]
  | isLimit b l IH =>
    refine eq_of_forall_ge_iff fun c => ?_
    rw [opow_le_of_limit Ordinal.one_ne_zero l]
    exact ⟨fun H => by simpa only [opow_zero] using H 0 l.pos, fun H b' h => by rwa [IH _ h]⟩

Exponentiation Identity: $1^a = 1$ for All Ordinals $a$

Informal description

For any ordinal $a$, the exponentiation of the ordinal $1$ to the power of $a$ equals $1$, i.e., $1^a = 1$.

Ordinal.opow_pos theorem

{a : Ordinal} (b : Ordinal) (a0 : 0 < a) : 0 < a ^ b

Full source

theorem opow_pos {a : Ordinal} (b : Ordinal) (a0 : 0 < a) : 0 < a ^ b := by
  have h0 : 0 < a ^ (0 : Ordinal) := by simp only [opow_zero, zero_lt_one]
  induction b using limitRecOn with
  | zero => exact h0
  | succ b IH =>
    rw [opow_succ]
    exact mul_pos IH a0
  | isLimit b l _ =>
    exact (lt_opow_of_limit (Ordinal.pos_iff_ne_zero.1 a0) l).2 ⟨0, l.pos, h0⟩

Positivity of Ordinal Exponentiation: $0 < a^b$ when $0 < a$

Informal description

For any ordinals $a$ and $b$, if $0 < a$, then $0 < a^b$.

Ordinal.opow_ne_zero theorem

{a : Ordinal} (b : Ordinal) (a0 : a ≠ 0) : a ^ b ≠ 0

Full source

theorem opow_ne_zero {a : Ordinal} (b : Ordinal) (a0 : a ≠ 0) : a ^ b ≠ 0 :=
  Ordinal.pos_iff_ne_zero.1 <| opow_pos b <| Ordinal.pos_iff_ne_zero.2 a0

Non-Zero Property of Ordinal Exponentiation: $a^b \neq 0$ when $a \neq 0$

Informal description

For any ordinals $a$ and $b$, if $a \neq 0$, then the ordinal exponentiation $a^b$ is not equal to $0$.

Ordinal.opow_eq_zero theorem

{a b : Ordinal} : a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

Full source

@[simp]
theorem opow_eq_zero {a b : Ordinal} : a ^ b = 0 ↔ a = 0 ∧ b ≠ 0 := by
  obtain rfl | ha := eq_or_ne a 0
  · obtain rfl | hb := eq_or_ne b 0
    · simp
    · simp [hb]
  · simp [opow_ne_zero b ha, ha]

Characterization of Zero in Ordinal Exponentiation: $a^b = 0 \leftrightarrow (a = 0 \land b \neq 0)$

Informal description

For any ordinals $a$ and $b$, the exponentiation $a^b$ equals $0$ if and only if $a = 0$ and $b \neq 0$.

Ordinal.opow_natCast theorem

(a : Ordinal) (n : ℕ) : a ^ (n : Ordinal) = a ^ n

Full source

@[simp, norm_cast]
theorem opow_natCast (a : Ordinal) (n : ℕ) : a ^ (n : Ordinal) = a ^ n := by
  induction n with
  | zero => rw [Nat.cast_zero, opow_zero, pow_zero]
  | succ n IH => rw [Nat.cast_succ, add_one_eq_succ, opow_succ, pow_succ, IH]

Ordinal Exponentiation of Natural Number Cast: $a^{(n : \text{Ordinal})} = a^n$

Informal description

For any ordinal $a$ and natural number $n$, the ordinal exponentiation $a^{(n : \text{Ordinal})}$ is equal to the $n$-fold ordinal power $a^n$.

Ordinal.isNormal_opow theorem

{a : Ordinal} (h : 1 < a) : IsNormal (a ^ ·)

Full source

theorem isNormal_opow {a : Ordinal} (h : 1 < a) : IsNormal (a ^ ·) :=
  have a0 : 0 < a := zero_lt_one.trans h
  ⟨fun b => by simpa only [mul_one, opow_succ] using (mul_lt_mul_iff_left (opow_pos b a0)).2 h,
    fun _ l _ => opow_le_of_limit (ne_of_gt a0) l⟩

Normality of Ordinal Exponentiation for Base $a > 1$

Informal description

For any ordinal $a > 1$, the exponential function $b \mapsto a^b$ is a normal function on ordinals. That is: 1. It is strictly increasing: for every ordinal $b$, $a^b < a^{\text{succ } b}$. 2. It is order-continuous: for every limit ordinal $b$, $a^b = \bigsqcup_{c < b} a^c$.

Ordinal.opow_lt_opow_iff_right theorem

{a b c : Ordinal} (a1 : 1 < a) : a ^ b < a ^ c ↔ b < c

Full source

theorem opow_lt_opow_iff_right {a b c : Ordinal} (a1 : 1 < a) : a ^ b < a ^ c ↔ b < c :=
  (isNormal_opow a1).lt_iff

Strict Monotonicity of Ordinal Exponentiation: $a^b < a^c \leftrightarrow b < c$ for $a > 1$

Informal description

For ordinals $a > 1$, $b$, and $c$, the inequality $a^b < a^c$ holds if and only if $b < c$.

Ordinal.opow_le_opow_iff_right theorem

{a b c : Ordinal} (a1 : 1 < a) : a ^ b ≤ a ^ c ↔ b ≤ c

Full source

theorem opow_le_opow_iff_right {a b c : Ordinal} (a1 : 1 < a) : a ^ b ≤ a ^ c ↔ b ≤ c :=
  (isNormal_opow a1).le_iff

Monotonicity of Ordinal Exponentiation: $a^b \leq a^c \leftrightarrow b \leq c$ for $a > 1$

Informal description

For ordinals $a > 1$, $b$, and $c$, the inequality $a^b \leq a^c$ holds if and only if $b \leq c$.

Ordinal.opow_right_inj theorem

{a b c : Ordinal} (a1 : 1 < a) : a ^ b = a ^ c ↔ b = c

Full source

theorem opow_right_inj {a b c : Ordinal} (a1 : 1 < a) : a ^ b = a ^ c ↔ b = c :=
  (isNormal_opow a1).inj

Injective Property of Ordinal Exponentiation: $a^b = a^c \leftrightarrow b = c$ for $a > 1$

Informal description

For ordinals $a > 1$, $b$, and $c$, the equality $a^b = a^c$ holds if and only if $b = c$.

Ordinal.isLimit_opow theorem

{a b : Ordinal} (a1 : 1 < a) : IsLimit b → IsLimit (a ^ b)

Full source

theorem isLimit_opow {a b : Ordinal} (a1 : 1 < a) : IsLimit b → IsLimit (a ^ b) :=
  (isNormal_opow a1).isLimit

Limit ordinal property of exponentiation: $a^b$ is limit when $b$ is limit and $a > 1$

Informal description

For any ordinals $a > 1$ and $b$, if $b$ is a limit ordinal, then the ordinal power $a^b$ is also a limit ordinal.

Ordinal.isLimit_opow_left theorem

{a b : Ordinal} (l : IsLimit a) (hb : b ≠ 0) : IsLimit (a ^ b)

Full source

theorem isLimit_opow_left {a b : Ordinal} (l : IsLimit a) (hb : b ≠ 0) : IsLimit (a ^ b) := by
  rcases zero_or_succ_or_limit b with (e | ⟨b, rfl⟩ | l')
  · exact absurd e hb
  · rw [opow_succ]
    exact isLimit_mul (opow_pos _ l.pos) l
  · exact isLimit_opow l.one_lt l'

Limit Ordinal Property of Exponentiation: $a^b$ is limit when $a$ is limit and $b \neq 0$

Informal description

For any ordinals $a$ and $b$, if $a$ is a limit ordinal and $b \neq 0$, then the ordinal power $a^b$ is also a limit ordinal.

Ordinal.opow_le_opow_right theorem

{a b c : Ordinal} (h₁ : 0 < a) (h₂ : b ≤ c) : a ^ b ≤ a ^ c

Full source

theorem opow_le_opow_right {a b c : Ordinal} (h₁ : 0 < a) (h₂ : b ≤ c) : a ^ b ≤ a ^ c := by
  rcases lt_or_eq_of_le (one_le_iff_pos.2 h₁) with h₁ | h₁
  · exact (opow_le_opow_iff_right h₁).2 h₂
  · subst a
    -- Porting note: `le_refl` is required.
    simp only [one_opow, le_refl]

Monotonicity of Ordinal Exponentiation in the Exponent: $a^b \leq a^c$ for $a > 0$ and $b \leq c$

Informal description

For any ordinals $a > 0$, $b$, and $c$ such that $b \leq c$, the inequality $a^b \leq a^c$ holds.

Ordinal.opow_le_opow_left theorem

{a b : Ordinal} (c : Ordinal) (ab : a ≤ b) : a ^ c ≤ b ^ c

Full source

theorem opow_le_opow_left {a b : Ordinal} (c : Ordinal) (ab : a ≤ b) : a ^ c ≤ b ^ c := by
  by_cases a0 : a = 0
  -- Porting note: `le_refl` is required.
  · subst a
    by_cases c0 : c = 0
    · subst c
      simp only [opow_zero, le_refl]
    · simp only [zero_opow c0, Ordinal.zero_le]
  · induction c using limitRecOn with
    | zero => simp only [opow_zero, le_refl]
    | succ c IH =>
      simpa only [opow_succ] using mul_le_mul' IH ab
    | isLimit c l IH =>
      exact
        (opow_le_of_limit a0 l).2 fun b' h =>
          (IH _ h).trans (opow_le_opow_right ((Ordinal.pos_iff_ne_zero.2 a0).trans_le ab) h.le)

Monotonicity of Ordinal Exponentiation in the Base: $a^c \leq b^c$ when $a \leq b$

Informal description

For any ordinals $a$, $b$, and $c$, if $a \leq b$, then $a^c \leq b^c$.

Ordinal.opow_le_opow theorem

{a b c d : Ordinal} (hac : a ≤ c) (hbd : b ≤ d) (hc : 0 < c) : a ^ b ≤ c ^ d

Full source

theorem opow_le_opow {a b c d : Ordinal} (hac : a ≤ c) (hbd : b ≤ d) (hc : 0 < c) : a ^ b ≤ c ^ d :=
  (opow_le_opow_left b hac).trans (opow_le_opow_right hc hbd)

Monotonicity of Ordinal Exponentiation: $a^b \leq c^d$ under $a \leq c$, $b \leq d$, and $c > 0$

Informal description

For any ordinals $a, b, c, d$ such that $a \leq c$, $b \leq d$, and $c > 0$, we have $a^b \leq c^d$.

Ordinal.left_le_opow theorem

(a : Ordinal) {b : Ordinal} (b1 : 0 < b) : a ≤ a ^ b

Full source

theorem left_le_opow (a : Ordinal) {b : Ordinal} (b1 : 0 < b) : a ≤ a ^ b := by
  nth_rw 1 [← opow_one a]
  rcases le_or_gt a 1 with a1 | a1
  · rcases lt_or_eq_of_le a1 with a0 | a1
    · rw [lt_one_iff_zero] at a0
      rw [a0, zero_opow Ordinal.one_ne_zero]
      exact Ordinal.zero_le _
    rw [a1, one_opow, one_opow]
  rwa [opow_le_opow_iff_right a1, one_le_iff_pos]

Monotonicity of Ordinal Exponentiation: $a \leq a^b$ for $b > 0$

Informal description

For any ordinal $a$ and any positive ordinal $b$ (i.e., $b > 0$), we have $a \leq a^b$.

Ordinal.left_lt_opow theorem

{a b : Ordinal} (ha : 1 < a) (hb : 1 < b) : a < a ^ b

Full source

theorem left_lt_opow {a b : Ordinal} (ha : 1 < a) (hb : 1 < b) : a < a ^ b := by
  conv_lhs => rw [← opow_one a]
  rwa [opow_lt_opow_iff_right ha]

Strict Growth of Ordinal Exponentiation: $a < a^b$ for $a, b > 1$

Informal description

For any ordinals $a > 1$ and $b > 1$, the exponentiation satisfies $a < a^b$.

Ordinal.right_le_opow theorem

{a : Ordinal} (b : Ordinal) (a1 : 1 < a) : b ≤ a ^ b

Full source

theorem right_le_opow {a : Ordinal} (b : Ordinal) (a1 : 1 < a) : b ≤ a ^ b :=
  (isNormal_opow a1).le_apply

Ordinal exponentiation dominates identity for base $a > 1$

Informal description

For any ordinal $b$ and any ordinal $a > 1$, we have $b \leq a^b$.

Ordinal.opow_lt_opow_left_of_succ theorem

{a b c : Ordinal} (ab : a < b) : a ^ succ c < b ^ succ c

Full source

theorem opow_lt_opow_left_of_succ {a b c : Ordinal} (ab : a < b) : a ^ succ c < b ^ succ c := by
  rw [opow_succ, opow_succ]
  exact
    (mul_le_mul_right' (opow_le_opow_left c ab.le) a).trans_lt
      (mul_lt_mul_of_pos_left ab (opow_pos c ((Ordinal.zero_le a).trans_lt ab)))

Strict Monotonicity of Ordinal Exponentiation in Base for Successor Exponents: $a^{c+1} < b^{c+1}$ when $a < b$

Informal description

For any ordinals $a$, $b$, and $c$, if $a < b$, then $a^{c+1} < b^{c+1}$, where $c+1$ denotes the successor ordinal of $c$.

Ordinal.opow_add theorem

(a b c : Ordinal) : a ^ (b + c) = a ^ b * a ^ c

Full source

theorem opow_add (a b c : Ordinal) : a ^ (b + c) = a ^ b * a ^ c := by
  rcases eq_or_ne a 0 with (rfl | a0)
  · rcases eq_or_ne c 0 with (rfl | c0)
    · simp
    have : b + c ≠ 0 := ((Ordinal.pos_iff_ne_zero.2 c0).trans_le (le_add_left _ _)).ne'
    simp only [zero_opow c0, zero_opow this, mul_zero]
  rcases eq_or_lt_of_le (one_le_iff_ne_zero.2 a0) with (rfl | a1)
  · simp only [one_opow, mul_one]
  induction c using limitRecOn with
  | zero => simp
  | succ c IH =>
    rw [add_succ, opow_succ, IH, opow_succ, mul_assoc]
  | isLimit c l IH =>
    refine
      eq_of_forall_ge_iff fun d =>
        (((isNormal_opow a1).trans (isNormal_add_right b)).limit_le l).trans ?_
    dsimp only [Function.comp_def]
    simp +contextual only [IH]
    exact
      (((isNormal_mul_right <| opow_pos b (Ordinal.pos_iff_ne_zero.2 a0)).trans
              (isNormal_opow a1)).limit_le
          l).symm

Exponentiation Law for Ordinals: $a^{b + c} = a^b \cdot a^c$

Informal description

For any ordinals $a$, $b$, and $c$, the exponentiation $a^{b + c}$ equals the product $a^b \cdot a^c$.

Ordinal.opow_one_add theorem

(a b : Ordinal) : a ^ (1 + b) = a * a ^ b

Full source

theorem opow_one_add (a b : Ordinal) : a ^ (1 + b) = a * a ^ b := by rw [opow_add, opow_one]

Exponentiation Identity for Ordinals: $a^{1 + b} = a \cdot a^b$

Informal description

For any ordinals $a$ and $b$, the exponentiation $a^{1 + b}$ equals the product $a \cdot a^b$.

Ordinal.opow_dvd_opow theorem

(a : Ordinal) {b c : Ordinal} (h : b ≤ c) : a ^ b ∣ a ^ c

Full source

theorem opow_dvd_opow (a : Ordinal) {b c : Ordinal} (h : b ≤ c) : a ^ b ∣ a ^ c :=
  ⟨a ^ (c - b), by rw [← opow_add, Ordinal.add_sub_cancel_of_le h]⟩

Divisibility of Ordinal Powers: $a^b \mid a^c$ when $b \leq c$

Informal description

For any ordinals $a$, $b$, and $c$ with $b \leq c$, the ordinal power $a^b$ divides $a^c$.

Ordinal.opow_dvd_opow_iff theorem

{a b c : Ordinal} (a1 : 1 < a) : a ^ b ∣ a ^ c ↔ b ≤ c

Full source

theorem opow_dvd_opow_iff {a b c : Ordinal} (a1 : 1 < a) : a ^ b ∣ a ^ ca ^ b ∣ a ^ c ↔ b ≤ c :=
  ⟨fun h =>
    le_of_not_lt fun hn =>
      not_le_of_lt ((opow_lt_opow_iff_right a1).2 hn) <|
        le_of_dvd (opow_ne_zero _ <| one_le_iff_ne_zero.1 <| a1.le) h,
    opow_dvd_opow _⟩

Divisibility Criterion for Ordinal Powers: $a^b \mid a^c \leftrightarrow b \leq c$ when $a > 1$

Informal description

For ordinals $a > 1$, $b$, and $c$, the divisibility relation $a^b \mid a^c$ holds if and only if $b \leq c$.

Ordinal.opow_mul theorem

(a b c : Ordinal) : a ^ (b * c) = (a ^ b) ^ c

Full source

theorem opow_mul (a b c : Ordinal) : a ^ (b * c) = (a ^ b) ^ c := by
  by_cases b0 : b = 0; · simp only [b0, zero_mul, opow_zero, one_opow]
  by_cases a0 : a = 0
  · subst a
    by_cases c0 : c = 0
    · simp only [c0, mul_zero, opow_zero]
    simp only [zero_opow b0, zero_opow c0, zero_opow (mul_ne_zero b0 c0)]
  rcases eq_or_lt_of_le (one_le_iff_ne_zero.2 a0) with a1 | a1
  · subst a1
    simp only [one_opow]
  induction c using limitRecOn with
  | zero => simp only [mul_zero, opow_zero]
  | succ c IH =>
    rw [mul_succ, opow_add, IH, opow_succ]
  | isLimit c l IH =>
    refine
      eq_of_forall_ge_iff fun d =>
        (((isNormal_opow a1).trans (isNormal_mul_right (Ordinal.pos_iff_ne_zero.2 b0))).limit_le
              l).trans
          ?_
    dsimp only [Function.comp_def]
    simp +contextual only [IH]
    exact (opow_le_of_limit (opow_ne_zero _ a0) l).symm

Exponentiation Law for Ordinals: $a^{b \cdot c} = (a^b)^c$

Informal description

For any ordinals $a$, $b$, and $c$, the exponentiation $a^{b \cdot c}$ equals $(a^b)^c$.

Ordinal.opow_mul_add_pos theorem

{b v : Ordinal} (hb : b ≠ 0) (u : Ordinal) (hv : v ≠ 0) (w : Ordinal) : 0 < b ^ u * v + w

Full source

theorem opow_mul_add_pos {b v : Ordinal} (hb : b ≠ 0) (u : Ordinal) (hv : v ≠ 0) (w : Ordinal) :
    0 < b ^ u * v + w :=
  (opow_pos u <| Ordinal.pos_iff_ne_zero.2 hb).trans_le <|
    (le_mul_left _ <| Ordinal.pos_iff_ne_zero.2 hv).trans <| le_add_right _ _

Positivity of Ordinal Expression $b^u \cdot v + w$ for Nonzero $b$ and $v$

Informal description

For any ordinals $b$, $v$, $u$, and $w$, if $b \neq 0$ and $v \neq 0$, then $0 < b^u \cdot v + w$.

Ordinal.opow_mul_add_lt_opow_mul_succ theorem

{b u w : Ordinal} (v : Ordinal) (hw : w < b ^ u) : b ^ u * v + w < b ^ u * succ v

Full source

theorem opow_mul_add_lt_opow_mul_succ {b u w : Ordinal} (v : Ordinal) (hw : w < b ^ u) :
    b ^ u * v + w < b ^ u * succ v := by
  rwa [mul_succ, add_lt_add_iff_left]

Inequality for Ordinal Exponentiation and Multiplication with Successor: $b^u \cdot v + w < b^u \cdot \text{succ}(v)$

Informal description

For ordinals $b, u, v, w$ with $w < b^u$, we have the inequality $b^u \cdot v + w < b^u \cdot \text{succ}(v)$.

Ordinal.opow_mul_add_lt_opow_succ theorem

{b u v w : Ordinal} (hvb : v < b) (hw : w < b ^ u) : b ^ u * v + w < b ^ succ u

Full source

theorem opow_mul_add_lt_opow_succ {b u v w : Ordinal} (hvb : v < b) (hw : w < b ^ u) :
    b ^ u * v + w < b ^ succ u := by
  convert (opow_mul_add_lt_opow_mul_succ v hw).trans_le
    (mul_le_mul_left' (succ_le_of_lt hvb) _) using 1
  exact opow_succ b u

Inequality for Ordinal Exponentiation and Successor: $b^u \cdot v + w < b^{u+1}$

Informal description

For ordinals $b, u, v, w$ with $v < b$ and $w < b^u$, we have the inequality $b^u \cdot v + w < b^{\text{succ}(u)}$.

Ordinal.log definition

(b : Ordinal) (x : Ordinal) : Ordinal

Full source

/-- The ordinal logarithm is the solution `u` to the equation `x = b ^ u * v + w` where `v < b` and
`w < b ^ u`. -/
@[pp_nodot]
def log (b : Ordinal) (x : Ordinal) : Ordinal :=
  if 1 < b then pred (sInf { o | x < b ^ o }) else 0

Ordinal logarithm

Informal description

The ordinal logarithm function $\log_b x$ is defined as the predecessor of the smallest ordinal $o$ such that $x < b^o$, when $1 < b$. If $b \leq 1$, the logarithm is defined to be $0$. More precisely, for ordinals $b$ and $x$, the logarithm satisfies the equation $x = b^{\log_b x} \cdot v + w$ where $v < b$ and $w < b^{\log_b x}$.

Ordinal.log_def theorem

{b : Ordinal} (h : 1 < b) (x : Ordinal) : log b x = pred (sInf {o | x < b ^ o})

Full source

theorem log_def {b : Ordinal} (h : 1 < b) (x : Ordinal) : log b x = pred (sInf { o | x < b ^ o }) :=
  if_pos h

Definition of Ordinal Logarithm via Infimum of Exponents

Informal description

For ordinals $b > 1$ and any ordinal $x$, the logarithm $\log_b x$ is equal to the predecessor of the smallest ordinal $o$ such that $x < b^o$. In other words: \[ \log_b x = \text{pred}(\inf \{o \mid x < b^o\}) \]

Ordinal.log_of_left_le_one theorem

{b : Ordinal} (h : b ≤ 1) (x : Ordinal) : log b x = 0

Full source

theorem log_of_left_le_one {b : Ordinal} (h : b ≤ 1) (x : Ordinal) : log b x = 0 :=
  if_neg h.not_lt

Logarithm of Ordinals with Base at Most One is Zero

Informal description

For any ordinals $b$ and $x$, if $b \leq 1$, then the logarithm $\log_b x$ is equal to $0$.

Ordinal.log_zero_left theorem

: ∀ b, log 0 b = 0

Full source

@[simp]
theorem log_zero_left : ∀ b, log 0 b = 0 :=
  log_of_left_le_one zero_le_one

Logarithm with Base Zero is Zero

Informal description

For any ordinal $b$, the logarithm with base $0$ satisfies $\log_0 b = 0$.

Ordinal.log_zero_right theorem

(b : Ordinal) : log b 0 = 0

Full source

@[simp]
theorem log_zero_right (b : Ordinal) : log b 0 = 0 := by
  obtain hb | hb := lt_or_le 1 b
  · rw [log_def hb, ← Ordinal.le_zero, pred_le, succ_zero]
    apply csInf_le'
    rw [mem_setOf, opow_one]
    exact bot_lt_of_lt hb
  · rw [log_of_left_le_one hb]

Logarithm of Zero Ordinal is Zero: $\log_b 0 = 0$

Informal description

For any ordinal $b$, the logarithm of the zero ordinal with base $b$ is equal to zero, i.e., $\log_b 0 = 0$.

Ordinal.log_one_left theorem

: ∀ b, log 1 b = 0

Full source

@[simp]
theorem log_one_left : ∀ b, log 1 b = 0 :=
  log_of_left_le_one le_rfl

Logarithm with Base One is Zero

Informal description

For any ordinal $b$, the logarithm of $b$ with base $1$ is equal to $0$, i.e., $\log_1 b = 0$.

Ordinal.succ_log_def theorem

{b x : Ordinal} (hb : 1 < b) (hx : x ≠ 0) : succ (log b x) = sInf {o : Ordinal | x < b ^ o}

Full source

theorem succ_log_def {b x : Ordinal} (hb : 1 < b) (hx : x ≠ 0) :
    succ (log b x) = sInf { o : Ordinal | x < b ^ o } := by
  let t := sInf { o : Ordinal | x < b ^ o }
  have : x < b ^ t := csInf_mem (log_nonempty hb)
  rcases zero_or_succ_or_limit t with (h | h | h)
  · refine ((one_le_iff_ne_zero.2 hx).not_lt ?_).elim
    simpa only [h, opow_zero] using this
  · rw [show log b x = pred t from log_def hb x, succ_pred_iff_is_succ.2 h]
  · rcases (lt_opow_of_limit (zero_lt_one.trans hb).ne' h).1 this with ⟨a, h₁, h₂⟩
    exact h₁.not_le.elim ((le_csInf_iff'' (log_nonempty hb)).1 le_rfl a h₂)

Successor of Ordinal Logarithm Equals Infimum of Exponents

Informal description

For ordinals $b > 1$ and $x \neq 0$, the successor of the logarithm $\log_b x$ is equal to the infimum of the set of ordinals $o$ such that $x < b^o$. That is, \[ \text{succ}(\log_b x) = \inf \{ o \mid x < b^o \}. \]

Ordinal.lt_opow_succ_log_self theorem

{b : Ordinal} (hb : 1 < b) (x : Ordinal) : x < b ^ succ (log b x)

Full source

theorem lt_opow_succ_log_self {b : Ordinal} (hb : 1 < b) (x : Ordinal) :
    x < b ^ succ (log b x) := by
  rcases eq_or_ne x 0 with (rfl | hx)
  · apply opow_pos _ (zero_lt_one.trans hb)
  · rw [succ_log_def hb hx]
    exact csInf_mem (log_nonempty hb)

Strict inequality for ordinal exponentiation and logarithm: $x < b^{\text{succ}(\log_b x)}$

Informal description

For any ordinal $b > 1$ and any ordinal $x$, we have the strict inequality: \[ x < b^{\text{succ}(\log_b x)} \] where $\text{succ}(\log_b x)$ denotes the successor ordinal of $\log_b x$.

Ordinal.opow_log_le_self theorem

(b : Ordinal) {x : Ordinal} (hx : x ≠ 0) : b ^ log b x ≤ x

Full source

theorem opow_log_le_self (b : Ordinal) {x : Ordinal} (hx : x ≠ 0) : b ^ log b x ≤ x := by
  rcases eq_or_ne b 0 with (rfl | b0)
  · exact (zero_opow_le _).trans (one_le_iff_ne_zero.2 hx)
  rcases lt_or_eq_of_le (one_le_iff_ne_zero.2 b0) with (hb | rfl)
  · refine le_of_not_lt fun h => (lt_succ (log b x)).not_le ?_
    have := @csInf_le' _ _ { o | x < b ^ o } _ h
    rwa [← succ_log_def hb hx] at this
  · rwa [one_opow, one_le_iff_ne_zero]

Ordinal Logarithm Inequality: $b^{\log_b x} \leq x$ for $x \neq 0$

Informal description

For any ordinals $b$ and $x$ with $x \neq 0$, the inequality $b^{\log_b x} \leq x$ holds.

Ordinal.opow_le_iff_le_log theorem

{b x c : Ordinal} (hb : 1 < b) (hx : x ≠ 0) : b ^ c ≤ x ↔ c ≤ log b x

Full source

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

See `opow_le_iff_le_log'` for a variant assuming `c ≠ 0` rather than `x ≠ 0`. See also
`le_log_of_opow_le` and `opow_le_of_le_log`, which are both separate implications under weaker
assumptions. -/
theorem opow_le_iff_le_log {b x c : Ordinal} (hb : 1 < b) (hx : x ≠ 0) :
    b ^ c ≤ x ↔ c ≤ log b x := by
  constructor <;>
  intro h
  · apply le_of_not_lt
    intro hn
    apply (lt_opow_succ_log_self hb x).not_le <|
      ((opow_le_opow_iff_right hb).2 <| succ_le_of_lt hn).trans h
  · exact ((opow_le_opow_iff_right hb).2 h).trans <| opow_log_le_self b hx

Galois Connection Between Ordinal Exponentiation and Logarithm: $b^c \leq x \leftrightarrow c \leq \log_b x$ for $b > 1$ and $x \neq 0$

Informal description

For ordinals $b > 1$, $x \neq 0$, and $c$, the inequality $b^c \leq x$ holds if and only if $c \leq \log_b x$. This shows that the functions $b^c$ and $\log_b x$ form a Galois connection when $b > 1$ and $x \neq 0$.

Ordinal.opow_le_iff_le_log' theorem

{b x c : Ordinal} (hb : 1 < b) (hc : c ≠ 0) : b ^ c ≤ x ↔ c ≤ log b x

Full source

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

See `opow_le_iff_le_log` for a variant assuming `x ≠ 0` rather than `c ≠ 0`. See also
`le_log_of_opow_le` and `opow_le_of_le_log`, which are both separate implications under weaker
assumptions. -/
theorem opow_le_iff_le_log' {b x c : Ordinal} (hb : 1 < b) (hc : c ≠ 0) :
    b ^ c ≤ x ↔ c ≤ log b x := by
  obtain rfl | hx := eq_or_ne x 0
  · rw [log_zero_right, Ordinal.le_zero, Ordinal.le_zero, opow_eq_zero]
    simp [hc, (zero_lt_one.trans hb).ne']
  · exact opow_le_iff_le_log hb hx

Galois Connection Between Ordinal Exponentiation and Logarithm (Variant): $b^c \leq x \leftrightarrow c \leq \log_b x$ for $b > 1$ and $c \neq 0$

Informal description

For ordinals $b > 1$, $c \neq 0$, and $x$, the inequality $b^c \leq x$ holds if and only if $c \leq \log_b x$. This shows that the functions $b^c$ and $\log_b x$ form a Galois connection when $b > 1$ and $c \neq 0$.

Ordinal.le_log_of_opow_le theorem

{b x c : Ordinal} (hb : 1 < b) (h : b ^ c ≤ x) : c ≤ log b x

Full source

theorem le_log_of_opow_le {b x c : Ordinal} (hb : 1 < b) (h : b ^ c ≤ x) : c ≤ log b x := by
  obtain rfl | hx := eq_or_ne x 0
  · rw [Ordinal.le_zero, opow_eq_zero] at h
    exact (zero_lt_one.asymm <| h.1 ▸ hb).elim
  · exact (opow_le_iff_le_log hb hx).1 h

Implication from Ordinal Exponentiation to Logarithm: $b^c \leq x \Rightarrow c \leq \log_b x$ for $b > 1$

Informal description

For ordinals $b > 1$, $x$, and $c$, if $b^c \leq x$, then $c \leq \log_b x$.

Ordinal.opow_le_of_le_log theorem

{b x c : Ordinal} (hc : c ≠ 0) (h : c ≤ log b x) : b ^ c ≤ x

Full source

theorem opow_le_of_le_log {b x c : Ordinal} (hc : c ≠ 0) (h : c ≤ log b x) : b ^ c ≤ x := by
  obtain hb | hb := le_or_lt b 1
  · rw [log_of_left_le_one hb] at h
    exact (h.not_lt (Ordinal.pos_iff_ne_zero.2 hc)).elim
  · rwa [opow_le_iff_le_log' hb hc]

Implication from Ordinal Logarithm to Exponentiation: $c \leq \log_b x \Rightarrow b^c \leq x$ for $c \neq 0$

Informal description

For ordinals $b$, $x$, and $c \neq 0$, if $c \leq \log_b x$, then $b^c \leq x$.

Ordinal.lt_opow_iff_log_lt theorem

{b x c : Ordinal} (hb : 1 < b) (hx : x ≠ 0) : x < b ^ c ↔ log b x < c

Full source

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

See `lt_opow_iff_log_lt'` for a variant assuming `c ≠ 0` rather than `x ≠ 0`. See also
`lt_opow_of_log_lt` and `lt_log_of_lt_opow`, which are both separate implications under weaker
assumptions. -/
theorem lt_opow_iff_log_lt {b x c : Ordinal} (hb : 1 < b) (hx : x ≠ 0) : x < b ^ c ↔ log b x < c :=
  lt_iff_lt_of_le_iff_le (opow_le_iff_le_log hb hx)

Strict Inequality Characterization for Ordinal Exponentiation and Logarithm: $x < b^c \leftrightarrow \log_b x < c$ for $b > 1$ and $x \neq 0$

Informal description

For ordinals $b > 1$, $x \neq 0$, and $c$, the inequality $x < b^c$ holds if and only if $\log_b x < c$.

Ordinal.lt_opow_iff_log_lt' theorem

{b x c : Ordinal} (hb : 1 < b) (hc : c ≠ 0) : x < b ^ c ↔ log b x < c

Full source

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

See `lt_opow_iff_log_lt` for a variant assuming `x ≠ 0` rather than `c ≠ 0`. See also
`lt_opow_of_log_lt` and `lt_log_of_lt_opow`, which are both separate implications under weaker
assumptions. -/
theorem lt_opow_iff_log_lt' {b x c : Ordinal} (hb : 1 < b) (hc : c ≠ 0) : x < b ^ c ↔ log b x < c :=
  lt_iff_lt_of_le_iff_le (opow_le_iff_le_log' hb hc)

Strict Inequality Characterization for Ordinal Exponentiation and Logarithm: $x < b^c \leftrightarrow \log_b x < c$ for $b > 1$ and $c \neq 0$

Informal description

For ordinals $b > 1$, $c \neq 0$, and $x$, the strict inequality $x < b^c$ holds if and only if $\log_b x < c$.

Ordinal.lt_opow_of_log_lt theorem

{b x c : Ordinal} (hb : 1 < b) : log b x < c → x < b ^ c

Full source

theorem lt_opow_of_log_lt {b x c : Ordinal} (hb : 1 < b) : log b x < c → x < b ^ c :=
  lt_imp_lt_of_le_imp_le <| le_log_of_opow_le hb

Strict Implication from Logarithm to Ordinal Exponentiation: $\log_b x < c \Rightarrow x < b^c$ for $b > 1$

Informal description

For ordinals $b > 1$, $x$, and $c$, if $\log_b x < c$, then $x < b^c$.

Ordinal.lt_log_of_lt_opow theorem

{b x c : Ordinal} (hc : c ≠ 0) : x < b ^ c → log b x < c

Full source

theorem lt_log_of_lt_opow {b x c : Ordinal} (hc : c ≠ 0) : x < b ^ c → log b x < c :=
  lt_imp_lt_of_le_imp_le <| opow_le_of_le_log hc

Strict Implication from Ordinal Exponentiation to Logarithm: $x < b^c \Rightarrow \log_b x < c$ for $c \neq 0$

Informal description

For ordinals $b$, $x$, and $c \neq 0$, if $x < b^c$, then $\log_b x < c$.

Ordinal.log_pos theorem

{b o : Ordinal} (hb : 1 < b) (ho : o ≠ 0) (hbo : b ≤ o) : 0 < log b o

Full source

theorem log_pos {b o : Ordinal} (hb : 1 < b) (ho : o ≠ 0) (hbo : b ≤ o) : 0 < log b o := by
  rwa [← succ_le_iff, succ_zero, ← opow_le_iff_le_log hb ho, opow_one]

Positivity of Ordinal Logarithm: $0 < \log_b o$ for $b > 1$ and $b \leq o \neq 0$

Informal description

For ordinals $b > 1$ and $o \neq 0$ with $b \leq o$, the logarithm $\log_b o$ is strictly positive, i.e., $0 < \log_b o$.

Ordinal.log_eq_zero theorem

{b o : Ordinal} (hbo : o < b) : log b o = 0

Full source

theorem log_eq_zero {b o : Ordinal} (hbo : o < b) : log b o = 0 := by
  rcases eq_or_ne o 0 with (rfl | ho)
  · exact log_zero_right b
  rcases le_or_lt b 1 with hb | hb
  · rcases le_one_iff.1 hb with (rfl | rfl)
    · exact log_zero_left o
    · exact log_one_left o
  · rwa [← Ordinal.le_zero, ← lt_succ_iff, succ_zero, ← lt_opow_iff_log_lt hb ho, opow_one]

Logarithm of Ordinal Less Than Base is Zero: $\log_b o = 0$ when $o < b$

Informal description

For any ordinals $b$ and $o$ such that $o < b$, the logarithm of $o$ with base $b$ is zero, i.e., $\log_b o = 0$.

Ordinal.log_mono_right theorem

(b : Ordinal) {x y : Ordinal} (xy : x ≤ y) : log b x ≤ log b y

Full source

@[mono]
theorem log_mono_right (b : Ordinal) {x y : Ordinal} (xy : x ≤ y) : log b x ≤ log b y := by
  obtain rfl | hx := eq_or_ne x 0
  · simp_rw [log_zero_right, Ordinal.zero_le]
  · obtain hb | hb := lt_or_le 1 b
    · exact (opow_le_iff_le_log hb (hx.bot_lt.trans_le xy).ne').1 <|
        (opow_log_le_self _ hx).trans xy
    · rw [log_of_left_le_one hb, log_of_left_le_one hb]

Monotonicity of Ordinal Logarithm: $\log_b x \leq \log_b y$ when $x \leq y$

Informal description

For any ordinals $b$, $x$, and $y$ with $x \leq y$, the logarithm satisfies $\log_b x \leq \log_b y$.

Ordinal.log_le_self theorem

(b x : Ordinal) : log b x ≤ x

Full source

theorem log_le_self (b x : Ordinal) : log b x ≤ x := by
  obtain rfl | hx := eq_or_ne x 0
  · rw [log_zero_right]
  · obtain hb | hb := lt_or_le 1 b
    · exact (right_le_opow _ hb).trans (opow_log_le_self b hx)
    · simp_rw [log_of_left_le_one hb, Ordinal.zero_le]

Logarithm Bound: $\log_b x \leq x$ for Ordinals

Informal description

For any ordinals $b$ and $x$, the logarithm $\log_b x$ is less than or equal to $x$.

Ordinal.log_one_right theorem

(b : Ordinal) : log b 1 = 0

Full source

@[simp]
theorem log_one_right (b : Ordinal) : log b 1 = 0 := by
  obtain hb | hb := lt_or_le 1 b
  · exact log_eq_zero hb
  · exact log_of_left_le_one hb 1

Logarithm of One: $\log_b 1 = 0$ for any ordinal $b$

Informal description

For any ordinal $b$, the logarithm of $1$ with base $b$ is $0$, i.e., $\log_b 1 = 0$.

Ordinal.mod_opow_log_lt_self theorem

(b : Ordinal) {o : Ordinal} (ho : o ≠ 0) : o % (b ^ log b o) < o

Full source

theorem mod_opow_log_lt_self (b : Ordinal) {o : Ordinal} (ho : o ≠ 0) : o % (b ^ log b o) < o := by
  rcases eq_or_ne b 0 with (rfl | hb)
  · simpa using Ordinal.pos_iff_ne_zero.2 ho
  · exact (mod_lt _ <| opow_ne_zero _ hb).trans_le (opow_log_le_self _ ho)

Remainder Bound in Ordinal Logarithmic Division: $o \% (b^{\log_b o}) < o$

Informal description

For any ordinals $b$ and $o$ with $o \neq 0$, the remainder $o \% (b^{\log_b o})$ is strictly less than $o$.

Ordinal.log_mod_opow_log_lt_log_self theorem

{b o : Ordinal} (hb : 1 < b) (hbo : b ≤ o) : log b (o % (b ^ log b o)) < log b o

Full source

theorem log_mod_opow_log_lt_log_self {b o : Ordinal} (hb : 1 < b) (hbo : b ≤ o) :
    log b (o % (b ^ log b o)) < log b o := by
  rcases eq_or_ne (o % (b ^ log b o)) 0 with h | h
  · rw [h, log_zero_right]
    exact log_pos hb (one_le_iff_ne_zero.1 (hb.le.trans hbo)) hbo
  · rw [← succ_le_iff, succ_log_def hb h]
    apply csInf_le'
    apply mod_lt
    rw [← Ordinal.pos_iff_ne_zero]
    exact opow_pos _ (zero_lt_one.trans hb)

Logarithmic Remainder Inequality: $\log_b(o \% b^{\log_b o}) < \log_b o$ for $b > 1$ and $b \leq o$

Informal description

For ordinals $b > 1$ and $o \geq b$, the logarithm of the remainder $o \% (b^{\log_b o})$ with base $b$ is strictly less than $\log_b o$, i.e., \[ \log_b (o \% (b^{\log_b o})) < \log_b o. \]

Ordinal.log_eq_iff theorem

{b x : Ordinal} (hb : 1 < b) (hx : x ≠ 0) (y : Ordinal) : log b x = y ↔ b ^ y ≤ x ∧ x < b ^ succ y

Full source

theorem log_eq_iff {b x : Ordinal} (hb : 1 < b) (hx : x ≠ 0) (y : Ordinal) :
    loglog b x = y ↔ b ^ y ≤ x ∧ x < b ^ succ y := by
  constructor
  · rintro rfl
    use opow_log_le_self b hx, lt_opow_succ_log_self hb x
  · rintro ⟨hx₁, hx₂⟩
    apply le_antisymm
    · rwa [← lt_succ_iff, ← lt_opow_iff_log_lt hb hx]
    · rwa [← opow_le_iff_le_log hb hx]

Characterization of Ordinal Logarithm: $\log_b x = y \leftrightarrow b^y \leq x < b^{y+1}$ for $b > 1$ and $x \neq 0$

Informal description

For ordinals $b > 1$, $x \neq 0$, and $y$, the equality $\log_b x = y$ holds if and only if $b^y \leq x$ and $x < b^{y+1}$, where $y+1$ denotes the successor ordinal of $y$.

Ordinal.log_opow_mul_add theorem

{b u v w : Ordinal} (hb : 1 < b) (hv : v ≠ 0) (hw : w < b ^ u) : log b (b ^ u * v + w) = u + log b v

Full source

theorem log_opow_mul_add {b u v w : Ordinal} (hb : 1 < b) (hv : v ≠ 0) (hw : w < b ^ u) :
    log b (b ^ u * v + w) = u + log b v := by
  rw [log_eq_iff hb]
  · constructor
    · rw [opow_add]
      exact (mul_le_mul_left' (opow_log_le_self b hv) _).trans (le_add_right _ w)
    · apply (add_lt_add_left hw _).trans_le
      rw [← mul_succ, ← add_succ, opow_add]
      apply mul_le_mul_left'
      rw [succ_le_iff]
      exact lt_opow_succ_log_self hb _
  · exact fun h ↦ mul_ne_zero (opow_ne_zero u (bot_lt_of_lt hb).ne') hv <|
      left_eq_zero_of_add_eq_zero h

Logarithm of Sum of Scaled Ordinals: $\log_b(b^u \cdot v + w) = u + \log_b v$ for $b > 1$, $v \neq 0$, $w < b^u$

Informal description

For ordinals $b > 1$, $v \neq 0$, and $w < b^u$, the logarithm of $b^u \cdot v + w$ with base $b$ satisfies: \[ \log_b (b^u \cdot v + w) = u + \log_b v. \]

Ordinal.log_opow_mul theorem

{b v : Ordinal} (hb : 1 < b) (u : Ordinal) (hv : v ≠ 0) : log b (b ^ u * v) = u + log b v

Full source

theorem log_opow_mul {b v : Ordinal} (hb : 1 < b) (u : Ordinal) (hv : v ≠ 0) :
    log b (b ^ u * v) = u + log b v := by
  simpa using log_opow_mul_add hb hv (opow_pos u (bot_lt_of_lt hb))

Logarithm of Scaled Ordinal: $\log_b(b^u \cdot v) = u + \log_b v$ for $b > 1$ and $v \neq 0$

Informal description

For ordinals $b > 1$, $v \neq 0$, and any ordinal $u$, the logarithm of $b^u \cdot v$ with base $b$ satisfies: \[ \log_b (b^u \cdot v) = u + \log_b v. \]

Ordinal.log_opow theorem

{b : Ordinal} (hb : 1 < b) (x : Ordinal) : log b (b ^ x) = x

Full source

theorem log_opow {b : Ordinal} (hb : 1 < b) (x : Ordinal) : log b (b ^ x) = x := by
  convert log_opow_mul hb x zero_ne_one.symm using 1
  · rw [mul_one]
  · rw [log_one_right, add_zero]

Logarithm of Power Identity: $\log_b(b^x) = x$ for $b > 1$

Informal description

For any ordinals $b > 1$ and $x$, the logarithm of $b^x$ with base $b$ satisfies: \[ \log_b (b^x) = x. \]

Ordinal.div_opow_log_pos theorem

(b : Ordinal) {o : Ordinal} (ho : o ≠ 0) : 0 < o / (b ^ log b o)

Full source

theorem div_opow_log_pos (b : Ordinal) {o : Ordinal} (ho : o ≠ 0) : 0 < o / (b ^ log b o) := by
  rcases eq_zero_or_pos b with (rfl | hb)
  · simpa using Ordinal.pos_iff_ne_zero.2 ho
  · rw [div_pos (opow_ne_zero _ hb.ne')]
    exact opow_log_le_self b ho

Positivity of Ordinal Division by Exponential of Logarithm: $0 < o / (b^{\log_b o})$ for $o \neq 0$

Informal description

For any ordinals $b$ and $o$ with $o \neq 0$, the division $o / (b^{\log_b o})$ is strictly positive, i.e., $0 < o / (b^{\log_b o})$.

Ordinal.div_opow_log_lt theorem

{b : Ordinal} (o : Ordinal) (hb : 1 < b) : o / (b ^ log b o) < b

Full source

theorem div_opow_log_lt {b : Ordinal} (o : Ordinal) (hb : 1 < b) : o / (b ^ log b o) < b := by
  rw [div_lt (opow_pos _ (zero_lt_one.trans hb)).ne', ← opow_succ]
  exact lt_opow_succ_log_self hb o

Strict Inequality for Ordinal Division and Exponentiation: $o / (b^{\log_b o}) < b$

Informal description

For any ordinals $b > 1$ and $o$, we have the strict inequality: \[ o / (b^{\log_b o}) < b \] where $\log_b o$ is the ordinal logarithm of $o$ with base $b$.

Ordinal.add_log_le_log_mul theorem

{x y : Ordinal} (b : Ordinal) (hx : x ≠ 0) (hy : y ≠ 0) : log b x + log b y ≤ log b (x * y)

Full source

theorem add_log_le_log_mul {x y : Ordinal} (b : Ordinal) (hx : x ≠ 0) (hy : y ≠ 0) :
    log b x + log b y ≤ log b (x * y) := by
  obtain hb | hb := lt_or_le 1 b
  · rw [← opow_le_iff_le_log hb (mul_ne_zero hx hy), opow_add]
    exact mul_le_mul' (opow_log_le_self b hx) (opow_log_le_self b hy)
  · simpa only [log_of_left_le_one hb, zero_add] using le_rfl

Subadditivity of Ordinal Logarithm: $\log_b x + \log_b y \leq \log_b (x \cdot y)$ for $x, y \neq 0$

Informal description

For any ordinals $b$, $x$, and $y$ with $x \neq 0$ and $y \neq 0$, the sum of the logarithms satisfies \[ \log_b x + \log_b y \leq \log_b (x \cdot y). \]

Ordinal.omega0_opow_mul_nat_lt theorem

{a b : Ordinal} (h : a < b) (n : ℕ) : ω ^ a * n < ω ^ b

Full source

theorem omega0_opow_mul_nat_lt {a b : Ordinal} (h : a < b) (n : ℕ) : ω ^ a * n < ω ^ b := by
  apply lt_of_lt_of_le _ (opow_le_opow_right omega0_pos (succ_le_of_lt h))
  rw [opow_succ]
  exact mul_lt_mul_of_pos_left (nat_lt_omega0 n) (opow_pos a omega0_pos)

Strict inequality for ordinal exponentiation and multiplication: $\omega^a \cdot n < \omega^b$ when $a < b$

Informal description

For any ordinals $a$ and $b$ such that $a < b$, and for any natural number $n$, the ordinal $\omega^a \cdot n$ is strictly less than $\omega^b$, where $\omega$ is the first infinite ordinal.

Ordinal.lt_omega0_opow theorem

{a b : Ordinal} (hb : b ≠ 0) : a < ω ^ b ↔ ∃ c < b, ∃ n : ℕ, a < ω ^ c * n

Full source

theorem lt_omega0_opow {a b : Ordinal} (hb : b ≠ 0) :
    a < ω ^ b ↔ ∃ c < b, ∃ n : ℕ, a < ω ^ c * n := by
  refine ⟨fun ha ↦ ⟨_, lt_log_of_lt_opow hb ha, ?_⟩,
    fun ⟨c, hc, n, hn⟩ ↦ hn.trans (omega0_opow_mul_nat_lt hc n)⟩
  obtain ⟨n, hn⟩ := lt_omega0.1 (div_opow_log_lt a one_lt_omega0)
  use n.succ
  rw [natCast_succ, ← hn]
  exact lt_mul_succ_div a (opow_ne_zero _ omega0_ne_zero)

Characterization of ordinals less than $\omega^b$ via $\omega^c \cdot n$ for $c < b$ and $n \in \mathbb{N}$

Informal description

For any ordinals $a$ and $b$ with $b \neq 0$, the inequality $a < \omega^b$ holds if and only if there exist an ordinal $c < b$ and a natural number $n$ such that $a < \omega^c \cdot n$, where $\omega$ is the first infinite ordinal.

Ordinal.lt_omega0_opow_succ theorem

{a b : Ordinal} : a < ω ^ succ b ↔ ∃ n : ℕ, a < ω ^ b * n

Full source

theorem lt_omega0_opow_succ {a b : Ordinal} : a < ω ^ succ b ↔ ∃ n : ℕ, a < ω ^ b * n := by
  refine ⟨fun ha ↦ ?_, fun ⟨n, hn⟩ ↦ hn.trans (omega0_opow_mul_nat_lt (lt_succ b) n)⟩
  obtain ⟨c, hc, n, hn⟩ := (lt_omega0_opow (succ_ne_zero b)).1 ha
  refine ⟨n, hn.trans_le (mul_le_mul_right' ?_ _)⟩
  rwa [opow_le_opow_iff_right one_lt_omega0, ← lt_succ_iff]

Characterization of ordinals less than $\omega^{\mathrm{succ}(b)}$ via $\omega^b \cdot n$ for $n \in \mathbb{N}$

Informal description

For any ordinals $a$ and $b$, the inequality $a < \omega^{\mathrm{succ}(b)}$ holds if and only if there exists a natural number $n$ such that $a < \omega^b \cdot n$, where $\omega$ is the first infinite ordinal and $\mathrm{succ}(b)$ denotes the successor ordinal of $b$.

Ordinal.natCast_opow theorem

(m : ℕ) : ∀ n : ℕ, ↑(m ^ n : ℕ) = (m : Ordinal) ^ (n : Ordinal)

Full source

@[simp, norm_cast]
theorem natCast_opow (m : ℕ) : ∀ n : ℕ, ↑(m ^ n : ℕ) = (m : Ordinal) ^ (n : Ordinal)
  | 0 => by simp
  | n + 1 => by
    rw [pow_succ, natCast_mul, natCast_opow m n, Nat.cast_succ, add_one_eq_succ, opow_succ]

Natural Number Power to Ordinal Power Preservation: $(m^n) = m^n$

Informal description

For any natural numbers $m$ and $n$, the canonical embedding of the natural number power $m^n$ into the ordinals is equal to the ordinal exponentiation of the embedded values, i.e., $(m^n) = m^n$ where the left-hand side is the natural number power and the right-hand side is the ordinal power.

Ordinal.iSup_pow theorem

{o : Ordinal} (ho : 0 < o) : ⨆ n : ℕ, o ^ n = o ^ ω

Full source

theorem iSup_pow {o : Ordinal} (ho : 0 < o) : ⨆ n : ℕ, o ^ n = o ^ ω := by
  simp_rw [← opow_natCast]
  rcases (one_le_iff_pos.2 ho).lt_or_eq with ho₁ | rfl
  · exact (isNormal_opow ho₁).apply_omega0
  · rw [one_opow]
    refine le_antisymm (Ordinal.iSup_le fun n => by rw [one_opow]) ?_
    exact_mod_cast Ordinal.le_iSup _ 0

Supremum of Powers of Nonzero Ordinal Equals Omega Power: $\bigsqcup_{n} o^n = o^\omega$

Informal description

For any ordinal $o > 0$, the supremum of the sequence $(o^n)_{n \in \mathbb{N}}$ is equal to $o^\omega$, where $\omega$ is the first infinite ordinal. In other words, $\bigsqcup_{n \in \mathbb{N}} o^n = o^\omega$.