CLRS-Lean
Chapters 1–35 · CLRS Fourth Edition
Chapter 3. Characterizing Running Times
3.3. Standard Notations and Common Functions

Imports

import CLRSLean.FourthEdition.Chapter_03.Section_03_2_Standard_Functions

3.3. Standard Notations and Common Functions

This is the canonical fourth-edition reader facade for the standard functions used throughout CLRS. The imported theorem modules cover integer rounding, modular arithmetic, exponentials and logarithms, factorials, functional iteration, Fibonacci numbers, and the growth hierarchy.

Main results

The page exposes the proved floor, ceiling, remainder, logarithm, factorial, iteration, and Fibonacci identities; real-exponent and polynomial-growth bridges; the hierarchy through n^(log n) and n^n; and the exact effective Robbins refinement of Stirling's formula.

Status: proved for the represented identities and growth comparisons.

Definitions and proofs

CLRSLean.FourthEdition.Chapter_03.Section_03_2_Standard_Functions.Core

              open Filteropen Asymptoticsopen Realopen Stirlingopen scoped Topology

3.2. Standard Notations and Common Functions

Concrete asymptotic comparisons for algorithm analysis.

nᵃ = o(nᵇ) when a < b
nᵃ = o(cⁿ) when 1 < c
log n = o(nʳ) when 0 < r
(log n)ᵃ = o(nʳ) when 0 < r
aⁿ = o(bⁿ) when 0 ≤ a < b
the harmonic numbers satisfy Hₙ ~ log n and Hₙ = Θ(log n)
⌊n⌋ = Θ(n) and ⌈n⌉ = Θ(n) on ℕ
⌊n/2⌋ = Θ(n) and ⌈n/2⌉ = Θ(n) on ℕ
lower and upper factorial bounds
aⁿ = o(n!) and n! = o(nⁿ)
nᵃ = o(2ⁿ), 2ⁿ = o(n!), and nᵃ = o(n!)
n! = Ω(cⁿ) for every base c
log n = o(n) and log (log n) = o(log n)
log_b n = Θ(log n) and log_b n = o(nʳ) for 0 < r
(log n)ᵃ = o(cⁿ) when 1 < c
Fibonacci growth: closed form Fₙ = (φⁿ − ψⁿ)/√5, Fₙ = Θ(φⁿ), and the closest-integer bound |φⁿ/√5 − Fₙ| < 1/2
the iterated logarithm lg* n with base values, lg*(2ⁿ) = 1 + lg* n, monotonicity, lg* n ≤ log₂ n + 1, and the extreme slow growth lg* n = o(log n)

namespace CLRSnamespace Chapter03

Polynomial comparisons

nᵃ = o(nᵇ) when a < b.

theorem isLittleO_pow_pow {a b : ℕ} (h : a < b) :
    isLittleO (fun n : ℕ => (n : ℝ) ^ a) (fun n : ℕ => (n : ℝ) ^ b) := by
  unfold isLittleO
  have h_ℝ : (fun x : ℝ => x ^ a) =o[atTop] (fun x : ℝ => x ^ b) :=
    Asymptotics.isLittleO_pow_pow_atTop_of_lt (𝕜 := ℝ) h
  exact (h_ℝ.comp_tendsto tendsto_natCast_atTop_atTop).congr
    (by simp) (by simp)

nᵃ = O(nᵇ) when a ≤ b.

theorem isBigO_pow_pow {a b : ℕ} (h : a ≤ b) :
    isBigO (fun n : ℕ => (n : ℝ) ^ a) (fun n : ℕ => (n : ℝ) ^ b) := by
  rcases Nat.eq_or_lt_of_le h with (rfl | hlt)
  · exact isBigO_refl _
  · exact (isLittleO_pow_pow hlt).isBigO

Polynomial, logarithmic, and exponential comparisons

For any natural exponent a and real base c > 1, nᵃ = o(cⁿ).

theorem isLittleO_pow_const_exp {a : ℕ} {c : ℝ} (hc : 1 < c) :
    isLittleO (fun n : ℕ => (n : ℝ) ^ a) (fun n : ℕ => c ^ n) := by
  unfold isLittleO
  exact isLittleO_pow_const_const_pow_of_one_lt (R := ℝ) a hc

For every positive real exponent r, log n = o(nʳ).

theorem isLittleO_log_rpow {r : ℝ} (hr : 0 < r) :
    isLittleO (fun n : ℕ => Real.log (n : ℝ)) (fun n : ℕ => (n : ℝ) ^ r) := by
  unfold isLittleO
  exact (isLittleO_log_rpow_atTop hr).comp_tendsto tendsto_natCast_atTop_atTop

For every fixed natural exponent a and positive real exponent r, (log n)ᵃ = o(nʳ).

theorem isLittleO_log_pow_rpow {a : ℕ} {r : ℝ} (hr : 0 < r) :
    isLittleO (fun n : ℕ => Real.log (n : ℝ) ^ a) (fun n : ℕ => (n : ℝ) ^ r) := by
  unfold isLittleO
  have hreal :
      (fun x : ℝ => Real.log x ^ (a : ℝ)) =o[atTop] (fun x : ℝ => x ^ r) :=
    isLittleO_log_rpow_rpow_atTop (a : ℝ) hr
  simpa [Function.comp_def, Real.rpow_natCast] using
    hreal.comp_tendsto tendsto_natCast_atTop_atTop

Weak O form of isLittleO_log_pow_rpow.

theorem isBigO_log_pow_rpow {a : ℕ} {r : ℝ} (hr : 0 < r) :
    isBigO (fun n : ℕ => Real.log (n : ℝ) ^ a) (fun n : ℕ => (n : ℝ) ^ r) :=
  (isLittleO_log_pow_rpow (a := a) hr).isBigO

If 0 ≤ a < b, then aⁿ = o(bⁿ).

theorem isLittleO_exp_exp_of_lt {a b : ℝ} (ha : 0 ≤ a) (hab : a < b) :
    isLittleO (fun n : ℕ => a ^ n) (fun n : ℕ => b ^ n) := by
  unfold isLittleO
  exact isLittleO_pow_pow_of_lt_left ha hab

Harmonic numbers

The harmonic numbers are asymptotic to log n.


theorem isEquivalent_harmonic_log :
    (fun n : ℕ => (harmonic n : ℝ)) ~[atTop] (fun n : ℕ => Real.log (n : ℝ)) := by
  have hdiffO :
      (fun n : ℕ => (harmonic n : ℝ) - Real.log (n : ℝ)) =O[atTop]
        (fun _ : ℕ => (1 : ℝ)) := by
    exact Filter.Tendsto.isBigO_one (F := ℝ) Real.tendsto_harmonic_sub_log
  have hconst :
      (fun _ : ℕ => (1 : ℝ)) =o[atTop] (fun n : ℕ => Real.log (n : ℝ)) := by
    exact Real.isLittleO_const_log_atTop.comp_tendsto tendsto_natCast_atTop_atTop
  exact hdiffO.trans_isLittleO hconst

The harmonic numbers have logarithmic growth, Hₙ = Θ(log n).

theorem isBigTheta_harmonic_log :
    isBigTheta (fun n : ℕ => (harmonic n : ℝ)) (fun n : ℕ => Real.log (n : ℝ)) := by
  have htheta :
      (fun n : ℕ => (harmonic n : ℝ)) =Θ[atTop]
        (fun n : ℕ => Real.log (n : ℝ)) :=
    isEquivalent_harmonic_log.isTheta
  exact ⟨by unfold isBigO; exact htheta.1, by unfold isBigOmega; exact htheta.2⟩

Floor and ceiling are Θ(id) on ℕ

              

theorem isBigTheta_nat_floor_coerce : isBigTheta (fun n : ℕ => (⌊(n : ℝ)⌋₊ : ℝ)) (fun n : ℕ => (n : ℝ)) := by
  have h_equiv : (fun x : ℝ => (⌊x⌋₊ : ℝ)) ~[atTop] (fun x : ℝ => x) := isEquivalent_nat_floor
  have hO : (fun n : ℕ => (⌊(n : ℝ)⌋₊ : ℝ)) =O[atTop] (fun n : ℕ => (n : ℝ)) :=
    (h_equiv.isBigO.comp_tendsto tendsto_natCast_atTop_atTop).congr (by simp) (by simp)
  have hΩ : (fun n : ℕ => (n : ℝ)) =O[atTop] (fun n : ℕ => (⌊(n : ℝ)⌋₊ : ℝ)) :=
    (h_equiv.symm.isBigO.comp_tendsto tendsto_natCast_atTop_atTop).congr (by simp) (by simp)
  exact ⟨by unfold isBigO; exact hO, by unfold isBigOmega; exact hΩ⟩

theorem isBigTheta_nat_ceil_coerce : isBigTheta (fun n : ℕ => (⌈(n : ℝ)⌉₊ : ℝ)) (fun n : ℕ => (n : ℝ)) := by
  have h_equiv : (fun x : ℝ => (⌈x⌉₊ : ℝ)) ~[atTop] (fun x : ℝ => x) := isEquivalent_nat_ceil
  have hO : (fun n : ℕ => (⌈(n : ℝ)⌉₊ : ℝ)) =O[atTop] (fun n : ℕ => (n : ℝ)) :=
    (h_equiv.isBigO.comp_tendsto tendsto_natCast_atTop_atTop).congr (by simp) (by simp)
  have hΩ : (fun n : ℕ => (n : ℝ)) =O[atTop] (fun n : ℕ => (⌈(n : ℝ)⌉₊ : ℝ)) :=
    (h_equiv.symm.isBigO.comp_tendsto tendsto_natCast_atTop_atTop).congr (by simp) (by simp)
  exact ⟨by unfold isBigO; exact hO, by unfold isBigOmega; exact hΩ⟩

private theorem self_le_four_mul_div_two_nat {n : ℕ} (hn : 2 ≤ n) :
    n ≤ 4 * (n / 2) := by
  have hpos : 0 < n / 2 := Nat.div_pos hn (by decide)
  have hmod_lt : n % 2 < 2 := Nat.mod_lt n (by decide)
  have hdecomp : 2 * (n / 2) + n % 2 = n := Nat.div_add_mod n 2
  omegaprivate theorem ceil_half_le_self_nat {n : ℕ} (hn : 1 ≤ n) :
    (n + 1) / 2 ≤ n := by
  omega

private theorem self_le_two_mul_ceil_half_nat (n : ℕ) :
    n ≤ 2 * ((n + 1) / 2) := by
  have hmod_lt : (n + 1) % 2 < 2 := Nat.mod_lt (n + 1) (by decide)
  have hdecomp : 2 * ((n + 1) / 2) + (n + 1) % 2 = n + 1 :=
    Nat.div_add_mod (n + 1) 2
  omega

Natural-number floor half-scale: ⌊n/2⌋ = Θ(n).


theorem isBigTheta_nat_floor_half_coerce :
    isBigTheta (fun n : ℕ => ((n / 2 : ℕ) : ℝ)) (fun n : ℕ => (n : ℝ)) := by
  constructor
  · rw [isBigO_iff]
    refine ⟨1, by norm_num, 0, ?_⟩
    intro n _hn
    have hnat : n / 2 ≤ n := Nat.div_le_self n 2
    have hreal : ((n / 2 : ℕ) : ℝ) ≤ (n : ℝ) := by exact_mod_cast hnat
    simpa using hreal
  · change isBigO (fun n : ℕ => (n : ℝ)) (fun n : ℕ => ((n / 2 : ℕ) : ℝ))
    rw [isBigO_iff]
    refine ⟨4, by norm_num, 2, ?_⟩
    intro n hn
    have hnat : n ≤ 4 * (n / 2) := self_le_four_mul_div_two_nat hn
    have hreal : (n : ℝ) ≤ 4 * ((n / 2 : ℕ) : ℝ) := by exact_mod_cast hnat
    simpa using hreal

Natural-number ceiling half-scale, represented as (n+1)/2: ⌈n/2⌉ = Θ(n).


theorem isBigTheta_nat_ceil_half_coerce :
    isBigTheta (fun n : ℕ => (((n + 1) / 2 : ℕ) : ℝ)) (fun n : ℕ => (n : ℝ)) := by
  constructor
  · rw [isBigO_iff]
    refine ⟨1, by norm_num, 1, ?_⟩
    intro n hn
    have hnat : (n + 1) / 2 ≤ n := ceil_half_le_self_nat hn
    have hreal : (((n + 1) / 2 : ℕ) : ℝ) ≤ (n : ℝ) := by exact_mod_cast hnat
    simpa using hreal
  · change isBigO (fun n : ℕ => (n : ℝ)) (fun n : ℕ => (((n + 1) / 2 : ℕ) : ℝ))
    rw [isBigO_iff]
    refine ⟨2, by norm_num, 0, ?_⟩
    intro n _hn
    have hnat : n ≤ 2 * ((n + 1) / 2) := self_le_two_mul_ceil_half_nat n
    have hreal : (n : ℝ) ≤ 2 * ((((n + 1) / 2 : ℕ) : ℝ)) := by exact_mod_cast hnat
    simpa using hreal

Factorial bound

n! ≤ nⁿ for all n. Proof on ℕ: each factor 1..n ≤ n.

theorem factorial_upper_bound_nat (n : ℕ) : Nat.factorial n ≤ n ^ n := by
  exact Nat.factorial_le_pow n

n! ≤ nⁿ for all n, real version.

theorem factorial_upper_bound (n : ℕ) : (Nat.factorial n : ℝ) ≤ (n : ℝ) ^ n := by
  exact_mod_cast factorial_upper_bound_nat n

For any offset m, the last k factors in (m+k)! are each at least m+1, so (m+1)^k ≤ (m+k)!.

theorem factorial_lower_bound_offset_nat (m k : ℕ) :
    (m + 1) ^ k ≤ Nat.factorial (m + k) := by
  have h := Nat.factorial_mul_pow_le_factorial (m := m) (n := k)
  have hle : (m + 1) ^ k ≤ Nat.factorial m * (m + 1) ^ k :=
    Nat.le_mul_of_pos_left ((m + 1) ^ k) (Nat.factorial_pos m)
  exact le_trans hle h

Real-valued version of factorial_lower_bound_offset_nat.

theorem factorial_lower_bound_offset (m k : ℕ) :
    ((m + 1 : ℕ) : ℝ) ^ k ≤ (Nat.factorial (m + k) : ℝ) := by
  exact_mod_cast factorial_lower_bound_offset_nat m k

A CLRS-style half-scale lower bound: the upper half of the factors in n! contributes at least (⌊n/2⌋+1)^(n-⌊n/2⌋).

theorem factorial_lower_bound_half_pow_nat (n : ℕ) :
    (n / 2 + 1) ^ (n - n / 2) ≤ Nat.factorial n := by
  have h := factorial_lower_bound_offset_nat (m := n / 2) (k := n - n / 2)
  have hsum : n / 2 + (n - n / 2) = n :=
    Nat.add_sub_of_le (Nat.div_le_self n 2)
  simpa [hsum] using h

Real-valued version of factorial_lower_bound_half_pow_nat.

theorem factorial_lower_bound_half_pow (n : ℕ) :
    (((n / 2 + 1 : ℕ) : ℝ) ^ (n - n / 2)) ≤ (Nat.factorial n : ℝ) := by
  exact_mod_cast factorial_lower_bound_half_pow_nat n

Exponential vs factorial

aⁿ = o(n!) as n → ∞. Follows from FloorSemiring.tendsto_pow_div_factorial_atTop, the standard lemma that cⁿ / n! → 0 for any real c.


theorem isLittleO_exp_vs_factorial (a : ℝ) :
    isLittleO (fun n : ℕ => a ^ n) (fun n : ℕ => (Nat.factorial n : ℝ)) := by
  -- The key lemma: a^n / n! → 0 as n → ∞ (standard result in mathlib)
  have h_tendsto : Tendsto (fun n : ℕ => a ^ n / ((Nat.factorial n : ℕ) : ℝ)) atTop (𝓝 0) := by
    -- FloorSemiring.tendsto_pow_div_factorial_atTop gives a^n / n! → 0 in ℝ
    -- where n! is the ℝ factorial via the factorial notation {lit}`n !`
    simpa using FloorSemiring.tendsto_pow_div_factorial_atTop (K := ℝ) a
  -- Use isLittleO_iff_tendsto: f =o[atTop] g  ↔  f/g → 0  (when g=0 → f=0)
  have h_cond : ∀ n : ℕ, ((Nat.factorial n : ℝ) = 0) → a ^ n = 0 := by
    intro n hn
    have hpos : 0 < (Nat.factorial n : ℝ) := by exact_mod_cast Nat.factorial_pos n
    linarith
  unfold isLittleO
  rw [isLittleO_iff_tendsto h_cond]
  exact h_tendsto

CLRS standard growth-table fact: n! = o(nⁿ).


theorem isLittleO_factorial_pow_self :
    isLittleO (fun n : ℕ => (Nat.factorial n : ℝ)) (fun n : ℕ => (n : ℝ) ^ n) := by
  have h_tendsto :
      Tendsto (fun n : ℕ => (Nat.factorial n : ℝ) / ((n : ℝ) ^ n)) atTop (𝓝 0) := by
    simpa using tendsto_factorial_div_pow_self_atTop
  have h_cond : ∀ n : ℕ, ((n : ℝ) ^ n = 0) → (Nat.factorial n : ℝ) = 0 := by
    intro n hn
    exfalso
    have hpow_pos : 0 < (n : ℝ) ^ n := by
      cases n with
      | zero => norm_num
      | succ k => positivity
    exact (ne_of_gt hpow_pos) hn
  unfold isLittleO
  rw [isLittleO_iff_tendsto h_cond]
  exact h_tendsto

Log-factorial asymptotics (Stirling)

Theorem (log-factorial is Θ(n log n)). log(n!) = Θ(n log n). CLRS equation (3.19). Upper bound: n! ≤ n^n. Lower bound: Mathlib's Stirling approximation le_log_factorial_stirling.


theorem isBigTheta_log_factorial :
    isBigTheta (fun n : ℕ => Real.log (Nat.factorial n : ℝ))
      (fun n : ℕ => (n : ℝ) * Real.log (n : ℝ)) := by
  constructor
  · rw [isBigO_iff]
    refine ⟨1, by norm_num, 0, ?_⟩
    intro n _
    by_cases hn : n = 0
    · subst n; simp
    · have h_fact_le : (Nat.factorial n : ℝ) ≤ (n : ℝ) ^ n := by
        exact_mod_cast factorial_upper_bound_nat n
      have h_log : Real.log (Nat.factorial n : ℝ) ≤ Real.log ((n : ℝ) ^ n) :=
        Real.log_le_log (by exact_mod_cast Nat.factorial_pos n) h_fact_le
      rw [Real.log_pow] at h_log
      have h_nonneg : 0 ≤ Real.log (Nat.factorial n : ℝ) :=
        Real.log_nonneg (by exact_mod_cast Nat.factorial_pos n)
      calc
        |Real.log (Nat.factorial n : ℝ)| = Real.log (Nat.factorial n : ℝ) := abs_of_nonneg h_nonneg
        _ ≤ (n : ℝ) * Real.log (n : ℝ) := h_log
        _ = 1 * |(n : ℝ) * Real.log (n : ℝ)| := by
          have hn_nonneg : 0 ≤ (n : ℝ) := by exact_mod_cast Nat.zero_le n
          have hlog_nonneg : 0 ≤ Real.log (n : ℝ) :=
            Real.log_nonneg (by exact_mod_cast (Nat.one_le_of_lt (Nat.pos_of_ne_zero hn)))
          rw [abs_mul, abs_of_nonneg hn_nonneg, abs_of_nonneg hlog_nonneg]; ring
  · rw [isBigOmega_iff]
    refine ⟨1/2, by norm_num, 8, ?_⟩
    intro n hn8
    have hn0 : n ≠ 0 := by omega
    have hstirling := le_log_factorial_stirling hn0
    have h_log_n_ge_two : (2 : ℝ) ≤ Real.log (n : ℝ) := by
      have h_exp2_lt_8 : Real.exp (2 : ℝ) < 8 := by
        calc
          Real.exp (2 : ℝ) = Real.exp ((1 : ℝ) + (1 : ℝ)) := by norm_num
          _ = Real.exp 1 * Real.exp 1 := by rw [Real.exp_add]
          _ < 2.7182818286 * 2.7182818286 := by
            nlinarith [Real.exp_one_lt_d9, Real.exp_one_gt_d9]
          _ < 8 := by norm_num
      have h_log_exp2_lt_log8 : Real.log (Real.exp (2 : ℝ)) < Real.log (8 : ℝ) :=
        Real.log_lt_log (Real.exp_pos _) h_exp2_lt_8
      rw [Real.log_exp (2 : ℝ)] at h_log_exp2_lt_log8
      have hlog8le : Real.log (8 : ℝ) ≤ Real.log (n : ℝ) :=
        Real.log_le_log (by norm_num) (by exact_mod_cast hn8)
      linarith
    have hn_nonneg : 0 ≤ (n : ℝ) := by exact_mod_cast Nat.zero_le n
    have h_log_nonneg : 0 ≤ Real.log (n : ℝ) := by linarith
    have h_fact_ge_one : 1 ≤ (Nat.factorial n : ℝ) := by
      have h : 1 ≤ Nat.factorial n := Nat.succ_le_of_lt (Nat.factorial_pos n)
      exact_mod_cast h
    calc
      |Real.log (Nat.factorial n : ℝ)| = Real.log (Nat.factorial n : ℝ) :=
        abs_of_nonneg (Real.log_nonneg h_fact_ge_one)
      _ ≥ (n : ℝ) * Real.log (n : ℝ) - (n : ℝ) + Real.log (n : ℝ) / 2 +
          Real.log (2 * Real.pi) / 2 := hstirling
      _ ≥ (n : ℝ) * Real.log (n : ℝ) - (n : ℝ) := by
        have h_rem_nonneg : 0 ≤ Real.log (n : ℝ) / 2 + Real.log (2 * Real.pi) / 2 := by
          have h1 : 0 ≤ Real.log (n : ℝ) / 2 := div_nonneg (by linarith) (by norm_num)
          have h2 : 0 ≤ Real.log (2 * Real.pi) / 2 := by
            have h2pi_ge_one : 1 ≤ 2 * Real.pi := by
              have hpi_gt_one : (1 : ℝ) < Real.pi := by linarith [Real.pi_gt_three]
              nlinarith
            exact div_nonneg (Real.log_nonneg h2pi_ge_one) (by norm_num)
          linarith
        linarith
      _ ≥ ((n : ℝ) * Real.log (n : ℝ)) / 2 := by
        have : (n : ℝ) ≤ ((n : ℝ) * Real.log (n : ℝ)) / 2 := by nlinarith
        linarith
      _ = (1/2 : ℝ) * |(n : ℝ) * Real.log (n : ℝ)| := by
        rw [abs_mul, abs_of_nonneg hn_nonneg, abs_of_nonneg h_log_nonneg]; ring

Logarithm base change

Changing the base of a logarithm only changes its value by a constant factor. For any base b > 1, log n = Θ(log_b n).


theorem isBigTheta_log_logb {b : ℝ} (hb : 1 < b) :
    isBigTheta (fun n : ℕ => Real.log (n : ℝ))
      (fun n : ℕ => Real.logb b (n : ℝ)) := by
  have hlogb_pos : 0 < Real.log b := Real.log_pos hb
  have hlogb_ne_zero : Real.log b ≠ 0 := by linarith
  constructor
  · rw [isBigO_iff]
    refine ⟨Real.log b, hlogb_pos, 1, ?_⟩
    intro n hn
    have hnpos : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
    have hlog_nonneg : 0 ≤ Real.log (n : ℝ) := Real.log_nonneg hnpos
    rw [Real.logb, abs_of_nonneg hlog_nonneg,
      abs_of_nonneg (div_nonneg hlog_nonneg hlogb_pos.le)]
    have h : Real.log b * (Real.log (n : ℝ) / Real.log b) = Real.log (n : ℝ) := by
      field_simp [hlogb_ne_zero]
    rw [h]
  · rw [isBigOmega_iff]
    refine ⟨(Real.log b) / 2, half_pos hlogb_pos, 2, ?_⟩
    intro n hn
    have hn1real : (1 : ℝ) ≤ (n : ℝ) := by exact mod_cast (show (1 : ℕ) ≤ n from by omega)
    have hnpos : (0 : ℝ) ≤ Real.log (n : ℝ) := Real.log_nonneg hn1real
    rw [Real.logb, abs_of_nonneg hnpos,
      abs_of_nonneg (div_nonneg hnpos hlogb_pos.le)]
    have h_simp : (Real.log b) / 2 * (Real.log (n : ℝ) / Real.log b) =
        Real.log (n : ℝ) / 2 := by
      field_simp [hlogb_ne_zero]
    rw [h_simp]
    linarith

The logarithm grows without bound: 1 = o(log n).

theorem isLittleO_one_log :
    isLittleO (fun _ : ℕ => (1 : ℝ)) (fun n : ℕ => Real.log (n : ℝ)) := by
  unfold isLittleO
  exact (isLittleO_const_log_atTop (c := 1)).comp_tendsto tendsto_natCast_atTop_atTop

Completing the CLRS 3.2 comparison table

The lemmas below fill in the remaining adjacent comparisons of the CLRS 3.2 growth hierarchy

1 ≺ log (log n) ≺ log n ≺ n ≺ nᵃ ≺ 2ⁿ ≺ n!,

together with the base-change facts for log_b.

Logarithms grow slower than the identity: log n = o(n). This is the log n ≺ n row of the CLRS 3.2 growth hierarchy.

theorem isLittleO_log_id :
    isLittleO (fun n : ℕ => Real.log (n : ℝ)) (fun n : ℕ => (n : ℝ)) := by
  unfold isLittleO
  simpa [Function.comp_def, id_eq] using
    Real.isLittleO_log_id_atTop.comp_tendsto tendsto_natCast_atTop_atTop

The doubly-iterated logarithm is dominated by the logarithm: log (log n) = o(log n). This is the log (log n) ≺ log n row of the CLRS 3.2 hierarchy.

theorem isLittleO_loglog_log :
    isLittleO (fun n : ℕ => Real.log (Real.log (n : ℝ)))
      (fun n : ℕ => Real.log (n : ℝ)) := by
  unfold isLittleO
  have h :=
    (Real.isLittleO_log_id_atTop.comp_tendsto Real.tendsto_log_atTop).comp_tendsto
      tendsto_natCast_atTop_atTop
  simpa [Function.comp_def, id_eq] using h

Any fixed polynomial is dominated by the base-2 exponential: nᵃ = o(2ⁿ). The canonical CLRS 3.2 exponential comparison; instance of isLittleO_pow_const_exp at base c = 2.

theorem isLittleO_pow_two_pow (a : ℕ) :
    isLittleO (fun n : ℕ => (n : ℝ) ^ a) (fun n : ℕ => (2 : ℝ) ^ n) :=
  isLittleO_pow_const_exp (a := a) (by norm_num : (1 : ℝ) < 2)

The base-2 exponential is dominated by the factorial: 2ⁿ = o(n!). Equivalently n! = ω(2ⁿ) (CLRS 3.2).

theorem isLittleO_two_pow_factorial :
    isLittleO (fun n : ℕ => (2 : ℝ) ^ n) (fun n : ℕ => (Nat.factorial n : ℝ)) :=
  isLittleO_exp_vs_factorial 2

The factorial dominates every exponential in the Ω sense: n! = Ω(cⁿ) for every base c. CLRS 3.2 (n! = ω(2ⁿ)).

theorem isBigOmega_factorial_exp (c : ℝ) :
    isBigOmega (fun n : ℕ => (Nat.factorial n : ℝ)) (fun n : ℕ => c ^ n) := by
  unfold isBigOmega
  have h : (fun n : ℕ => c ^ n) =o[atTop] (fun n : ℕ => (Nat.factorial n : ℝ)) :=
    isLittleO_exp_vs_factorial c
  exact h.isBigO

Every fixed polynomial is dominated by the factorial: nᵃ = o(n!). Obtained by chaining nᵃ = o(2ⁿ) and 2ⁿ = o(n!). CLRS 3.2.

theorem isLittleO_pow_factorial (a : ℕ) :
    isLittleO (fun n : ℕ => (n : ℝ) ^ a) (fun n : ℕ => (Nat.factorial n : ℝ)) := by
  have h1 : (fun n : ℕ => (n : ℝ) ^ a) =o[atTop] (fun n : ℕ => (2 : ℝ) ^ n) :=
    isLittleO_pow_two_pow a
  have h2 : (fun n : ℕ => (2 : ℝ) ^ n) =o[atTop]
      (fun n : ℕ => (Nat.factorial n : ℝ)) := isLittleO_two_pow_factorial
  unfold isLittleO
  exact h1.trans_isBigO h2.isBigO

Base change is a Θ-preserving operation: log_b n = Θ(log n) for b > 1. This is the companion of isBigTheta_log_logb with the two functions swapped. CLRS 3.2.

theorem isBigTheta_logb_log {b : ℝ} (hb : 1 < b) :
    isBigTheta (fun n : ℕ => Real.logb b (n : ℝ)) (fun n : ℕ => Real.log (n : ℝ)) :=
  isBigTheta_symm (isBigTheta_log_logb hb)

The base-b logarithm is dominated by any positive real power: log_b n = o(nʳ) for b > 1 and 0 < r. CLRS 3.2 (log_b n vs nᶜ).

theorem isLittleO_logb_rpow {b r : ℝ} (hb : 1 < b) (hr : 0 < r) :
    isLittleO (fun n : ℕ => Real.logb b (n : ℝ)) (fun n : ℕ => (n : ℝ) ^ r) := by
  have hO : (fun n : ℕ => Real.logb b (n : ℝ)) =O[atTop]
      (fun n : ℕ => Real.log (n : ℝ)) := (isBigTheta_logb_log hb).1
  have ho : (fun n : ℕ => Real.log (n : ℝ)) =o[atTop] (fun n : ℕ => (n : ℝ) ^ r) :=
    isLittleO_log_rpow hr
  unfold isLittleO
  exact hO.trans_isLittleO ho

Every fixed power of the logarithm is dominated by any exponential with base c > 1: (log n)ᵃ = o(cⁿ). Chains (log n)ᵃ = o(n) and n = o(cⁿ). CLRS 3.2 (polylogarithm vs exponential).


theorem isLittleO_log_pow_const_exp {a : ℕ} {c : ℝ} (hc : 1 < c) :
    isLittleO (fun n : ℕ => Real.log (n : ℝ) ^ a) (fun n : ℕ => c ^ n) := by
  have h1 : (fun n : ℕ => Real.log (n : ℝ) ^ a) =o[atTop] (fun n : ℕ => (n : ℝ)) := by
    have h := isLittleO_log_pow_rpow (a := a) (r := 1) (by norm_num)
    unfold isLittleO at h
    simpa using h
  have h2 : (fun n : ℕ => (n : ℝ)) =o[atTop] (fun n : ℕ => c ^ n) := by
    have h := isLittleO_pow_const_exp (a := 1) hc
    unfold isLittleO at h
    simpa using h
  unfold isLittleO
  exact h1.trans_isBigO h2.isBigO

Fibonacci-number growth (CLRS §3.3)

CLRS §3.3 closes with the Fibonacci numbers and two growth facts: the golden-ratio closed form eq (3.25) and eq (3.26), which states that Fₙ is the closest integer to φⁿ/√5, hence Fₙ = Θ(φⁿ). Mathlib supplies Binet's formula Real.coe_fib_eq and the golden-ratio arithmetic; the lemmas below restate them under the CLRS asymptotic wrappers. Here φ = (1+√5)/2 is Real.goldenRatio and ψ = (1−√5)/2 is Real.goldenConj.

              private theorem sqrt5_pos : (0 : ℝ) < Real.sqrt 5 := Real.sqrt_pos.mpr (by norm_num)private theorem two_lt_sqrt5 : (2 : ℝ) < Real.sqrt 5 := by
  nlinarith [Real.sq_sqrt (show (0 : ℝ) ≤ 5 by norm_num), Real.sqrt_nonneg 5]private theorem sqrt5_le_nine_quarters : Real.sqrt 5 ≤ 9 / 4 := by
  nlinarith [Real.sq_sqrt (show (0 : ℝ) ≤ 5 by norm_num), Real.sqrt_nonneg 5]

The conjugate golden ratio satisfies |ψ| ≤ 1, hence |ψⁿ| ≤ 1.


private theorem abs_goldenConj_pow_le_one (n : ℕ) : |Real.goldenConj ^ n| ≤ 1 := by
  rw [abs_pow]
  apply pow_le_one₀ (abs_nonneg _)
  rw [abs_le]
  exact ⟨Real.neg_one_lt_goldenConj.le, by linarith [Real.goldenConj_neg]⟩

CLRS equation (3.25) — Binet's closed form. The n-th Fibonacci number equals (φⁿ − ψⁿ)/√5. This is a thin CLRS-facing restatement of Mathlib's Real.coe_fib_eq.

theorem coe_fib_closed_form (n : ℕ) :
    (Nat.fib n : ℝ) = (Real.goldenRatio ^ n - Real.goldenConj ^ n) / Real.sqrt 5 :=
  Real.coe_fib_eq n

CLRS equation (3.26) — Fibonacci exponential growth. The Fibonacci numbers grow like the golden ratio: Fₙ = Θ(φⁿ). Proof: from Binet's formula, √5·Fₙ = φⁿ − ψⁿ; since |ψ| < 1 < φ the ψⁿ term is negligible, so Fₙ ≤ φⁿ (upper bound) and (1/5)·φⁿ ≤ Fₙ for n ≥ 2 (lower bound).


theorem isBigTheta_fib_goldenRatio :
    isBigTheta (fun n : ℕ => (Nat.fib n : ℝ)) (fun n : ℕ => Real.goldenRatio ^ n) := by
  have hφ0 : ∀ n : ℕ, (0 : ℝ) ≤ Real.goldenRatio ^ n :=
    fun n => pow_nonneg Real.goldenRatio_pos.le n
  have hφ1 : ∀ n : ℕ, (1 : ℝ) ≤ Real.goldenRatio ^ n :=
    fun n => one_le_pow₀ Real.one_lt_goldenRatio.le
  have hnegψ : ∀ n : ℕ, -(Real.goldenConj ^ n) ≤ Real.goldenRatio ^ n := by
    intro n
    have h := (abs_le.mp (abs_goldenConj_pow_le_one n)).1
    linarith [hφ1 n]
  constructor
  · -- Upper bound: `Fₙ ≤ φⁿ`, so `Fₙ = O(φⁿ)`.
    rw [isBigO_iff]
    refine ⟨1, one_pos, 0, ?_⟩
    intro n _
    show |(Nat.fib n : ℝ)| ≤ 1 * |Real.goldenRatio ^ n|
    have hbound : (Nat.fib n : ℝ) ≤ Real.goldenRatio ^ n := by
      rw [Real.coe_fib_eq n, div_le_iff₀ sqrt5_pos]
      nlinarith [hnegψ n, hφ0 n, two_lt_sqrt5,
        mul_nonneg (hφ0 n) (show (0 : ℝ) ≤ Real.sqrt 5 - 2 by linarith [two_lt_sqrt5])]
    rw [abs_of_nonneg (by positivity : (0 : ℝ) ≤ (Nat.fib n : ℝ)),
        abs_of_nonneg (hφ0 n), one_mul]
    exact hbound
  · -- Lower bound: `(1/5)·φⁿ ≤ Fₙ` for `n ≥ 2`, so `Fₙ = Ω(φⁿ)`.
    rw [isBigOmega_iff]
    refine ⟨1 / 5, by norm_num, 2, ?_⟩
    intro n hn
    show (1 / 5 : ℝ) * |Real.goldenRatio ^ n| ≤ |(Nat.fib n : ℝ)|
    have hφn2 : (2 : ℝ) ≤ Real.goldenRatio ^ n := by
      have h2n : Real.goldenRatio ^ 2 ≤ Real.goldenRatio ^ n :=
        pow_le_pow_right₀ Real.one_lt_goldenRatio.le hn
      nlinarith [Real.one_lt_goldenRatio, h2n, Real.goldenRatio_sq]
    have hψle : Real.goldenConj ^ n ≤ 1 := (abs_le.mp (abs_goldenConj_pow_le_one n)).2
    have hbound : (1 / 5 : ℝ) * Real.goldenRatio ^ n ≤ (Nat.fib n : ℝ) := by
      rw [Real.coe_fib_eq n, le_div_iff₀ sqrt5_pos]
      nlinarith [hφn2, hψle, sqrt5_le_nine_quarters,
        mul_nonneg (hφ0 n)
          (show (0 : ℝ) ≤ 9 / 4 - Real.sqrt 5 by linarith [sqrt5_le_nine_quarters])]
    rw [abs_of_nonneg (hφ0 n), abs_of_nonneg (by positivity : (0 : ℝ) ≤ (Nat.fib n : ℝ))]
    exact hbound

CLRS equation (3.26) — closest-integer bound. Fₙ is the closest integer to φⁿ/√5: |φⁿ/√5 − Fₙ| < 1/2. The error is exactly |ψⁿ|/√5 ≤ 1/√5, which is below 1/2 because √5 > 2.


theorem goldenRatio_pow_div_sqrt5_sub_fib_abs_lt_half (n : ℕ) :
    |Real.goldenRatio ^ n / Real.sqrt 5 - (Nat.fib n : ℝ)| < 1 / 2 := by
  have hkey : Real.goldenRatio ^ n / Real.sqrt 5 - (Nat.fib n : ℝ)
      = Real.goldenConj ^ n / Real.sqrt 5 := by
    rw [Real.coe_fib_eq n]; ring
  rw [hkey, abs_div, abs_of_pos sqrt5_pos, div_lt_iff₀ sqrt5_pos]
  nlinarith [abs_goldenConj_pow_le_one n, two_lt_sqrt5]

Exponential envelope (upper): for any base c > φ, Fₙ = o(cⁿ). Chains Fₙ = O(φⁿ) with φⁿ = o(cⁿ).

theorem isLittleO_fib_exp {c : ℝ} (hc : Real.goldenRatio < c) :
    isLittleO (fun n : ℕ => (Nat.fib n : ℝ)) (fun n : ℕ => c ^ n) := by
  have hO : (fun n : ℕ => (Nat.fib n : ℝ)) =O[atTop] (fun n : ℕ => Real.goldenRatio ^ n) :=
    isBigTheta_fib_goldenRatio.1
  have ho : (fun n : ℕ => Real.goldenRatio ^ n) =o[atTop] (fun n : ℕ => c ^ n) :=
    isLittleO_exp_exp_of_lt Real.goldenRatio_pos.le hc
  unfold isLittleO
  exact hO.trans_isLittleO ho

Exponential envelope (lower): for any base 0 ≤ c < φ, cⁿ = o(Fₙ). Chains cⁿ = o(φⁿ) with φⁿ = O(Fₙ).

theorem isLittleO_exp_fib {c : ℝ} (hc0 : 0 ≤ c) (hc : c < Real.goldenRatio) :
    isLittleO (fun n : ℕ => c ^ n) (fun n : ℕ => (Nat.fib n : ℝ)) := by
  have hΩ : (fun n : ℕ => Real.goldenRatio ^ n) =O[atTop] (fun n : ℕ => (Nat.fib n : ℝ)) :=
    isBigTheta_fib_goldenRatio.2
  have ho : (fun n : ℕ => c ^ n) =o[atTop] (fun n : ℕ => Real.goldenRatio ^ n) :=
    isLittleO_exp_exp_of_lt hc0 hc
  unfold isLittleO
  exact ho.trans_isBigO hΩ

Iterated logarithm `lg*` (CLRS §3.3)

CLRS §3.3 defines the iterated logarithm lg* n = min { i ≥ 0 : lg⁽ⁱ⁾ n ≤ 1 }, the number of times lg must be applied before the result drops to ≤ 1, and stresses how extraordinarily slowly it grows. Mathlib has no iterated logarithm (only Nat.log/Nat.clog), so we define lgStar by well-founded recursion on ℕ, base 2, then prove the recurrence, monotonicity, and the o(log n) slow-growth bound.

The base-2 iterated logarithm lg* n (CLRS §3.3 definition): the number of times base-2 Nat.log must be applied to n before reaching ≤ 1. Defined by well-founded recursion; the recursive argument Nat.log 2 n is strictly smaller than n for n ≥ 2.

def lgStar (n : ℕ) : ℕ :=
  if h : n ≤ 1 then 0 else 1 + lgStar (Nat.log 2 n)
termination_by n
decreasing_by exact Nat.log_lt_self 2 (by omega)

Base case: lg* n = 0 for n ≤ 1.


theorem lgStar_of_le_one {n : ℕ} (h : n ≤ 1) : lgStar n = 0 := by
  conv_lhs => rw [lgStar]
  rw [dif_pos h]

One-step recurrence: lg* n = 1 + lg* (log₂ n) for n ≥ 2.


theorem lgStar_of_two_le {n : ℕ} (h : 2 ≤ n) : lgStar n = 1 + lgStar (Nat.log 2 n) := by
  conv_lhs => rw [lgStar]
  rw [dif_neg (by omega : ¬ n ≤ 1)]

lg* 0 = 0.

theorem lgStar_zero : lgStar 0 = 0 := lgStar_of_le_one (by norm_num)

lg* 1 = 0.

theorem lgStar_one : lgStar 1 = 0 := lgStar_of_le_one (le_refl 1)

lg* 2 = 1.


theorem lgStar_two : lgStar 2 = 1 := by
  have hl : Nat.log 2 2 = 1 := by decide
  rw [lgStar_of_two_le (le_refl 2), hl, lgStar_of_le_one (le_refl 1)]

Tower recurrence (CLRS §3.3). For n ≥ 1, lg* (2ⁿ) = 1 + lg* n: each extra power-of-two "tower level" adds exactly one to the iterated logarithm.


theorem lgStar_two_pow {n : ℕ} (hn : 1 ≤ n) : lgStar (2 ^ n) = 1 + lgStar n := by
  have h2 : 2 ≤ 2 ^ n := by
    calc (2 : ℕ) = 2 ^ 1 := (pow_one 2).symm
      _ ≤ 2 ^ n := Nat.pow_le_pow_right (by norm_num) hn
  rw [lgStar_of_two_le h2, Nat.log_pow (by norm_num)]

lg* is monotone (nondecreasing). Proved by strong induction: for a ≤ b with b ≥ 2, log₂ is monotone and strictly decreasing, so the recurrence lg* b = 1 + lg* (log₂ b) reduces to the smaller instance.


theorem lgStar_monotone : Monotone lgStar := by
  have key : ∀ b, ∀ a, a ≤ b → lgStar a ≤ lgStar b := by
    intro b
    induction b using Nat.strongRecOn with
    | ind b ih =>
      intro a ha
      by_cases hb : b ≤ 1
      · rw [lgStar_of_le_one (le_trans ha hb), lgStar_of_le_one hb]
      · by_cases haa : a ≤ 1
        · rw [lgStar_of_le_one haa]; exact Nat.zero_le _
        · rw [lgStar_of_two_le (by omega : 2 ≤ a), lgStar_of_two_le (by omega : 2 ≤ b)]
          have hlog : Nat.log 2 a ≤ Nat.log 2 b := Nat.log_mono_right ha
          have hb_lt : Nat.log 2 b < b := Nat.log_lt_self 2 (by omega)
          exact Nat.add_le_add_left (ih (Nat.log 2 b) hb_lt (Nat.log 2 a) hlog) 1
  intro a b hab
  exact key b a hab

Slow-growth bound: lg* n ≤ log₂ n + 1 for every n. Proved by strong induction using log₂ (log₂ n) < log₂ n.


theorem lgStar_le_log_add_one : ∀ n, lgStar n ≤ Nat.log 2 n + 1 := by
  intro n
  induction n using Nat.strongRecOn with
  | ind n ih =>
    by_cases hn : n ≤ 1
    · rw [lgStar_of_le_one hn]; exact Nat.zero_le _
    · rw [lgStar_of_two_le (by omega : 2 ≤ n)]
      have hlog_ge1 : 1 ≤ Nat.log 2 n := Nat.log_pos (by norm_num) (by omega)
      have hloglog_lt : Nat.log 2 (Nat.log 2 n) < Nat.log 2 n :=
        Nat.log_lt_self 2 (by omega)
      have hIH := ih (Nat.log 2 n) (Nat.log_lt_self 2 (by omega))
      omega

Every base-2 integer logarithm is bounded by twice the real logarithm: log₂ m ≤ 2·log m for m ≥ 1. From 2^(log₂ m) ≤ m and log 2 > 1/2.


theorem natLog_two_le_two_log {m : ℕ} (hm : 1 ≤ m) :
    (Nat.log 2 m : ℝ) ≤ 2 * Real.log (m : ℝ) := by
  have h1 : (2 : ℕ) ^ Nat.log 2 m ≤ m := Nat.pow_log_le_self 2 (by omega)
  have h2 : ((2 : ℝ)) ^ Nat.log 2 m ≤ (m : ℝ) := by exact_mod_cast h1
  have h3 : Real.log ((2 : ℝ) ^ Nat.log 2 m) ≤ Real.log (m : ℝ) :=
    Real.log_le_log (by positivity) h2
  rw [Real.log_pow] at h3
  have hcast : (0 : ℝ) ≤ (Nat.log 2 m : ℝ) := by positivity
  nlinarith [h3, hcast, Real.log_two_gt_d9,
    mul_nonneg hcast (show (0 : ℝ) ≤ Real.log 2 - 0.5 by linarith [Real.log_two_gt_d9])]

Extreme slow growth (CLRS §3.3). The iterated logarithm is o(log n): lg* n = o(log n), placing it below log n in the growth hierarchy. Proof: lg* n ≤ log₂(log₂ n) + 2 ≤ 2·log 2 + 2·log(log n) + 2 for n ≥ 4, so lg* n = O(1 + log(log n)), and 1 + log(log n) = o(log n) by isLittleO_one_log and isLittleO_loglog_log.


theorem isLittleO_lgStar_log :
    isLittleO (fun n : ℕ => (lgStar n : ℝ)) (fun n : ℕ => Real.log (n : ℝ)) := by
  have hdom : (fun n : ℕ => (1 : ℝ) + Real.log (Real.log (n : ℝ))) =o[atTop]
      (fun n : ℕ => Real.log (n : ℝ)) := by
    have hone : (fun _ : ℕ => (1 : ℝ)) =o[atTop] (fun n : ℕ => Real.log (n : ℝ)) :=
      isLittleO_one_log
    have hll : (fun n : ℕ => Real.log (Real.log (n : ℝ))) =o[atTop]
        (fun n : ℕ => Real.log (n : ℝ)) := isLittleO_loglog_log
    exact hone.add hll
  have hO : (fun n : ℕ => (lgStar n : ℝ)) =O[atTop]
      (fun n : ℕ => (1 : ℝ) + Real.log (Real.log (n : ℝ))) := by
    rw [Asymptotics.isBigO_iff]
    refine ⟨2 * Real.log 2 + 4, ?_⟩
    filter_upwards [Filter.eventually_ge_atTop 4] with n hn
    show ‖(lgStar n : ℝ)‖ ≤
      (2 * Real.log 2 + 4) * ‖(1 : ℝ) + Real.log (Real.log (n : ℝ))‖
    have hlog2pos : (0 : ℝ) < Real.log 2 := Real.log_pos (by norm_num)
    have hn1 : 1 ≤ n := by omega
    have hn2 : 2 ≤ n := by omega
    have hlogn_ge1 : (1 : ℝ) ≤ Real.log (n : ℝ) := by
      have h4 : Real.log 4 ≤ Real.log (n : ℝ) :=
        Real.log_le_log (by norm_num) (by exact_mod_cast hn)
      have h4' : (1 : ℝ) ≤ Real.log 4 := by
        rw [show (4 : ℝ) = 2 ^ 2 by norm_num, Real.log_pow]
        push_cast
        nlinarith [Real.log_two_gt_d9]
      linarith
    have hlogn_pos : (0 : ℝ) < Real.log (n : ℝ) := by linarith
    have hloglogn_nonneg : (0 : ℝ) ≤ Real.log (Real.log (n : ℝ)) :=
      Real.log_nonneg hlogn_ge1
    have hlogn_ge2 : 2 ≤ Nat.log 2 n := by
      have hmono : Nat.log 2 4 ≤ Nat.log 2 n := Nat.log_mono_right hn
      have h44 : Nat.log 2 4 = 2 := by decide
      omega
    have hstar : lgStar n ≤ Nat.log 2 (Nat.log 2 n) + 2 := by
      rw [lgStar_of_two_le hn2]
      have := lgStar_le_log_add_one (Nat.log 2 n)
      omega
    have hstarR : (lgStar n : ℝ) ≤ (Nat.log 2 (Nat.log 2 n) : ℝ) + 2 := by
      exact_mod_cast hstar
    have hb1 : (Nat.log 2 (Nat.log 2 n) : ℝ) ≤ 2 * Real.log (Nat.log 2 n : ℝ) :=
      natLog_two_le_two_log (by omega)
    have hb2 : (Nat.log 2 n : ℝ) ≤ 2 * Real.log (n : ℝ) := natLog_two_le_two_log hn1
    have hlogln_pos : (0 : ℝ) < (Nat.log 2 n : ℝ) := by
      have : 0 < Nat.log 2 n := by omega
      exact_mod_cast this
    have hb3 : Real.log (Nat.log 2 n : ℝ) ≤ Real.log (2 * Real.log (n : ℝ)) :=
      Real.log_le_log hlogln_pos hb2
    have hb4 : Real.log (2 * Real.log (n : ℝ)) = Real.log 2 + Real.log (Real.log (n : ℝ)) :=
      Real.log_mul (by norm_num) (by positivity)
    have hcombine : (lgStar n : ℝ) ≤
        2 * Real.log 2 + 2 * Real.log (Real.log (n : ℝ)) + 2 := by
      calc (lgStar n : ℝ) ≤ (Nat.log 2 (Nat.log 2 n) : ℝ) + 2 := hstarR
        _ ≤ 2 * Real.log (Nat.log 2 n : ℝ) + 2 := by linarith [hb1]
        _ ≤ 2 * Real.log (2 * Real.log (n : ℝ)) + 2 := by linarith [hb3]
        _ = 2 * (Real.log 2 + Real.log (Real.log (n : ℝ))) + 2 := by rw [hb4]
        _ = 2 * Real.log 2 + 2 * Real.log (Real.log (n : ℝ)) + 2 := by ring
    rw [Real.norm_eq_abs, Real.norm_eq_abs,
      abs_of_nonneg (by positivity : (0 : ℝ) ≤ (lgStar n : ℝ)),
      abs_of_nonneg (by linarith : (0 : ℝ) ≤ 1 + Real.log (Real.log (n : ℝ)))]
    nlinarith [hcombine, hloglogn_nonneg, hlog2pos,
      mul_nonneg (le_of_lt hlog2pos) hloglogn_nonneg]
  unfold isLittleO
  exact hO.trans_isLittleO hdom

end Chapter03end CLRS

CLRSLean.FourthEdition.Chapter_03.Section_03_2_Standard_Functions.TextbookIdentities

              open Filteropen Asymptoticsopen scoped Topology

CLRS §3.3 textbook identities

This file gives stable CLRS-facing names to the elementary identities used in the prose of §3.3. Most proofs deliberately delegate to Mathlib; the value of these declarations is an explicit, searchable textbook interface rather than a second implementation of integer or real arithmetic.

namespace CLRSnamespace Chapter03

Monotonicity

              def MonotonicallyIncreasing {α β : Type*} [Preorder α] [Preorder β]
    (f : α → β) : Prop := Monotone fdef MonotonicallyDecreasing {α β : Type*} [Preorder α] [Preorder β]
    (f : α → β) : Prop := Antitone fdef StrictlyIncreasing {α β : Type*} [Preorder α] [Preorder β]
    (f : α → β) : Prop := StrictMono fdef StrictlyDecreasing {α β : Type*} [Preorder α] [Preorder β]
    (f : α → β) : Prop := StrictAnti f

Floors, ceilings, and remainders

CLRS (3.1): an integer is unchanged by floor and ceiling.

theorem floor_ceil_int (n : ℤ) :
    ⌊(n : ℝ)⌋ = n ∧ ⌈(n : ℝ)⌉ = n :=
  ⟨Int.floor_intCast n, Int.ceil_intCast n⟩

The two defining inequalities for the floor of a real number.

theorem clrs_floor_bounds (x : ℝ) :
    (⌊x⌋ : ℝ) ≤ x ∧ x < (⌊x⌋ : ℝ) + 1 :=
  ⟨Int.floor_le x, Int.lt_floor_add_one x⟩

The two defining inequalities for the ceiling of a real number.

theorem clrs_ceil_bounds (x : ℝ) :
    (⌈x⌉ : ℝ) - 1 < x ∧ x ≤ (⌈x⌉ : ℝ) := by
  constructor
  · have h := Int.ceil_lt_add_one x
    linarith
  · exact Int.le_ceil x

CLRS (3.3): negating a floor gives the ceiling of the negation.


theorem neg_floor_eq_ceil_neg (x : ℝ) : -⌊x⌋ = ⌈-x⌉ := by
  rw [Int.ceil_neg]

CLRS (3.4): negating a ceiling gives the floor of the negation.


theorem neg_ceil_eq_floor_neg (x : ℝ) : -⌈x⌉ = ⌊-x⌋ := by
  rw [Int.floor_neg]

⌊n/2⌋ + ⌈n/2⌉ = n, using natural floor/ceiling division.


theorem floor_add_ceil_half (n : ℕ) : n / 2 + (n ⌈/⌉ 2) = n := by
  rw [Nat.ceilDiv_eq_add_pred_div]
  omega

Nested flooring divisions combine their divisors.

theorem floor_nested_div (n a b : ℕ) : (n / a) / b = n / (a * b) :=
  Nat.div_div_eq_div_mul n a b

Nested ceiling divisions combine their positive divisors.


theorem ceil_nested_div (n a b : ℕ) (ha : 0 < a) (hb : 0 < b) :
    (n ⌈/⌉ a) ⌈/⌉ b = n ⌈/⌉ (a * b) := by
  apply le_antisymm
  · rw [ceilDiv_le_iff_le_mul hb, ceilDiv_le_iff_le_mul ha]
    have h := le_smul_ceilDiv (α := ℕ) (β := ℕ) (b := n) (Nat.mul_pos ha hb)
    simpa [nsmul_eq_mul, mul_assoc] using h
  · rw [ceilDiv_le_iff_le_mul (Nat.mul_pos ha hb)]
    have h₁ := le_smul_ceilDiv (α := ℕ) (β := ℕ) (b := n) ha
    have h₂ := le_smul_ceilDiv (α := ℕ) (β := ℕ) (b := n ⌈/⌉ a) hb
    calc
      n ≤ a * (n ⌈/⌉ a) := by simpa [nsmul_eq_mul] using h₁
      _ ≤ a * (b * ((n ⌈/⌉ a) ⌈/⌉ b)) := Nat.mul_le_mul_left a (by
        simpa [nsmul_eq_mul] using h₂)
      _ = (a * b) * ((n ⌈/⌉ a) ⌈/⌉ b) := by simp [mul_assoc]

CLRS (3.6), in its original real/integer form.


theorem floor_nested_div_real (x : ℝ) (a b : ℕ) :
    ⌊(⌊x / a⌋ : ℝ) / b⌋ = ⌊x / (a * b)⌋ := by
  rw [Int.floor_div_natCast, Int.floor_intCast, Int.floor_div_natCast]
  have hab : (a : ℝ) * (b : ℝ) = ((a * b : ℕ) : ℝ) := by norm_num
  rw [hab]
  rw [Int.floor_div_natCast]
  exact Int.ediv_ediv_of_nonneg (Int.natCast_nonneg a)

CLRS (3.5), in its original real/integer form.


theorem ceil_nested_div_real (x : ℝ) (a b : ℕ) :
    ⌈(⌈x / a⌉ : ℝ) / b⌉ = ⌈x / (a * b)⌉ := by
  calc
    ⌈(⌈x / a⌉ : ℝ) / b⌉ = -⌊-((⌈x / a⌉ : ℝ) / b)⌋ := by
      rw [Int.floor_neg]; simp
    _ = -⌊(⌊(-x) / a⌋ : ℝ) / b⌋ := by
      congr 2
      rw [show (-x) / (a : ℝ) = -(x / a) by ring, Int.floor_neg, Int.cast_neg]
      ring
    _ = -⌊(-x) / (a * b)⌋ := by rw [floor_nested_div_real]
    _ = ⌈x / (a * b)⌉ := by
      rw [show (-x) / ((a : ℝ) * b) = -(x / ((a : ℝ) * b)) by ring,
        Int.floor_neg]
      simp

CLRS (3.7): ceiling division is at most the usual upper rounding envelope.


theorem ceilDiv_le_add_pred_div (a b : ℕ) (hb : 0 < b) :
    ((a ⌈/⌉ b : ℕ) : ℝ) ≤ ((a + (b - 1) : ℕ) : ℝ) / b := by
  rw [Nat.ceilDiv_eq_add_pred_div]
  rw [show a + b - 1 = a + (b - 1) by omega]
  rw [le_div_iff₀ (by exact_mod_cast hb)]
  exact_mod_cast Nat.div_mul_le_self (a + (b - 1)) b

CLRS (3.8): ceiling division is at least the usual lower rounding envelope.


theorem sub_pred_div_le_ceilDiv (a b : ℕ) (hb : 0 < b) :
    ((a : ℝ) - ((b - 1 : ℕ) : ℝ)) / b ≤ ((a ⌈/⌉ b : ℕ) : ℝ) := by
  rw [div_le_iff₀ (by exact_mod_cast hb)]
  have hceil := le_smul_ceilDiv (α := ℕ) (β := ℕ) (b := a) hb
  have hceilR : (a : ℝ) ≤ b * (a ⌈/⌉ b) := by
    exact_mod_cast (by simpa [nsmul_eq_mul] using hceil)
  have hpred : (0 : ℝ) ≤ (b - 1 : ℕ) := by positivity
  linarith

CLRS (3.9): floor commutes with adding an integer.

theorem floor_int_add (n : ℤ) (x : ℝ) : ⌊(n : ℝ) + x⌋ = n + ⌊x⌋ :=
  Int.floor_intCast_add n x

CLRS (3.10): ceiling commutes with adding an integer.

theorem ceil_int_add (n : ℤ) (x : ℝ) : ⌈(n : ℝ) + x⌉ = n + ⌈x⌉ :=
  Int.ceil_intCast_add n x

Remainder as the amount left after removing the quotient multiples.

theorem mod_eq_sub_mul_div (n d : ℕ) : n % d = n - d * (n / d) := by
  have h := Nat.div_add_mod n d
  omega

A remainder is smaller than its positive divisor.

theorem mod_lt_divisor (n d : ℕ) (hd : 0 < d) : n % d < d :=
  Nat.mod_lt n hd

CLRS (3.11), valid also for a negative integer dividend.

theorem int_mod_eq_sub_mul_floor (a : ℤ) (n : ℕ) :
    a % (n : ℤ) = a - n * ⌊(a : ℚ) / n⌋ :=
  Int.mod_nat_eq_sub_mul_floor_rat_div

CLRS (3.12), including negative integer dividends.

theorem int_mod_bounds (a : ℤ) (n : ℕ) (hn : 0 < n) :
    0 ≤ a % (n : ℤ) ∧ a % (n : ℤ) < n :=
  ⟨Int.emod_nonneg _ (by exact_mod_cast hn.ne'), Int.emod_lt_of_pos _ (by exact_mod_cast hn)⟩

Powers and the exponential function

              theorem pow_zero_identity {M : Type*} [Monoid M] (a : M) : a ^ 0 = 1 :=
  pow_zero atheorem pow_add_identity {M : Type*} [Monoid M] (a : M) (m n : ℕ) :
    a ^ (m + n) = a ^ m * a ^ n :=
  pow_add a m ntheorem pow_mul_identity {M : Type*} [Monoid M] (a : M) (m n : ℕ) :
    (a ^ m) ^ n = a ^ (m * n) :=
  (pow_mul a m n).symmtheorem mul_pow_identity {M : Type*} [CommMonoid M] (a b : M) (n : ℕ) :
    (a * b) ^ n = a ^ n * b ^ n :=
  mul_pow a b ntheorem rpow_zero_identity (a : ℝ) : a ^ (0 : ℝ) = 1 := Real.rpow_zero atheorem rpow_one_identity (a : ℝ) : a ^ (1 : ℝ) = a := Real.rpow_one atheorem rpow_neg_one_identity (a : ℝ) : a ^ (-1 : ℝ) = a⁻¹ := Real.rpow_neg_one atheorem rpow_mul_identity {a : ℝ} (ha : 0 ≤ a) (m n : ℝ) :
    (a ^ m) ^ n = a ^ (m * n) :=
  (Real.rpow_mul ha m n).symm

theorem rpow_swap_identity {a : ℝ} (ha : 0 ≤ a) (m n : ℝ) :
    (a ^ m) ^ n = (a ^ n) ^ m := by
  rw [rpow_mul_identity ha, rpow_mul_identity ha, mul_comm]theorem rpow_add_identity {a : ℝ} (ha : 0 < a) (m n : ℝ) :
    a ^ m * a ^ n = a ^ (m + n) :=
  (Real.rpow_add ha m n).symm

CLRS equation 1 + x ≤ eˣ.

theorem one_add_le_exp (x : ℝ) : 1 + x ≤ Real.exp x := by
  simpa [add_comm] using Real.add_one_le_exp x

The power-series expansion of the real exponential.


theorem exp_series (x : ℝ) :
    HasSum (fun n : ℕ => x ^ n / (Nat.factorial n : ℝ)) (Real.exp x) := by
  rw [Real.exp_eq_exp_ℝ]
  simpa using NormedSpace.expSeries_div_hasSum_exp x

CLRS's limit (1 + 1/n)ⁿ → e.

theorem tendsto_one_add_inv_pow :
    Tendsto (fun n : ℕ => (1 + (1 : ℝ) / n) ^ n) atTop (𝓝 (Real.exp 1)) := by
  simpa using Real.tendsto_one_add_div_pow_exp 1

CLRS (3.15): exp x = 1 + x + Θ(x²) as x → 0.


theorem exp_sub_one_sub_id_isTheta_sq :
    (fun x : ℝ => Real.exp x - 1 - x) =Θ[𝓝 0] (fun x => x ^ 2) := by
  have ho := Real.exp_sub_sum_range_succ_isLittleO_pow 2
  have ho' :
      (fun x : ℝ => Real.exp x - (1 + x + x ^ 2 / 2)) =o[𝓝 0]
        (fun x => x ^ 2) := by
    simpa [Finset.sum_range_succ] using ho
  have htheta : (fun x : ℝ => (1 / 2 : ℝ) * x ^ 2) =Θ[𝓝 0]
      (fun x => x ^ 2) :=
    IsTheta.const_mul_left (by norm_num) (isTheta_refl _ _)
  have h := htheta.add_isLittleO ho'
  have heq :
      (fun x : ℝ => (1 / 2 : ℝ) * x ^ 2) +
          (fun x => Real.exp x - (1 + x + x ^ 2 / 2)) =
        (fun x => Real.exp x - 1 - x) := by
    funext x
    simp only [Pi.add_apply]
    ring
  rw [heq] at h
  exact h

Logarithms

              noncomputable def lg (x : ℝ) : ℝ := Real.logb 2 xnoncomputable def ln (x : ℝ) : ℝ := Real.log xnoncomputable def lgPow (k : ℝ) (x : ℝ) : ℝ := lg x ^ knoncomputable def lgIterate (i : ℕ) (x : ℝ) : ℝ := lg^[i] xtheorem log_mul_identity {x y : ℝ} (hx : x ≠ 0) (hy : y ≠ 0) :
    Real.log (x * y) = Real.log x + Real.log y :=
  Real.log_mul hx hytheorem log_div_identity {x y : ℝ} (hx : x ≠ 0) (hy : y ≠ 0) :
    Real.log (x / y) = Real.log x - Real.log y :=
  Real.log_div hx hytheorem log_pow_identity (x : ℝ) (n : ℕ) :
    Real.log (x ^ n) = n * Real.log x :=
  Real.log_pow x n

CLRS (3.17).

theorem rpow_logb_identity {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hb1 : b ≠ 1) :
    b ^ Real.logb b a = a :=
  Real.rpow_logb hb hb1 ha

CLRS (3.18).

theorem logb_mul_identity {a b c : ℝ} (ha : a ≠ 0) (hb : b ≠ 0) :
    Real.logb c (a * b) = Real.logb c a + Real.logb c b :=
  Real.logb_mul ha hb

CLRS (3.18), power form with a real exponent.

theorem logb_rpow_identity {a b n : ℝ} (ha : 0 < a) :
    Real.logb b (a ^ n) = n * Real.logb b a :=
  Real.logb_rpow_eq_mul_logb_of_pos ha

CLRS (3.19), change of base.

theorem logb_change_base (a : ℝ) {b c : ℝ}
    (hb : 0 < b) (hb1 : b ≠ 1) (hc : 0 < c) (hc1 : c ≠ 1) :
    Real.logb b a = Real.logb c a / Real.logb c b := by
  simp only [Real.logb]
  field_simp [Real.log_ne_zero_of_pos_of_ne_one hb hb1,
    Real.log_ne_zero_of_pos_of_ne_one hc hc1]

The reciprocal identity in CLRS (3.20).

theorem logb_reciprocal (a b : ℝ) :
    (Real.logb a b)⁻¹ = Real.logb b a :=
  Real.inv_logb a b

The inverse-argument identity in CLRS (3.20).

theorem logb_inv_identity (a b : ℝ) :
    Real.logb b a⁻¹ = -Real.logb b a :=
  Real.logb_inv b a

CLRS (3.21).


theorem rpow_logb_swap {a b c : ℝ} (ha : 0 < a) (hc : 0 < c) :
    a ^ Real.logb b c = c ^ Real.logb b a := by
  rw [Real.rpow_def_of_pos ha, Real.rpow_def_of_pos hc]
  congr 1
  simp [Real.logb]
  ring

CLRS (3.22): the power series for log (1 + x).

theorem log_one_add_series {x : ℝ} (hx : |x| < 1) :
    HasSum (fun n : ℕ => -((-x) ^ (n + 1) / (n + 1)))
      (Real.log (1 + x)) := by
  simpa [sub_neg_eq_add] using
    (Real.hasSum_pow_div_log_of_abs_lt_one (x := -x) (by simpa using hx)).neg

The upper inequality in CLRS (3.23).

theorem log_one_add_le {x : ℝ} (hx : -1 < x) : Real.log (1 + x) ≤ x := by
  simpa using Real.log_le_sub_one_of_pos (show 0 < 1 + x by linarith)

The lower inequality in CLRS (3.23).


theorem div_one_add_le_log_one_add {x : ℝ} (hx : -1 < x) :
    x / (1 + x) ≤ Real.log (1 + x) := by
  have hpos : 0 < 1 + x := by linarith
  have h := Real.log_le_sub_one_of_pos (x := (1 + x)⁻¹) (inv_pos.mpr hpos)
  rw [Real.log_inv] at h
  field_simp [hpos.ne'] at h ⊢
  linarith

Factorials

theorem factorial_recurrence (n : ℕ) :
    Nat.factorial (n + 1) = (n + 1) * Nat.factorial n :=
  Nat.factorial_succ n

theorem factorial_zero : Nat.factorial 0 = 1 := Nat.factorial_zero

Stirling's formula in asymptotic-equivalence form.

theorem stirling_formula :
    (fun n : ℕ => (Nat.factorial n : ℝ)) ~[atTop]
      (fun n : ℕ => Real.sqrt (2 * n * Real.pi) *
        (n / Real.exp 1) ^ n) :=
  Stirling.factorial_isEquivalent_stirling

The global lower half of the refined Stirling bound.

theorem stirling_lower_bound (n : ℕ) :
    Real.sqrt (2 * Real.pi * n) * (n / Real.exp 1) ^ n ≤
      (Nat.factorial n : ℝ) := by
  simpa [mul_assoc, mul_left_comm, mul_comm] using Stirling.le_factorial_stirling n

Robbins' sharp stepwise error bound underlying CLRS (3.29).

theorem robbins_stirling_log_error_step (n : ℕ) :
    Real.log (Stirling.stirlingSeq n) -
        Real.log (Stirling.stirlingSeq (n + 1)) ≤
      1 / (12 * n * (n + 1)) :=
  Stirling.log_stirlingSeq_sdiff_le n

Function iteration

              def iterateFunction {α : Type*} (f : α → α) (i : ℕ) : α → α := f^[i]theorem iterateFunction_zero {α : Type*} (f : α → α) (x : α) :
    iterateFunction f 0 x = x := by
  simp [iterateFunction]theorem iterateFunction_succ {α : Type*} (f : α → α) (i : ℕ) (x : α) :
    iterateFunction f (i + 1) x = f (iterateFunction f i x) := by
  simpa [iterateFunction] using Function.iterate_succ_apply' f i x

Fibonacci numbers and the golden ratio

              theorem fibonacci_recurrence (n : ℕ) :
    Nat.fib (n + 2) = Nat.fib n + Nat.fib (n + 1) :=
  Nat.fib_add_twotheorem fibonacci_zero : Nat.fib 0 = 0 := rfltheorem fibonacci_one : Nat.fib 1 = 1 := rfltheorem goldenRatio_definition :
    Real.goldenRatio = (1 + Real.sqrt 5) / 2 := rfltheorem goldenConj_definition :
    Real.goldenConj = (1 - Real.sqrt 5) / 2 := rfl

Concrete iterated-logarithm values

              

theorem lgStar_four : lgStar 4 = 2 := by
  rw [show 4 = 2 ^ 2 by norm_num, lgStar_two_pow (by norm_num), lgStar_two]

theorem lgStar_sixteen : lgStar 16 = 3 := by
  rw [show 16 = 2 ^ 4 by norm_num, lgStar_two_pow (by norm_num), lgStar_four]

theorem lgStar_65536 : lgStar 65536 = 4 := by
  rw [show 65536 = 2 ^ 16 by norm_num, lgStar_two_pow (by norm_num), lgStar_sixteen]

theorem lgStar_two_pow_65536 : lgStar (2 ^ 65536) = 5 := by
  rw [lgStar_two_pow (by norm_num), lgStar_65536]end Chapter03end CLRS

CLRSLean.FourthEdition.Chapter_03.Section_03_2_Standard_Functions.Robbins

open Filteropen scoped Topology

Robbins' finite Stirling error

CLRS equation (3.29) uses the effective error exponent in Stirling's approximation. Mathlib exposes the exact positive series for successive logarithmic errors and its sharp stepwise bound; this file telescopes those facts to the textbook finite bound.

namespace CLRSnamespace Chapter03

The logarithmic error between the normalized Stirling ratio and its limit.

noncomputable def robbinsAlpha (n : ℕ) : ℝ :=
  Real.log (Stirling.stirlingSeq n) - Real.log (Real.sqrt Real.pi)



private theorem robbinsAlpha_hasSum (n : ℕ) :
    HasSum
      (fun k : ℕ => Real.log (Stirling.stirlingSeq (n + 1 + k)) -
        Real.log (Stirling.stirlingSeq ((n + 1 + k) + 1)))
      (robbinsAlpha (n + 1)) := by
  let f (k : ℕ) := Real.log (Stirling.stirlingSeq (n + 1 + k))
  change HasSum (fun k => f k - f (k + 1)) (robbinsAlpha (n + 1))
  rw [hasSum_iff_tendsto_nat_of_nonneg]
  · have hlog : Tendsto (fun k : ℕ => Real.log (Stirling.stirlingSeq k)) atTop
        (𝓝 (Real.log (Real.sqrt Real.pi))) :=
      (Real.continuousAt_log (Real.sqrt_pos.mpr Real.pi_pos).ne').tendsto.comp
        Stirling.tendsto_stirlingSeq_sqrt_pi
    have htail : Tendsto f atTop (𝓝 (Real.log (Real.sqrt Real.pi))) := by
      simpa [f, Function.comp_def, add_comm] using
        hlog.comp (tendsto_add_atTop_nat (n + 1))
    convert tendsto_const_nhds.sub htail using 1
    · ext m
      rw [Finset.sum_range_sub']
    · simp [robbinsAlpha, f]
  · intro k
    apply sub_nonneg.mpr
    simpa [f, Function.comp_apply, add_assoc, add_comm, add_left_comm] using
      Stirling.log_stirlingSeq'_antitone (Nat.le_succ (n + k))



private theorem robbinsUpper_hasSum (n : ℕ) :
    HasSum (fun k : ℕ =>
      (1 : ℝ) / (12 * ((k + n + 1 : ℕ) : ℝ)) -
        1 / (12 * (((k + 1) + n + 1 : ℕ) : ℝ)))
      (1 / (12 * ((0 + n + 1 : ℕ) : ℝ))) := by
  let g (k : ℕ) : ℝ := 1 / (12 * ((k + n + 1 : ℕ) : ℝ))
  change HasSum (fun k => g k - g (k + 1)) (g 0)
  rw [hasSum_iff_tendsto_nat_of_nonneg]
  · have hinv : Tendsto g atTop (𝓝 0) := by
      apply tendsto_const_nhds.div_atTop
      have hcast : Tendsto (fun m : ℕ => ((m + (n + 1) : ℕ) : ℝ)) atTop atTop :=
        tendsto_natCast_atTop_atTop.comp (tendsto_add_atTop_nat (n + 1))
      simpa [g, add_assoc] using
        hcast.const_mul_atTop (by norm_num : (0 : ℝ) < 12)
    convert tendsto_const_nhds.sub hinv using 1
    ext m
    rw [Finset.sum_range_sub']
    simp [g]
  · intro k
    dsimp [g]
    rw [sub_nonneg]
    apply one_div_le_one_div_of_le (by positivity)
    norm_cast
    omega

The upper half αₙ ≤ 1/(12n) of the Robbins bound, for positive n.


theorem robbinsAlpha_le (n : ℕ) :
    robbinsAlpha (n + 1) ≤ 1 / (12 * ((n + 1 : ℕ) : ℝ)) := by
  have hle : robbinsAlpha (n + 1) ≤ 1 / (12 * ((0 + n + 1 : ℕ) : ℝ)) := by
    apply hasSum_le (fun k => ?_) (robbinsAlpha_hasSum n) (robbinsUpper_hasSum n)
    have h := Stirling.log_stirlingSeq_sdiff_le (n + 1 + k)
    calc
      Real.log (Stirling.stirlingSeq (n + 1 + k)) -
          Real.log (Stirling.stirlingSeq ((n + 1 + k) + 1))
        ≤ 1 / (12 * ((n + 1 + k : ℕ) : ℝ) * ((n + 1 + k : ℕ) + 1)) := h
      _ = (1 : ℝ) / (12 * ((k + n + 1 : ℕ) : ℝ)) -
          1 / (12 * (((k + 1) + n + 1 : ℕ) : ℝ)) := by
        have hm : (0 : ℝ) < ((n + 1 + k : ℕ) : ℝ) := by positivity
        push_cast
        field_simp
        ring
  simpa using hle



private theorem robbinsLogStep_lt (n : ℕ) :
    Real.log (Stirling.stirlingSeq (n + 1)) -
        Real.log (Stirling.stirlingSeq (n + 2)) <
      1 / (12 * ((n + 1 : ℕ) : ℝ) * ((n + 2 : ℕ) : ℝ)) := by
  let r := ((1 : ℝ) / (2 * ((n + 1 : ℕ) : ℝ) + 1)) ^ 2
  have hr0 : 0 ≤ r := by positivity
  have hr1 : r < 1 := by
    dsimp [r]
    grw [← n.zero_le]
    norm_num
  have hg : HasSum (fun j : ℕ => r ^ (j + 1) / 3)
      (1 / (12 * ((n + 1 : ℕ) : ℝ) * ((n + 2 : ℕ) : ℝ))) := by
    grind [((hasSum_geometric_of_lt_one hr0 hr1).mul_right r).div_const 3]
  have hf := Stirling.log_stirlingSeq_sdiff_hasSum n
  have hpoint : ∀ j : ℕ,
      (1 : ℝ) / (2 * ((j + 1 : ℕ) : ℝ) + 1) *
          ((1 / (2 * ((n + 1 : ℕ) : ℝ) + 1)) ^ 2) ^ (j + 1) ≤
        r ^ (j + 1) / 3 := by
    intro j
    simpa [r, field] using
      show (3 : ℝ) ≤ 2 * (j + 1) + 1 by norm_cast; omega
  have hstrict :
      (1 : ℝ) / (2 * ((1 + 1 : ℕ) : ℝ) + 1) *
          ((1 / (2 * ((n + 1 : ℕ) : ℝ) + 1)) ^ 2) ^ (1 + 1) <
        r ^ (1 + 1) / 3 := by
    have hpow : 0 < r ^ (1 + 1) := by positivity
    have hcoef : (1 : ℝ) / (2 * ((1 + 1 : ℕ) : ℝ) + 1) < 1 / 3 := by norm_num
    simpa [r, div_eq_mul_inv, mul_comm] using mul_lt_mul_of_pos_right hcoef hpow
  exact hasSum_lt hpoint hstrict hf hg

The strict upper half αₙ < 1/(12n) of Robbins' bound.


theorem robbinsAlpha_lt (n : ℕ) :
    robbinsAlpha (n + 1) < 1 / (12 * ((n + 1 : ℕ) : ℝ)) := by
  have hpoint : ∀ k : ℕ,
      Real.log (Stirling.stirlingSeq (n + 1 + k)) -
          Real.log (Stirling.stirlingSeq ((n + 1 + k) + 1)) ≤
        (1 : ℝ) / (12 * ((k + n + 1 : ℕ) : ℝ)) -
          1 / (12 * (((k + 1) + n + 1 : ℕ) : ℝ)) := by
    intro k
    have h := Stirling.log_stirlingSeq_sdiff_le (n + 1 + k)
    calc
      Real.log (Stirling.stirlingSeq (n + 1 + k)) -
          Real.log (Stirling.stirlingSeq ((n + 1 + k) + 1))
        ≤ 1 / (12 * ((n + 1 + k : ℕ) : ℝ) * ((n + 1 + k : ℕ) + 1)) := h
      _ = (1 : ℝ) / (12 * ((k + n + 1 : ℕ) : ℝ)) -
          1 / (12 * (((k + 1) + n + 1 : ℕ) : ℝ)) := by
        have hm : (0 : ℝ) < ((n + 1 + k : ℕ) : ℝ) := by positivity
        push_cast
        field_simp
        ring
  have hstrict :
      Real.log (Stirling.stirlingSeq (n + 1 + 0)) -
          Real.log (Stirling.stirlingSeq ((n + 1 + 0) + 1)) <
        (1 : ℝ) / (12 * ((0 + n + 1 : ℕ) : ℝ)) -
          1 / (12 * (((0 + 1) + n + 1 : ℕ) : ℝ)) := by
    have h := robbinsLogStep_lt n
    calc
      Real.log (Stirling.stirlingSeq (n + 1 + 0)) -
          Real.log (Stirling.stirlingSeq ((n + 1 + 0) + 1))
        < 1 / (12 * ((n + 1 : ℕ) : ℝ) * ((n + 2 : ℕ) : ℝ)) := by simpa using h
      _ = (1 : ℝ) / (12 * ((0 + n + 1 : ℕ) : ℝ)) -
          1 / (12 * (((0 + 1) + n + 1 : ℕ) : ℝ)) := by
        have hm : (0 : ℝ) < ((n + 1 : ℕ) : ℝ) := by positivity
        push_cast
        field_simp
        ring
  have hlt := hasSum_lt hpoint hstrict (robbinsAlpha_hasSum n) (robbinsUpper_hasSum n)
  simpa using hlt

              

private theorem robbinsLower_hasSum (n : ℕ) :
    HasSum (fun k : ℕ =>
      (1 : ℝ) / (12 * ((k + n + 1 : ℕ) : ℝ) + 1) -
        1 / (12 * (((k + 1) + n + 1 : ℕ) : ℝ) + 1))
      (1 / (12 * ((0 + n + 1 : ℕ) : ℝ) + 1)) := by
  let g (k : ℕ) : ℝ := 1 / (12 * ((k + n + 1 : ℕ) : ℝ) + 1)
  change HasSum (fun k => g k - g (k + 1)) (g 0)
  rw [hasSum_iff_tendsto_nat_of_nonneg]
  · have hinv : Tendsto g atTop (𝓝 0) := by
      apply tendsto_const_nhds.div_atTop
      have hcast : Tendsto (fun m : ℕ => ((m + (n + 1) : ℕ) : ℝ)) atTop atTop :=
        tendsto_natCast_atTop_atTop.comp (tendsto_add_atTop_nat (n + 1))
      have hmul := hcast.const_mul_atTop (by norm_num : (0 : ℝ) < 12)
      simpa [g, add_assoc] using tendsto_atTop_add_const_right atTop 1 hmul
    convert tendsto_const_nhds.sub hinv using 1
    ext m
    rw [Finset.sum_range_sub']
    simp [g]
  · intro k
    dsimp [g]
    rw [sub_nonneg]
    apply one_div_le_one_div_of_le (by positivity)
    norm_cast
    omega

private theorem robbinsLowerStep_lt_first (m : ℕ) (hm : 0 < m) :
    (1 : ℝ) / (12 * (m : ℝ) + 1) - 1 / (12 * ((m + 1 : ℕ) : ℝ) + 1) <
      (1 / 3 : ℝ) * ((1 / (2 * (m : ℝ) + 1)) ^ 2) := by
  have hmR : (0 : ℝ) < m := by exact_mod_cast hm
  have hm1 : (1 : ℝ) ≤ m := by exact_mod_cast hm
  push_cast
  field_simp
  ring_nf at *
  nlinarith

private theorem robbinsFirstTerm_le_step (n k : ℕ) :
    (1 / 3 : ℝ) * ((1 / (2 * ((n + 1 + k : ℕ) : ℝ) + 1)) ^ 2) ≤
      Real.log (Stirling.stirlingSeq (n + 1 + k)) -
        Real.log (Stirling.stirlingSeq ((n + 1 + k) + 1)) := by
  let term (j : ℕ) : ℝ :=
    1 / (2 * ((j + 1 : ℕ) : ℝ) + 1) *
      ((1 / (2 * ((n + k + 1 : ℕ) : ℝ) + 1)) ^ 2) ^ (j + 1)
  have hseries := Stirling.log_stirlingSeq_sdiff_hasSum (n + k)
  have hsingle : HasSum (fun j : ℕ => if j = 0 then term 0 else 0) (term 0) :=
    hasSum_ite_eq 0 (term 0)
  have hle : term 0 ≤
      Real.log (Stirling.stirlingSeq (n + k + 1)) -
        Real.log (Stirling.stirlingSeq (n + k + 2)) := by
    apply hasSum_le (fun j => ?_) hsingle hseries
    by_cases hj : j = 0
    · subst j; simp [term]
    · simp only [hj, ↓reduceIte]
      positivity
  norm_num [term, add_assoc, add_comm, add_left_comm] at hle ⊢
  exact hle

The strict lower half 1/(12n+1) < αₙ of Robbins' bound.


theorem robbinsAlpha_gt (n : ℕ) :
    1 / (12 * ((n + 1 : ℕ) : ℝ) + 1) < robbinsAlpha (n + 1) := by
  have hlt :
      1 / (12 * ((0 + n + 1 : ℕ) : ℝ) + 1) < robbinsAlpha (n + 1) := by
    have hpoint : ∀ k : ℕ,
        (1 : ℝ) / (12 * ((k + n + 1 : ℕ) : ℝ) + 1) -
            1 / (12 * (((k + 1) + n + 1 : ℕ) : ℝ) + 1) ≤
          Real.log (Stirling.stirlingSeq (n + 1 + k)) -
            Real.log (Stirling.stirlingSeq ((n + 1 + k) + 1)) := by
      intro k
      simpa [add_assoc, add_comm, add_left_comm] using
        (robbinsLowerStep_lt_first (n + 1 + k) (by omega)).le.trans
          (robbinsFirstTerm_le_step n k)
    have hstrict :
        (1 : ℝ) / (12 * ((0 + n + 1 : ℕ) : ℝ) + 1) -
            1 / (12 * (((0 + 1) + n + 1 : ℕ) : ℝ) + 1) <
          Real.log (Stirling.stirlingSeq (n + 1 + 0)) -
            Real.log (Stirling.stirlingSeq ((n + 1 + 0) + 1)) := by
      simpa [add_assoc, add_comm, add_left_comm] using
        (robbinsLowerStep_lt_first (n + 1) (by omega)).trans_le
          (robbinsFirstTerm_le_step n 0)
    exact hasSum_lt hpoint hstrict (robbinsLower_hasSum n) (robbinsAlpha_hasSum n)
  simpa using hlt

The normalized error exponent reconstructs the factorial exactly.


theorem factorial_eq_stirling_mul_exp_robbinsAlpha (n : ℕ) :
    (Nat.factorial (n + 1) : ℝ) =
      Real.sqrt (2 * Real.pi * (n + 1)) *
        (((n + 1 : ℕ) : ℝ) / Real.exp 1) ^ (n + 1) *
        Real.exp (robbinsAlpha (n + 1)) := by
  have hN : (0 : ℝ) < (n + 1 : ℕ) := by positivity
  have hs : 0 < Stirling.stirlingSeq (n + 1) := Stirling.stirlingSeq'_pos n
  have hsqrtpi : 0 < Real.sqrt Real.pi := Real.sqrt_pos.mpr Real.pi_pos
  have hsqrt_two_n : 0 < Real.sqrt (2 * ((n + 1 : ℕ) : ℝ)) := by positivity
  have hpow : 0 < (((n + 1 : ℕ) : ℝ) / Real.exp 1) ^ (n + 1) := by positivity
  have hsqrt :
      Real.sqrt (2 * Real.pi * ((n : ℝ) + 1)) =
        Real.sqrt Real.pi * Real.sqrt (2 * ((n : ℝ) + 1)) := by
    rw [show 2 * Real.pi * ((n : ℝ) + 1) =
      Real.pi * (2 * ((n : ℝ) + 1)) by ring,
      Real.sqrt_mul (le_of_lt Real.pi_pos)]
  rw [robbinsAlpha, Real.exp_sub, Real.exp_log hs, Real.exp_log hsqrtpi,
    Stirling.stirlingSeq]
  push_cast
  rw [hsqrt]
  field_simp

The exact strict effective Robbins bounds from CLRS equation (3.29).

theorem robbinsAlpha_bounds (n : ℕ) :
    1 / (12 * ((n + 1 : ℕ) : ℝ) + 1) < robbinsAlpha (n + 1) ∧
      robbinsAlpha (n + 1) < 1 / (12 * ((n + 1 : ℕ) : ℝ)) :=
  ⟨robbinsAlpha_gt n, robbinsAlpha_lt n⟩

end Chapter03end CLRS

CLRSLean.FourthEdition.Chapter_03.Section_03_2_Standard_Functions.GrowthBridges

              open Filteropen Asymptoticsopen Polynomial

Real-exponent and polynomial growth bridges

These are the two substantive generalizations requested by the Chapter 3 semantic audit: CLRS permits real exponents in its polynomial/exponential and polylogarithmic comparisons, and its polynomial-growth statement concerns an arbitrary nonzero polynomial rather than just a monomial.

namespace CLRSnamespace Chapter03

CLRS's predicate that f is bounded by some real polynomial power.

def PolynomiallyBounded (f : ℕ → ℝ) : Prop :=
  ∃ k : ℝ, isBigO f (fun n : ℕ => (n : ℝ) ^ k)

CLRS's predicate that f is bounded by some real power of log n.

def PolylogarithmicallyBounded (f : ℕ → ℝ) : Prop :=
  ∃ k : ℝ, isBigO f (fun n : ℕ => Real.log (n : ℝ) ^ k)

For every real exponent a and real base c > 1, nᵃ = o(cⁿ).


theorem isLittleO_rpow_const_exp {a c : ℝ} (hc : 1 < c) :
    isLittleO (fun n : ℕ => (n : ℝ) ^ a) (fun n : ℕ => c ^ n) := by
  unfold isLittleO
  have hreal := isLittleO_rpow_exp_pos_mul_atTop a (Real.log_pos hc)
  have hcomp := hreal.comp_tendsto tendsto_natCast_atTop_atTop
  refine hcomp.congr' (Eventually.of_forall fun _ => rfl) ?_
  filter_upwards with n
  simp only [Function.comp_apply]
  calc
    Real.exp (Real.log c * (n : ℝ)) = Real.exp ((n : ℝ) * Real.log c) := by rw [mul_comm]
    _ = Real.exp (Real.log c) ^ n := Real.exp_nat_mul (Real.log c) n
    _ = c ^ n := by rw [Real.exp_log (lt_trans zero_lt_one hc)]

For real a and positive real r, (log n)ᵃ = o(nʳ).

theorem isLittleO_log_rpow_rpow {a r : ℝ} (hr : 0 < r) :
    isLittleO (fun n : ℕ => Real.log (n : ℝ) ^ a)
      (fun n : ℕ => (n : ℝ) ^ r) := by
  unfold isLittleO
  exact (isLittleO_log_rpow_rpow_atTop a hr).comp_tendsto
    tendsto_natCast_atTop_atTop

A polynomial is asymptotically equivalent to its leading term.

theorem polynomial_isEquivalent_leadingTerm (P : ℝ[X]) :
    (fun n : ℕ => P.eval (n : ℝ)) ~[atTop]
      (fun n : ℕ => P.leadingCoeff * (n : ℝ) ^ P.natDegree) := by
  exact (P.isEquivalent_atTop_lead.comp_tendsto tendsto_natCast_atTop_atTop).congr
    (by simp) (by simp)

Every nonzero real polynomial has Θ(nᵈ) growth, where d is its degree.

theorem polynomial_isBigTheta_degree (P : ℝ[X]) (hP : P ≠ 0) :
    isBigTheta (fun n : ℕ => P.eval (n : ℝ))
      (fun n : ℕ => (n : ℝ) ^ P.natDegree) := by
  have hlead :
      (fun n : ℕ => P.eval (n : ℝ)) =Θ[atTop]
        (fun n : ℕ => P.leadingCoeff * (n : ℝ) ^ P.natDegree) :=
    (polynomial_isEquivalent_leadingTerm P).isTheta
  have hc : P.leadingCoeff ≠ 0 := Polynomial.leadingCoeff_ne_zero.mpr hP
  have hscale :
      (fun n : ℕ => P.leadingCoeff * (n : ℝ) ^ P.natDegree) =Θ[atTop]
        (fun n : ℕ => (n : ℝ) ^ P.natDegree) :=
    IsTheta.const_mul_left hc (isTheta_refl _ _)
  have h := hlead.trans hscale
  exact ⟨by unfold isBigO; exact h.1, by unfold isBigOmega; exact h.2⟩

end Chapter03end CLRS

CLRSLean.FourthEdition.Chapter_03.Section_03_2_Standard_Functions.GrowthHierarchy

              open Filteropen Asymptoticsopen scoped Topology

The complete CLRS growth hierarchy

This file supplies the two comparison layers that are easy to omit from a short growth table: arbitrary real powers, and the superpolynomial but subexponential function n^(log n). The latter is represented by the extension-safe real expression exp ((log n)^2); the two expressions agree for every positive n.

namespace CLRSnamespace Chapter03

An everywhere-defined real representation of n^(log n).

noncomputable def nPowLog (n : ℕ) : ℝ :=
  Real.exp (Real.log (n : ℝ) ^ 2)

On positive inputs, nPowLog n is exactly the real power n^(log n).


theorem nPowLog_eq_rpow_log {n : ℕ} (hn : 0 < n) :
    nPowLog n = (n : ℝ) ^ Real.log (n : ℝ) := by
  rw [nPowLog, Real.rpow_def_of_pos (by exact_mod_cast hn)]
  congr 1
  ring

Strictly larger real powers dominate smaller ones.


theorem isLittleO_rpow_rpow {a b : ℝ} (hab : a < b) :
    isLittleO (fun n : ℕ => (n : ℝ) ^ a)
      (fun n : ℕ => (n : ℝ) ^ b) := by
  unfold isLittleO
  apply isLittleO_of_tendsto'
  · filter_upwards [eventually_gt_atTop 0] with n hn _hzero
    exact False.elim ((Real.rpow_pos_of_pos
      (show (0 : ℝ) < (n : ℝ) by exact_mod_cast hn) b).ne' _hzero)
  · have hlim : Tendsto (fun x : ℝ => x ^ (-(b - a))) atTop (𝓝 0) :=
      tendsto_rpow_neg_atTop (sub_pos.mpr hab)
    have hcomp := hlim.comp tendsto_natCast_atTop_atTop
    apply hcomp.congr'
    filter_upwards [eventually_gt_atTop 0] with n hn
    simp only [Function.comp_apply]
    rw [show -(b - a) = a - b by ring,
      Real.rpow_sub (show (0 : ℝ) < (n : ℝ) by exact_mod_cast hn)]

Every fixed real power is dominated by n^(log n).


theorem isLittleO_rpow_nPowLog (a : ℝ) :
    isLittleO (fun n : ℕ => (n : ℝ) ^ a) nPowLog := by
  unfold isLittleO
  apply isLittleO_of_tendsto'
  · exact Eventually.of_forall fun n hzero =>
      (Real.exp_ne_zero (Real.log (n : ℝ) ^ 2) hzero).elim
  · have hgauss :
        Tendsto (fun x : ℝ => Real.exp ((-1) * x ^ 2 + a * x)) atTop (𝓝 0) := by
      have ho := rexp_neg_quadratic_isLittleO_rpow_atTop
        (a := (-1 : ℝ)) (by norm_num) a 0
      simpa using ho.tendsto_div_nhds_zero
    have hcomp := hgauss.comp
      (Real.tendsto_log_atTop.comp tendsto_natCast_atTop_atTop)
    apply hcomp.congr'
    filter_upwards [eventually_gt_atTop 0] with n hn
    simp only [Function.comp_apply]
    rw [Real.rpow_def_of_pos (by exact_mod_cast hn : (0 : ℝ) < n), nPowLog,
      ← Real.exp_sub]
    congr 1
    ring

The n^(log n) layer is below every fixed-base exponential c^n, c > 1.


theorem isLittleO_nPowLog_const_exp {c : ℝ} (hc : 1 < c) :
    isLittleO nPowLog (fun n : ℕ => c ^ n) := by
  unfold isLittleO
  have hlogc : 0 < Real.log c := Real.log_pos hc
  have hlogsq :
      (fun n : ℕ => Real.log (n : ℝ) ^ (2 : ℝ)) =o[atTop]
        (fun n : ℕ => (n : ℝ) ^ (1 : ℝ)) :=
    isLittleO_log_rpow_rpow (a := 2) (r := 1) (by norm_num)
  have hbound := hlogsq.def (half_pos hlogc)
  have htend :
      Tendsto (fun n : ℕ => Real.log c * (n : ℝ) - Real.log (n : ℝ) ^ 2)
        atTop atTop := by
    refine tendsto_atTop_mono' atTop ?_
      (tendsto_natCast_atTop_atTop.const_mul_atTop (half_pos hlogc))
    filter_upwards [hbound, eventually_ge_atTop 1] with n hn hnone
    have hnnonneg : (0 : ℝ) ≤ (n : ℝ) := by positivity
    simp only [Real.rpow_two, Real.rpow_one, Real.norm_eq_abs, abs_sq,
      abs_of_nonneg hnnonneg] at hn
    nlinarith
  have hexp :
      (fun n : ℕ => Real.exp (Real.log (n : ℝ) ^ 2)) =o[atTop]
        (fun n : ℕ => Real.exp (Real.log c * (n : ℝ))) := by
    rw [Real.isLittleO_exp_comp_exp_comp]
    exact htend
  refine hexp.congr' (Eventually.of_forall fun _ => rfl) ?_
  filter_upwards with n
  calc
    Real.exp (Real.log c * (n : ℝ)) = Real.exp ((n : ℝ) * Real.log c) := by rw [mul_comm]
    _ = Real.exp (Real.log c) ^ n := Real.exp_nat_mul (Real.log c) n
    _ = c ^ n := by rw [Real.exp_log (lt_trans zero_lt_one hc)]

A single public bundle of the represented Chapter 3 growth hierarchy.

It retains the previously proved constant/logarithmic edges and adds the fractional-power, n^(log n), exponential, factorial, and self-power edges.

theorem complete_growth_hierarchy :
    isLittleO (fun n : ℕ => (lgStar n : ℝ)) (fun n => Real.log (n : ℝ)) ∧
    isLittleO (fun _ : ℕ => (1 : ℝ)) (fun n => Real.log (n : ℝ)) ∧
    isLittleO (fun n : ℕ => Real.log (Real.log (n : ℝ)))
      (fun n => Real.log (n : ℝ)) ∧
    isLittleO (fun n : ℕ => Real.log (n : ℝ)) (fun n => (n : ℝ)) ∧
    (∀ {a b : ℝ}, a < b →
      isLittleO (fun n : ℕ => (n : ℝ) ^ a) (fun n => (n : ℝ) ^ b)) ∧
    (∀ a : ℝ, isLittleO (fun n : ℕ => (n : ℝ) ^ a) nPowLog) ∧
    isLittleO nPowLog (fun n : ℕ => (2 : ℝ) ^ n) ∧
    isLittleO (fun n : ℕ => (2 : ℝ) ^ n)
      (fun n => (Nat.factorial n : ℝ)) ∧
    isLittleO (fun n : ℕ => (Nat.factorial n : ℝ))
      (fun n => (n : ℝ) ^ n) := by
  exact ⟨isLittleO_lgStar_log, isLittleO_one_log, isLittleO_loglog_log,
    isLittleO_log_id, fun h => isLittleO_rpow_rpow h, isLittleO_rpow_nPowLog,
    isLittleO_nPowLog_const_exp (by norm_num), isLittleO_two_pow_factorial,
    isLittleO_factorial_pow_self⟩

end Chapter03end CLRS

3.3. Standard Notations and Common Functions

Main results

Definitions and proofs

CLRSLean.FourthEdition.Chapter_03.Section_03_2_Standard_Functions.Core

3.2. Standard Notations and Common Functions

Polynomial comparisons

Polynomial, logarithmic, and exponential comparisons

Harmonic numbers

Floor and ceiling are Θ(id) on ℕ

Factorial bound

Exponential vs factorial

Log-factorial asymptotics (Stirling)

Logarithm base change

Completing the CLRS 3.2 comparison table

Fibonacci-number growth (CLRS §3.3)

Iterated logarithm lg* (CLRS §3.3)

CLRSLean.FourthEdition.Chapter_03.Section_03_2_Standard_Functions.TextbookIdentities

CLRS §3.3 textbook identities

Monotonicity

Floors, ceilings, and remainders

Powers and the exponential function

Logarithms

Factorials

Function iteration

Fibonacci numbers and the golden ratio

Concrete iterated-logarithm values

CLRSLean.FourthEdition.Chapter_03.Section_03_2_Standard_Functions.Robbins

Robbins' finite Stirling error

CLRSLean.FourthEdition.Chapter_03.Section_03_2_Standard_Functions.GrowthBridges

Real-exponent and polynomial growth bridges

CLRSLean.FourthEdition.Chapter_03.Section_03_2_Standard_Functions.GrowthHierarchy

The complete CLRS growth hierarchy

Iterated logarithm `lg*` (CLRS §3.3)