Skip to content
  1. CLRS-Lean
  2. Chapters 1–35 · CLRS Fourth Edition
  3. Chapter 3. Characterizing Running Times
Browse chapters

Chapter 3 — Characterizing Running Times

CLRS, fourth edition · Lean 4 formalization

The proofs below use the models and assumptions described in the scope and implementation notes.

Imports
import CLRSLean.FourthEdition.Chapter_03.Section_03_1_Asymptotic_Notation.Core import CLRSLean.FourthEdition.Chapter_03.Section_03_1_Asymptotic_Notation.CLRSBridge

3.1. Asymptotic Notation

Stable facade for the core filter-based definitions and the explicit bridges to the nonnegative, strict-inequality formulations printed in CLRS.

Implementation details

Definitions and proofs

CLRSLean.FourthEdition.Chapter_03.Section_03_1_Asymptotic_Notation.Core

open Filteropen Asymptotics

3.1. Asymptotic Notation

CLRS-compatible wrappers for mathlib's filter-based asymptotics on ℕ → ℝ. Proves equivalence between the CLRS discrete definition and the filter definition, plus standard algebraic properties: the Θ characterization with a single shared threshold, the o/ω and O/Ω dualities, and the little-o closure properties (additivity, products, composition) used in the growth estimates of fourth-edition §3.3.

namespace CLRSnamespace Chapter03
Wrapper definitions
def isBigO (f g : ℕ → ℝ) : Prop := f =O[atTop] gdef isBigOmega (f g : ℕ → ℝ) : Prop := g =O[atTop] fdef isBigTheta (f g : ℕ → ℝ) : Prop := isBigO f g ∧ isBigOmega f gdef isLittleO (f g : ℕ → ℝ) : Prop := f =o[atTop] gdef isLittleOmega (f g : ℕ → ℝ) : Prop := g =o[atTop] f
Equivalence with CLRS discrete definition
theorem isBigO_iff (f g : ℕ → ℝ) : isBigO f g ↔ ∃ (c : ℝ), c > 0 ∧ ∃ (n₀ : ℕ), ∀ n, n ≥ n₀ → |f n| ≤ c * |g n| := by unfold isBigO rw [IsBigO_def] constructor · rintro ⟨c, hc⟩ rcases IsBigOWith.exists_pos hc with ⟨c', hc_pos, hc'⟩ have hevent := (isBigOWith_iff.mp hc') have hevent' : ∀ᶠ n in atTop, |f n| ≤ c' * |g n| := by simpa [Real.norm_eq_abs] using hevent rw [Filter.eventually_atTop] at hevent' rcases hevent' with ⟨n₀, hn₀⟩ exact ⟨c', hc_pos, n₀, hn₀⟩ · rintro ⟨c, hc_pos, n₀, hn₀⟩ have hevent : ∀ᶠ n in atTop, |f n| ≤ c * |g n| := by rw [Filter.eventually_atTop] exact ⟨n₀, hn₀⟩ have hevent' : ∀ᶠ n in atTop, ‖f n‖ ≤ c * ‖g n‖ := by simpa [Real.norm_eq_abs] using hevent have hOwith : IsBigOWith c atTop f g := isBigOWith_iff.mpr hevent' exact ⟨c, hOwith⟩ theorem isLittleO_iff (f g : ℕ → ℝ) : isLittleO f g ↔ ∀ (c : ℝ), c > 0 → ∃ (n₀ : ℕ), ∀ n, n ≥ n₀ → |f n| ≤ c * |g n| := by unfold isLittleO rw [isLittleO_iff_forall_isBigOWith] constructor · intro h c hc_pos have hOwith : IsBigOWith c atTop f g := h hc_pos have hevent := (isBigOWith_iff.mp hOwith) have hevent' : ∀ᶠ n in atTop, |f n| ≤ c * |g n| := by simpa [Real.norm_eq_abs] using hevent rw [Filter.eventually_atTop] at hevent' rcases hevent' with ⟨n₀, hn₀⟩ exact ⟨n₀, hn₀⟩ · intro h c hc_pos rcases h c hc_pos with ⟨n₀, hn₀⟩ have hevent : ∀ᶠ n in atTop, |f n| ≤ c * |g n| := by rw [Filter.eventually_atTop] exact ⟨n₀, hn₀⟩ have hevent' : ∀ᶠ n in atTop, ‖f n‖ ≤ c * ‖g n‖ := by simpa [Real.norm_eq_abs] using hevent exact isBigOWith_iff.mpr hevent' theorem isBigOmega_iff (f g : ℕ → ℝ) : isBigOmega f g ↔ ∃ (c : ℝ), c > 0 ∧ ∃ (n₀ : ℕ), ∀ n, n ≥ n₀ → c * |g n| ≤ |f n| := by -- isBigOmega f g = isBigO g f, and isBigO_iff g f gives -- isBigO g f ↔ ∃ c>0, n₀, ∀ n≥n₀, |g n| ≤ c * |f n| -- We prove this RHS is equivalent to -- ∃ c>0, n₀, ∀ n≥n₀, c * |g n| ≤ |f n| -- by exchanging c ↔ c⁻¹. have h_base := isBigO_iff g f -- isBigOmega f g = isBigO g f definitionally -- Now the goal is: isBigO g f ↔ ∃ c>0, n₀, ∀ n≥n₀, c * |g n| ≤ |f n| -- But h_base says: isBigO g f ↔ ∃ c>0, n₀, ∀ n≥n₀, |g n| ≤ c * |f n| -- So it suffices to show the two RHSs are equivalent. constructor · -- From isBigO g f, get ∃ c>0, n₀, ∀ n≥n₀, |g n| ≤ c * |f n| -- Transform to ∃ c'>0, n₀, ∀ n≥n₀, c' * |g n| ≤ |f n| via c' = c⁻¹ intro h_isO rcases h_base.mp h_isO with ⟨c, hc_pos, n₀, hn₀⟩ have hc_ne_zero : c ≠ 0 := by linarith refine ⟨c⁻¹, inv_pos.mpr hc_pos, n₀, λ n hn => ?_⟩ have hineq := hn₀ n hn calc c⁻¹ * |g n| ≤ c⁻¹ * (c * |f n|) := by gcongr _ = (c⁻¹ * c) * |f n| := by ring _ = 1 * |f n| := by field_simp [hc_ne_zero] _ = |f n| := by simp · intro h_omega rcases h_omega with ⟨c, hc_pos, n₀, hn₀⟩ have hc_ne_zero : c ≠ 0 := by linarith -- Need to show isBigO g f, i.e. ∃ c'>0, n₀, ∀ n≥n₀, |g n| ≤ c' * |f n| -- Using c' = c⁻¹ apply h_base.mpr refine ⟨c⁻¹, inv_pos.mpr hc_pos, n₀, λ n hn => ?_⟩ have hineq := hn₀ n hn calc |g n| = (c⁻¹ * c) * |g n| := by field_simp [hc_ne_zero] _ = c⁻¹ * (c * |g n|) := by ring _ ≤ c⁻¹ * |f n| := by gcongr theorem isLittleOmega_iff (f g : ℕ → ℝ) : isLittleOmega f g ↔ ∀ (c : ℝ), c > 0 → ∃ (n₀ : ℕ), ∀ n, n ≥ n₀ → c * |g n| ≤ |f n| := by -- isLittleOmega f g = isLittleO g f -- isLittleO_iff g f says: isLittleO g f ↔ ∀ c>0, ∃ n₀, |g n| ≤ c * |f n| -- We need to show the RHS is equivalent to ∀ c>0, c * |g n| ≤ |f n| -- via exchanging c ↔ c⁻¹. have h_base := isLittleO_iff g f -- isLittleOmega f g = isLittleO g f definitionally constructor · intro h_o c hc have hc_inv_pos : c⁻¹ > 0 := inv_pos.mpr hc rcases (h_base.mp h_o) c⁻¹ hc_inv_pos with ⟨n₀, hn₀⟩ have hc_ne_zero : c ≠ 0 := by linarith refine ⟨n₀, λ n hn => ?_⟩ have hineq := hn₀ n hn calc c * |g n| ≤ c * (c⁻¹ * |f n|) := by gcongr _ = (c * c⁻¹) * |f n| := by ring _ = 1 * |f n| := by field_simp [hc_ne_zero] _ = |f n| := by simp · intro h_forall apply h_base.mpr intro c' hc'_pos have hc_inv_pos : c'⁻¹ > 0 := inv_pos.mpr hc'_pos rcases h_forall c'⁻¹ hc_inv_pos with ⟨n₀, hn₀⟩ have hc_ne_zero : c' ≠ 0 := by linarith refine ⟨n₀, λ n hn => ?_⟩ have hineq := hn₀ n hn calc |g n| = c' * (c'⁻¹ * |g n|) := by field_simp [hc_ne_zero] _ ≤ c' * |f n| := by gcongr
Algebraic properties
theorem isBigO_refl (f : ℕ → ℝ) : isBigO f f := by unfold isBigO exact Asymptotics.isBigO_refl f atToptheorem isBigOmega_refl (f : ℕ → ℝ) : isBigOmega f f := isBigO_refl ftheorem isBigTheta_refl (f : ℕ → ℝ) : isBigTheta f f := ⟨isBigO_refl f, isBigOmega_refl f⟩theorem isBigO_trans {f g h : ℕ → ℝ} (hfg : isBigO f g) (hgh : isBigO g h) : isBigO f h := by unfold isBigO at hfg hgh ⊢ exact IsBigO.trans hfg hghtheorem isBigOmega_trans {f g h : ℕ → ℝ} (hfg : isBigOmega f g) (hgh : isBigOmega g h) : isBigOmega f h := by unfold isBigOmega at hfg hgh ⊢ exact IsBigO.trans hgh hfgtheorem isBigTheta_symm {f g : ℕ → ℝ} (h : isBigTheta f g) : isBigTheta g f := ⟨h.2, h.1⟩theorem isBigTheta_trans {f g h : ℕ → ℝ} (hfg : isBigTheta f g) (hgh : isBigTheta g h) : isBigTheta f h := ⟨isBigO_trans hfg.1 hgh.1, isBigOmega_trans hfg.2 hgh.2⟩theorem isBigO_add {f₁ f₂ g : ℕ → ℝ} (h₁ : isBigO f₁ g) (h₂ : isBigO f₂ g) : isBigO (λ n => f₁ n + f₂ n) g := by unfold isBigO at h₁ h₂ ⊢ exact IsBigO.add h₁ h₂theorem isBigTheta_iff (f g : ℕ → ℝ) : isBigTheta f g ↔ isBigO f g ∧ isBigO g f := by simp [isBigTheta, isBigOmega, isBigO]
Shared threshold for Θ and dualities

Theorem (Θ with a shared threshold). f = Θ(g) iff there exist positive constants c₁, c₂ and a single threshold n₀ such that for all n ≥ n₀, c₁ * |g n| ≤ |f n| ≤ c₂ * |g n|.

This is the two-sided witness characterization of Θ-notation from CLRS §3.1; the two independent witnesses are combined by taking the maximum of their thresholds.

theorem isBigTheta_iff_sharedThreshold (f g : ℕ → ℝ) : isBigTheta f g ↔ ∃ c₁ c₂ : ℝ, 0 < c₁ ∧ 0 < c₂ ∧ ∃ n₀ : ℕ, ∀ n, n₀ ≤ n → c₁ * |g n| ≤ |f n| ∧ |f n| ≤ c₂ * |g n| := by rw [isBigTheta_iff] rw [show isBigO g f ↔ isBigOmega f g by simp [isBigO, isBigOmega]] rw [isBigO_iff, isBigOmega_iff] constructor · rintro ⟨hO, hΩ⟩ rcases hO with ⟨c₂, hc₂, n₀₂, h₂⟩ rcases hΩ with ⟨c₁, hc₁, n₀₁, h₁⟩ refine ⟨c₁, c₂, hc₁, hc₂, max n₀₁ n₀₂, ?_⟩ intro n hn exact ⟨h₁ n (le_trans (le_max_left n₀₁ n₀₂) hn), h₂ n (le_trans (le_max_right n₀₁ n₀₂) hn)⟩ · rintro ⟨c₁, c₂, hc₁, hc₂, n₀, h⟩ constructor · refine ⟨c₂, hc₂, n₀, ?_⟩ intro n hn exact (h n hn).2 · refine ⟨c₁, hc₁, n₀, ?_⟩ intro n hn exact (h n hn).1

Lemma (duality of o and ω). f = o(g) iff g = ω(f) (CLRS §3.1, with the convention isLittleOmega f g := isLittleO g f).

theorem isLittleO_reciprocal (f g : ℕ → ℝ) : isLittleO f g ↔ isLittleOmega g f := by simp [isLittleO, isLittleOmega]

Lemma (duality of O and Ω). f = O(g) iff g = Ω(f) (CLRS §3.1, with the convention isBigOmega f g := isBigO g f).

theorem isBigO_reciprocal (f g : ℕ → ℝ) : isBigO f g ↔ isBigOmega g f := by simp [isBigO, isBigOmega]
Little-o and little-omega algebra

Lemma. Little-o implies big-O: if f = o(g) then f = O(g) (CLRS §3.1).

theorem isLittleO_isBigO {f g : ℕ → ℝ} : isLittleO f g → isBigO f g := by intro h unfold isLittleO at h unfold isBigO exact h.isBigO

Lemma (additivity of o). If f₁ = o(g) and f₂ = o(g), then f₁ + f₂ = o(g) (CLRS §3.1).

theorem isLittleO_add {f₁ f₂ g : ℕ → ℝ} : isLittleO f₁ g → isLittleO f₂ g → isLittleO (fun n => f₁ n + f₂ n) g := by intro h₁ h₂ unfold isLittleO at h₁ h₂ ⊢ exact h₁.add h₂

Lemma (product rule). If f₁ = o(g₁) and f₂ = O(g₂), then f₁ * f₂ = o(g₁ * g₂) (CLRS §3.1).

theorem isLittleO_mul {f₁ g₁ f₂ g₂ : ℕ → ℝ} : isLittleO f₁ g₁ → isBigO f₂ g₂ → isLittleO (fun n => f₁ n * f₂ n) (fun n => g₁ n * g₂ n) := by intro h₁ h₂ unfold isLittleO at h₁ ⊢ unfold isBigO at h₂ exact h₁.mul_isBigO h₂

Lemma (composition of o). If h : ℕ → ℕ tends to infinity and f = o(g), then f ∘ h = o(g ∘ h). This is the asymptotic analogue of substituting h n for n, as used in the growth estimates of fourth-edition CLRS §§3.2–3.3.

theorem isLittleO_comp {f g : ℕ → ℝ} {h : ℕ → ℕ} (hh : Tendsto h atTop atTop) : isLittleO f g → isLittleO (fun n => f (h n)) (fun n => g (h n)) := by intro hfg unfold isLittleO at hfg ⊢ exact hfg.comp_tendsto hh

Lemma (scaling ω). If c > 0 and f = ω(g), then c * f = ω(g) (CLRS §3.1: positive constant factors are irrelevant in asymptotic notation).

theorem isLittleOmega_scale {f g : ℕ → ℝ} {c : ℝ} (hc : 0 < c) : isLittleOmega f g → isLittleOmega (fun n => c * f n) g := by intro h unfold isLittleOmega at h ⊢ exact h.const_mul_right (ne_of_gt hc)

Lemma (ω survives addition of a dominated term). If f = ω(g) and h = O(g), then f + h = ω(g) (CLRS §3.1: adding an O(g) term does not change the ω(g) lower bound).

theorem isLittleOmega_add_dominated {f g h : ℕ → ℝ} : isLittleOmega f g → isBigO h g → isLittleOmega (fun n => f n + h n) g := by intro hfg hh have h_ho : isLittleO h f := by unfold isBigO at hh unfold isLittleO exact hh.trans_isLittleO hfg rw [isLittleOmega_iff] at hfg rw [isLittleO_iff] at h_ho rw [isLittleOmega_iff] intro c hc rcases hfg (2 * c) (by positivity) with ⟨n₁, hn₁⟩ rcases h_ho (1 / 2) (by norm_num) with ⟨n₂, hn₂⟩ refine ⟨max n₁ n₂, ?_⟩ intro n hn have hn₁' : n₁ ≤ n := le_trans (le_max_left n₁ n₂) hn have hn₂' : n₂ ≤ n := le_trans (le_max_right n₁ n₂) hn have hg : (2 * c) * |g n| ≤ |f n| := hn₁ n hn₁' have hh' : |h n| ≤ (1 / 2) * |f n| := hn₂ n hn₂' have htri : |f n| - |h n| ≤ |f n + h n| := by have h₁ : |f n| ≤ |f n + h n| + |h n| := by calc |f n| = |(f n + h n) + (-h n)| := by congr 1; ring _ ≤ |f n + h n| + |(-h n)| := abs_add_le (f n + h n) (-(h n)) _ = |f n + h n| + |h n| := by rw [abs_neg] linarith calc c * |g n| = (1 / 2) * (2 * c * |g n|) := by ring _ ≤ (1 / 2) * |f n| := by gcongr _ ≤ |f n| - |h n| := by linarith _ ≤ |f n + h n| := htri
end Chapter03end CLRS

CLRSLean.FourthEdition.Chapter_03.Section_03_1_Asymptotic_Notation.CLRSBridge

open Filteropen Asymptotics

CLRS-facing bridges for asymptotic notation

The core relations use norms, as Mathlib does, so that they remain meaningful for signed functions. CLRS prints inequalities without absolute values and silently works with eventually nonnegative running-time functions. The first five theorems make that representation boundary exact. The strict little-o and little-omega forms additionally require the comparison side to be eventually positive; without that assumption a strict inequality can fail at infinitely many common zeros even though the norm-based little-o relation holds.

namespace CLRSnamespace Chapter03

CLRS's nonnegative witness form of big-O.

theorem isBigO_iff_clrs {f g : ℕ → ℝ} (hf : ∀ᶠ n in atTop, 0 ≤ f n) (hg : ∀ᶠ n in atTop, 0 ≤ g n) : isBigO f g ↔ ∃ c : ℝ, 0 < c ∧ ∃ n₀ : ℕ, ∀ n, n₀ ≤ n → 0 ≤ f n ∧ f n ≤ c * g n := by rw [Filter.eventually_atTop] at hf hg rcases hf with ⟨nf, hf⟩ rcases hg with ⟨ng, hg⟩ constructor · intro h rcases (isBigO_iff f g).mp h with ⟨c, hc, n₀, hn₀⟩ refine ⟨c, hc, max n₀ (max nf ng), ?_⟩ intro n hn have hn₀' : n₀ ≤ n := le_trans (le_max_left _ _) hn have hnf : nf ≤ n := le_trans (le_max_left nf ng) (le_trans (le_max_right n₀ _) hn) have hng : ng ≤ n := le_trans (le_max_right nf ng) (le_trans (le_max_right n₀ _) hn) have hf0 := hf n hnf have hg0 := hg n hng simpa [abs_of_nonneg hf0, abs_of_nonneg hg0] using And.intro hf0 (hn₀ n hn₀') · rintro ⟨c, hc, n₀, hn₀⟩ apply (isBigO_iff f g).mpr refine ⟨c, hc, max n₀ ng, ?_⟩ intro n hn have hn₀' : n₀ ≤ n := le_trans (le_max_left _ _) hn have hng : ng ≤ n := le_trans (le_max_right _ _) hn have hfg := hn₀ n hn₀' simpa [abs_of_nonneg hfg.1, abs_of_nonneg (hg n hng)] using hfg.2

CLRS's nonnegative witness form of big-Omega.

theorem isBigOmega_iff_clrs {f g : ℕ → ℝ} (hf : ∀ᶠ n in atTop, 0 ≤ f n) (hg : ∀ᶠ n in atTop, 0 ≤ g n) : isBigOmega f g ↔ ∃ c : ℝ, 0 < c ∧ ∃ n₀ : ℕ, ∀ n, n₀ ≤ n → 0 ≤ g n ∧ c * g n ≤ f n := by rw [Filter.eventually_atTop] at hf hg rcases hf with ⟨nf, hf⟩ rcases hg with ⟨ng, hg⟩ constructor · intro h rcases (isBigOmega_iff f g).mp h with ⟨c, hc, n₀, hn₀⟩ refine ⟨c, hc, max n₀ (max nf ng), ?_⟩ intro n hn have hn₀' : n₀ ≤ n := le_trans (le_max_left _ _) hn have hnf : nf ≤ n := le_trans (le_max_left nf ng) (le_trans (le_max_right n₀ _) hn) have hng : ng ≤ n := le_trans (le_max_right nf ng) (le_trans (le_max_right n₀ _) hn) have hf0 := hf n hnf have hg0 := hg n hng simpa [abs_of_nonneg hf0, abs_of_nonneg hg0] using And.intro hg0 (hn₀ n hn₀') · rintro ⟨c, hc, n₀, hn₀⟩ apply (isBigOmega_iff f g).mpr refine ⟨c, hc, max n₀ nf, ?_⟩ intro n hn have hn₀' : n₀ ≤ n := le_trans (le_max_left _ _) hn have hnf : nf ≤ n := le_trans (le_max_right _ _) hn have hfg := hn₀ n hn₀' simpa [abs_of_nonneg (hf n hnf), abs_of_nonneg hfg.1] using hfg.2

CLRS's two-sided nonnegative definition of Theta.

theorem isBigTheta_iff_clrs {f g : ℕ → ℝ} (hf : ∀ᶠ n in atTop, 0 ≤ f n) (hg : ∀ᶠ n in atTop, 0 ≤ g n) : isBigTheta f g ↔ ∃ c₁ c₂ : ℝ, 0 < c₁ ∧ 0 < c₂ ∧ ∃ n₀ : ℕ, ∀ n, n₀ ≤ n → 0 ≤ f n ∧ 0 ≤ g n ∧ c₁ * g n ≤ f n ∧ f n ≤ c₂ * g n := by rw [Filter.eventually_atTop] at hf hg rcases hf with ⟨nf, hf⟩ rcases hg with ⟨ng, hg⟩ constructor · intro h rcases (isBigTheta_iff_sharedThreshold f g).mp h with ⟨c₁, c₂, hc₁, hc₂, n₀, hn₀⟩ refine ⟨c₁, c₂, hc₁, hc₂, max n₀ (max nf ng), ?_⟩ intro n hn have hn₀' : n₀ ≤ n := le_trans (le_max_left _ _) hn have hnf : nf ≤ n := le_trans (le_max_left nf ng) (le_trans (le_max_right n₀ _) hn) have hng : ng ≤ n := le_trans (le_max_right nf ng) (le_trans (le_max_right n₀ _) hn) have hf0 := hf n hnf have hg0 := hg n hng have hb := hn₀ n hn₀' simpa [abs_of_nonneg hf0, abs_of_nonneg hg0] using And.intro hf0 (And.intro hg0 hb) · rintro ⟨c₁, c₂, hc₁, hc₂, n₀, hn₀⟩ apply (isBigTheta_iff_sharedThreshold f g).mpr refine ⟨c₁, c₂, hc₁, hc₂, n₀, ?_⟩ intro n hn have hb := hn₀ n hn simpa [abs_of_nonneg hb.1, abs_of_nonneg hb.2.1] using hb.2.2

CLRS's strict, eventually nonnegative definition of little-o.

theorem isLittleO_iff_clrs_strict {f g : ℕ → ℝ} (hf : ∀ᶠ n in atTop, 0 ≤ f n) (hg : ∀ᶠ n in atTop, 0 < g n) : isLittleO f g ↔ ∀ c : ℝ, 0 < c → ∃ n₀ : ℕ, ∀ n, n₀ ≤ n → 0 ≤ f n ∧ f n < c * g n := by rw [Filter.eventually_atTop] at hf hg rcases hf with ⟨nf, hf⟩ rcases hg with ⟨ng, hg⟩ constructor · intro h c hc rcases (isLittleO_iff f g).mp h (c / 2) (by positivity) with ⟨n₀, hn₀⟩ refine ⟨max n₀ (max nf ng), ?_⟩ intro n hn have hn₀' : n₀ ≤ n := le_trans (le_max_left _ _) hn have hnf : nf ≤ n := le_trans (le_max_left nf ng) (le_trans (le_max_right n₀ _) hn) have hng : ng ≤ n := le_trans (le_max_right nf ng) (le_trans (le_max_right n₀ _) hn) have hf0 := hf n hnf have hg0 := hg n hng have hb := hn₀ n hn₀' rw [abs_of_nonneg hf0, abs_of_pos hg0] at hb constructor · exact hf0 · nlinarith [mul_pos hc hg0] · intro h apply (isLittleO_iff f g).mpr intro c hc rcases h c hc with ⟨n₀, hn₀⟩ refine ⟨max n₀ ng, ?_⟩ intro n hn have hn₀' : n₀ ≤ n := le_trans (le_max_left _ _) hn have hng : ng ≤ n := le_trans (le_max_right _ _) hn have hb := hn₀ n hn₀' simpa [abs_of_nonneg hb.1, abs_of_pos (hg n hng)] using hb.2.le

CLRS's strict, eventually nonnegative definition of little-omega.

theorem isLittleOmega_iff_clrs_strict {f g : ℕ → ℝ} (hf : ∀ᶠ n in atTop, 0 < f n) (hg : ∀ᶠ n in atTop, 0 ≤ g n) : isLittleOmega f g ↔ ∀ c : ℝ, 0 < c → ∃ n₀ : ℕ, ∀ n, n₀ ≤ n → 0 ≤ g n ∧ c * g n < f n := by rw [Filter.eventually_atTop] at hf hg rcases hf with ⟨nf, hf⟩ rcases hg with ⟨ng, hg⟩ constructor · intro h c hc rcases (isLittleOmega_iff f g).mp h (2 * c) (by positivity) with ⟨n₀, hn₀⟩ refine ⟨max n₀ (max nf ng), ?_⟩ intro n hn have hn₀' : n₀ ≤ n := le_trans (le_max_left _ _) hn have hnf : nf ≤ n := le_trans (le_max_left nf ng) (le_trans (le_max_right n₀ _) hn) have hng : ng ≤ n := le_trans (le_max_right nf ng) (le_trans (le_max_right n₀ _) hn) have hf0 := hf n hnf have hg0 := hg n hng have hb := hn₀ n hn₀' rw [abs_of_pos hf0, abs_of_nonneg hg0] at hb constructor · exact hg0 · nlinarith [mul_nonneg hc.le hg0] · intro h apply (isLittleOmega_iff f g).mpr intro c hc rcases h c hc with ⟨n₀, hn₀⟩ refine ⟨max n₀ nf, ?_⟩ intro n hn have hn₀' : n₀ ≤ n := le_trans (le_max_left _ _) hn have hnf : nf ≤ n := le_trans (le_max_right _ _) hn have hb := hn₀ n hn₀' simpa [abs_of_pos (hf n hnf), abs_of_nonneg hb.1] using hb.2.le

Little-o is transitive.

theorem isLittleO_trans {f g h : ℕ → ℝ} (hfg : isLittleO f g) (hgh : isLittleO g h) : isLittleO f h := by unfold isLittleO at hfg hgh ⊢ exact hfg.trans hgh

Little-omega is transitive.

theorem isLittleOmega_trans {f g h : ℕ → ℝ} (hfg : isLittleOmega f g) (hgh : isLittleOmega g h) : isLittleOmega f h := by unfold isLittleOmega at hfg hgh ⊢ exact hgh.trans hfg
Real-domain variants

CLRS permits the independent variable to range over either naturals or reals. The discrete wrappers remain the default elsewhere in this repository; these definitions expose the corresponding real-at-infinity interface without duplicating Mathlib's mature witness theory.

def isBigOReal (f g : ℝ → ℝ) : Prop := f =O[atTop] gdef isBigOmegaReal (f g : ℝ → ℝ) : Prop := g =O[atTop] fdef isBigThetaReal (f g : ℝ → ℝ) : Prop := isBigOReal f g ∧ isBigOmegaReal f gdef isLittleOReal (f g : ℝ → ℝ) : Prop := f =o[atTop] gdef isLittleOmegaReal (f g : ℝ → ℝ) : Prop := g =o[atTop] ftheorem isLittleOReal_trans {f g h : ℝ → ℝ} (hfg : isLittleOReal f g) (hgh : isLittleOReal g h) : isLittleOReal f h := by unfold isLittleOReal at hfg hgh ⊢ exact hfg.trans hghtheorem isLittleOmegaReal_trans {f g h : ℝ → ℝ} (hfg : isLittleOmegaReal f g) (hgh : isLittleOmegaReal g h) : isLittleOmegaReal f h := by unfold isLittleOmegaReal at hfg hgh ⊢ exact hgh.trans hfgend Chapter03end CLRS
Imports
import CLRSLean.FourthEdition.Chapter_03.Section_03_1_Asymptotic_Notation.Core import CLRSLean.FourthEdition.Chapter_03.Section_03_1_Asymptotic_Notation.CLRSBridge

3.2. Asymptotic Notation: Formal Definitions

This fourth-edition reader facade presents the formal definitions and laws for the five asymptotic relations. The implementation is shared with Section 3.1, but this page gives Section 3.2 its own canonical route and proof inventory.

Definitions

The imported development defines isBigO, isBigOmega, isBigTheta, isLittleO, and isLittleOmega over natural inputs, together with real-domain variants.

Main results

Status: proved for the formal asymptotic relations and the stated textbook bridges.

Definitions and proofs

CLRSLean.FourthEdition.Chapter_03.Section_03_1_Asymptotic_Notation.Core

open Filteropen Asymptotics

3.1. Asymptotic Notation

CLRS-compatible wrappers for mathlib's filter-based asymptotics on ℕ → ℝ. Proves equivalence between the CLRS discrete definition and the filter definition, plus standard algebraic properties: the Θ characterization with a single shared threshold, the o/ω and O/Ω dualities, and the little-o closure properties (additivity, products, composition) used in the growth estimates of fourth-edition §3.3.

namespace CLRSnamespace Chapter03
Wrapper definitions
def isBigO (f g : ℕ → ℝ) : Prop := f =O[atTop] gdef isBigOmega (f g : ℕ → ℝ) : Prop := g =O[atTop] fdef isBigTheta (f g : ℕ → ℝ) : Prop := isBigO f g ∧ isBigOmega f gdef isLittleO (f g : ℕ → ℝ) : Prop := f =o[atTop] gdef isLittleOmega (f g : ℕ → ℝ) : Prop := g =o[atTop] f
Equivalence with CLRS discrete definition
theorem isBigO_iff (f g : ℕ → ℝ) : isBigO f g ↔ ∃ (c : ℝ), c > 0 ∧ ∃ (n₀ : ℕ), ∀ n, n ≥ n₀ → |f n| ≤ c * |g n| := by unfold isBigO rw [IsBigO_def] constructor · rintro ⟨c, hc⟩ rcases IsBigOWith.exists_pos hc with ⟨c', hc_pos, hc'⟩ have hevent := (isBigOWith_iff.mp hc') have hevent' : ∀ᶠ n in atTop, |f n| ≤ c' * |g n| := by simpa [Real.norm_eq_abs] using hevent rw [Filter.eventually_atTop] at hevent' rcases hevent' with ⟨n₀, hn₀⟩ exact ⟨c', hc_pos, n₀, hn₀⟩ · rintro ⟨c, hc_pos, n₀, hn₀⟩ have hevent : ∀ᶠ n in atTop, |f n| ≤ c * |g n| := by rw [Filter.eventually_atTop] exact ⟨n₀, hn₀⟩ have hevent' : ∀ᶠ n in atTop, ‖f n‖ ≤ c * ‖g n‖ := by simpa [Real.norm_eq_abs] using hevent have hOwith : IsBigOWith c atTop f g := isBigOWith_iff.mpr hevent' exact ⟨c, hOwith⟩ theorem isLittleO_iff (f g : ℕ → ℝ) : isLittleO f g ↔ ∀ (c : ℝ), c > 0 → ∃ (n₀ : ℕ), ∀ n, n ≥ n₀ → |f n| ≤ c * |g n| := by unfold isLittleO rw [isLittleO_iff_forall_isBigOWith] constructor · intro h c hc_pos have hOwith : IsBigOWith c atTop f g := h hc_pos have hevent := (isBigOWith_iff.mp hOwith) have hevent' : ∀ᶠ n in atTop, |f n| ≤ c * |g n| := by simpa [Real.norm_eq_abs] using hevent rw [Filter.eventually_atTop] at hevent' rcases hevent' with ⟨n₀, hn₀⟩ exact ⟨n₀, hn₀⟩ · intro h c hc_pos rcases h c hc_pos with ⟨n₀, hn₀⟩ have hevent : ∀ᶠ n in atTop, |f n| ≤ c * |g n| := by rw [Filter.eventually_atTop] exact ⟨n₀, hn₀⟩ have hevent' : ∀ᶠ n in atTop, ‖f n‖ ≤ c * ‖g n‖ := by simpa [Real.norm_eq_abs] using hevent exact isBigOWith_iff.mpr hevent' theorem isBigOmega_iff (f g : ℕ → ℝ) : isBigOmega f g ↔ ∃ (c : ℝ), c > 0 ∧ ∃ (n₀ : ℕ), ∀ n, n ≥ n₀ → c * |g n| ≤ |f n| := by -- isBigOmega f g = isBigO g f, and isBigO_iff g f gives -- isBigO g f ↔ ∃ c>0, n₀, ∀ n≥n₀, |g n| ≤ c * |f n| -- We prove this RHS is equivalent to -- ∃ c>0, n₀, ∀ n≥n₀, c * |g n| ≤ |f n| -- by exchanging c ↔ c⁻¹. have h_base := isBigO_iff g f -- isBigOmega f g = isBigO g f definitionally -- Now the goal is: isBigO g f ↔ ∃ c>0, n₀, ∀ n≥n₀, c * |g n| ≤ |f n| -- But h_base says: isBigO g f ↔ ∃ c>0, n₀, ∀ n≥n₀, |g n| ≤ c * |f n| -- So it suffices to show the two RHSs are equivalent. constructor · -- From isBigO g f, get ∃ c>0, n₀, ∀ n≥n₀, |g n| ≤ c * |f n| -- Transform to ∃ c'>0, n₀, ∀ n≥n₀, c' * |g n| ≤ |f n| via c' = c⁻¹ intro h_isO rcases h_base.mp h_isO with ⟨c, hc_pos, n₀, hn₀⟩ have hc_ne_zero : c ≠ 0 := by linarith refine ⟨c⁻¹, inv_pos.mpr hc_pos, n₀, λ n hn => ?_⟩ have hineq := hn₀ n hn calc c⁻¹ * |g n| ≤ c⁻¹ * (c * |f n|) := by gcongr _ = (c⁻¹ * c) * |f n| := by ring _ = 1 * |f n| := by field_simp [hc_ne_zero] _ = |f n| := by simp · intro h_omega rcases h_omega with ⟨c, hc_pos, n₀, hn₀⟩ have hc_ne_zero : c ≠ 0 := by linarith -- Need to show isBigO g f, i.e. ∃ c'>0, n₀, ∀ n≥n₀, |g n| ≤ c' * |f n| -- Using c' = c⁻¹ apply h_base.mpr refine ⟨c⁻¹, inv_pos.mpr hc_pos, n₀, λ n hn => ?_⟩ have hineq := hn₀ n hn calc |g n| = (c⁻¹ * c) * |g n| := by field_simp [hc_ne_zero] _ = c⁻¹ * (c * |g n|) := by ring _ ≤ c⁻¹ * |f n| := by gcongr theorem isLittleOmega_iff (f g : ℕ → ℝ) : isLittleOmega f g ↔ ∀ (c : ℝ), c > 0 → ∃ (n₀ : ℕ), ∀ n, n ≥ n₀ → c * |g n| ≤ |f n| := by -- isLittleOmega f g = isLittleO g f -- isLittleO_iff g f says: isLittleO g f ↔ ∀ c>0, ∃ n₀, |g n| ≤ c * |f n| -- We need to show the RHS is equivalent to ∀ c>0, c * |g n| ≤ |f n| -- via exchanging c ↔ c⁻¹. have h_base := isLittleO_iff g f -- isLittleOmega f g = isLittleO g f definitionally constructor · intro h_o c hc have hc_inv_pos : c⁻¹ > 0 := inv_pos.mpr hc rcases (h_base.mp h_o) c⁻¹ hc_inv_pos with ⟨n₀, hn₀⟩ have hc_ne_zero : c ≠ 0 := by linarith refine ⟨n₀, λ n hn => ?_⟩ have hineq := hn₀ n hn calc c * |g n| ≤ c * (c⁻¹ * |f n|) := by gcongr _ = (c * c⁻¹) * |f n| := by ring _ = 1 * |f n| := by field_simp [hc_ne_zero] _ = |f n| := by simp · intro h_forall apply h_base.mpr intro c' hc'_pos have hc_inv_pos : c'⁻¹ > 0 := inv_pos.mpr hc'_pos rcases h_forall c'⁻¹ hc_inv_pos with ⟨n₀, hn₀⟩ have hc_ne_zero : c' ≠ 0 := by linarith refine ⟨n₀, λ n hn => ?_⟩ have hineq := hn₀ n hn calc |g n| = c' * (c'⁻¹ * |g n|) := by field_simp [hc_ne_zero] _ ≤ c' * |f n| := by gcongr
Algebraic properties
theorem isBigO_refl (f : ℕ → ℝ) : isBigO f f := by unfold isBigO exact Asymptotics.isBigO_refl f atToptheorem isBigOmega_refl (f : ℕ → ℝ) : isBigOmega f f := isBigO_refl ftheorem isBigTheta_refl (f : ℕ → ℝ) : isBigTheta f f := ⟨isBigO_refl f, isBigOmega_refl f⟩theorem isBigO_trans {f g h : ℕ → ℝ} (hfg : isBigO f g) (hgh : isBigO g h) : isBigO f h := by unfold isBigO at hfg hgh ⊢ exact IsBigO.trans hfg hghtheorem isBigOmega_trans {f g h : ℕ → ℝ} (hfg : isBigOmega f g) (hgh : isBigOmega g h) : isBigOmega f h := by unfold isBigOmega at hfg hgh ⊢ exact IsBigO.trans hgh hfgtheorem isBigTheta_symm {f g : ℕ → ℝ} (h : isBigTheta f g) : isBigTheta g f := ⟨h.2, h.1⟩theorem isBigTheta_trans {f g h : ℕ → ℝ} (hfg : isBigTheta f g) (hgh : isBigTheta g h) : isBigTheta f h := ⟨isBigO_trans hfg.1 hgh.1, isBigOmega_trans hfg.2 hgh.2⟩theorem isBigO_add {f₁ f₂ g : ℕ → ℝ} (h₁ : isBigO f₁ g) (h₂ : isBigO f₂ g) : isBigO (λ n => f₁ n + f₂ n) g := by unfold isBigO at h₁ h₂ ⊢ exact IsBigO.add h₁ h₂theorem isBigTheta_iff (f g : ℕ → ℝ) : isBigTheta f g ↔ isBigO f g ∧ isBigO g f := by simp [isBigTheta, isBigOmega, isBigO]
Shared threshold for Θ and dualities

Theorem (Θ with a shared threshold). f = Θ(g) iff there exist positive constants c₁, c₂ and a single threshold n₀ such that for all n ≥ n₀, c₁ * |g n| ≤ |f n| ≤ c₂ * |g n|.

This is the two-sided witness characterization of Θ-notation from CLRS §3.1; the two independent witnesses are combined by taking the maximum of their thresholds.

theorem isBigTheta_iff_sharedThreshold (f g : ℕ → ℝ) : isBigTheta f g ↔ ∃ c₁ c₂ : ℝ, 0 < c₁ ∧ 0 < c₂ ∧ ∃ n₀ : ℕ, ∀ n, n₀ ≤ n → c₁ * |g n| ≤ |f n| ∧ |f n| ≤ c₂ * |g n| := by rw [isBigTheta_iff] rw [show isBigO g f ↔ isBigOmega f g by simp [isBigO, isBigOmega]] rw [isBigO_iff, isBigOmega_iff] constructor · rintro ⟨hO, hΩ⟩ rcases hO with ⟨c₂, hc₂, n₀₂, h₂⟩ rcases hΩ with ⟨c₁, hc₁, n₀₁, h₁⟩ refine ⟨c₁, c₂, hc₁, hc₂, max n₀₁ n₀₂, ?_⟩ intro n hn exact ⟨h₁ n (le_trans (le_max_left n₀₁ n₀₂) hn), h₂ n (le_trans (le_max_right n₀₁ n₀₂) hn)⟩ · rintro ⟨c₁, c₂, hc₁, hc₂, n₀, h⟩ constructor · refine ⟨c₂, hc₂, n₀, ?_⟩ intro n hn exact (h n hn).2 · refine ⟨c₁, hc₁, n₀, ?_⟩ intro n hn exact (h n hn).1

Lemma (duality of o and ω). f = o(g) iff g = ω(f) (CLRS §3.1, with the convention isLittleOmega f g := isLittleO g f).

theorem isLittleO_reciprocal (f g : ℕ → ℝ) : isLittleO f g ↔ isLittleOmega g f := by simp [isLittleO, isLittleOmega]

Lemma (duality of O and Ω). f = O(g) iff g = Ω(f) (CLRS §3.1, with the convention isBigOmega f g := isBigO g f).

theorem isBigO_reciprocal (f g : ℕ → ℝ) : isBigO f g ↔ isBigOmega g f := by simp [isBigO, isBigOmega]
Little-o and little-omega algebra

Lemma. Little-o implies big-O: if f = o(g) then f = O(g) (CLRS §3.1).

theorem isLittleO_isBigO {f g : ℕ → ℝ} : isLittleO f g → isBigO f g := by intro h unfold isLittleO at h unfold isBigO exact h.isBigO

Lemma (additivity of o). If f₁ = o(g) and f₂ = o(g), then f₁ + f₂ = o(g) (CLRS §3.1).

theorem isLittleO_add {f₁ f₂ g : ℕ → ℝ} : isLittleO f₁ g → isLittleO f₂ g → isLittleO (fun n => f₁ n + f₂ n) g := by intro h₁ h₂ unfold isLittleO at h₁ h₂ ⊢ exact h₁.add h₂

Lemma (product rule). If f₁ = o(g₁) and f₂ = O(g₂), then f₁ * f₂ = o(g₁ * g₂) (CLRS §3.1).

theorem isLittleO_mul {f₁ g₁ f₂ g₂ : ℕ → ℝ} : isLittleO f₁ g₁ → isBigO f₂ g₂ → isLittleO (fun n => f₁ n * f₂ n) (fun n => g₁ n * g₂ n) := by intro h₁ h₂ unfold isLittleO at h₁ ⊢ unfold isBigO at h₂ exact h₁.mul_isBigO h₂

Lemma (composition of o). If h : ℕ → ℕ tends to infinity and f = o(g), then f ∘ h = o(g ∘ h). This is the asymptotic analogue of substituting h n for n, as used in the growth estimates of fourth-edition CLRS §§3.2–3.3.

theorem isLittleO_comp {f g : ℕ → ℝ} {h : ℕ → ℕ} (hh : Tendsto h atTop atTop) : isLittleO f g → isLittleO (fun n => f (h n)) (fun n => g (h n)) := by intro hfg unfold isLittleO at hfg ⊢ exact hfg.comp_tendsto hh

Lemma (scaling ω). If c > 0 and f = ω(g), then c * f = ω(g) (CLRS §3.1: positive constant factors are irrelevant in asymptotic notation).

theorem isLittleOmega_scale {f g : ℕ → ℝ} {c : ℝ} (hc : 0 < c) : isLittleOmega f g → isLittleOmega (fun n => c * f n) g := by intro h unfold isLittleOmega at h ⊢ exact h.const_mul_right (ne_of_gt hc)

Lemma (ω survives addition of a dominated term). If f = ω(g) and h = O(g), then f + h = ω(g) (CLRS §3.1: adding an O(g) term does not change the ω(g) lower bound).

theorem isLittleOmega_add_dominated {f g h : ℕ → ℝ} : isLittleOmega f g → isBigO h g → isLittleOmega (fun n => f n + h n) g := by intro hfg hh have h_ho : isLittleO h f := by unfold isBigO at hh unfold isLittleO exact hh.trans_isLittleO hfg rw [isLittleOmega_iff] at hfg rw [isLittleO_iff] at h_ho rw [isLittleOmega_iff] intro c hc rcases hfg (2 * c) (by positivity) with ⟨n₁, hn₁⟩ rcases h_ho (1 / 2) (by norm_num) with ⟨n₂, hn₂⟩ refine ⟨max n₁ n₂, ?_⟩ intro n hn have hn₁' : n₁ ≤ n := le_trans (le_max_left n₁ n₂) hn have hn₂' : n₂ ≤ n := le_trans (le_max_right n₁ n₂) hn have hg : (2 * c) * |g n| ≤ |f n| := hn₁ n hn₁' have hh' : |h n| ≤ (1 / 2) * |f n| := hn₂ n hn₂' have htri : |f n| - |h n| ≤ |f n + h n| := by have h₁ : |f n| ≤ |f n + h n| + |h n| := by calc |f n| = |(f n + h n) + (-h n)| := by congr 1; ring _ ≤ |f n + h n| + |(-h n)| := abs_add_le (f n + h n) (-(h n)) _ = |f n + h n| + |h n| := by rw [abs_neg] linarith calc c * |g n| = (1 / 2) * (2 * c * |g n|) := by ring _ ≤ (1 / 2) * |f n| := by gcongr _ ≤ |f n| - |h n| := by linarith _ ≤ |f n + h n| := htri
end Chapter03end CLRS

CLRSLean.FourthEdition.Chapter_03.Section_03_1_Asymptotic_Notation.CLRSBridge

open Filteropen Asymptotics

CLRS-facing bridges for asymptotic notation

The core relations use norms, as Mathlib does, so that they remain meaningful for signed functions. CLRS prints inequalities without absolute values and silently works with eventually nonnegative running-time functions. The first five theorems make that representation boundary exact. The strict little-o and little-omega forms additionally require the comparison side to be eventually positive; without that assumption a strict inequality can fail at infinitely many common zeros even though the norm-based little-o relation holds.

namespace CLRSnamespace Chapter03

CLRS's nonnegative witness form of big-O.

theorem isBigO_iff_clrs {f g : ℕ → ℝ} (hf : ∀ᶠ n in atTop, 0 ≤ f n) (hg : ∀ᶠ n in atTop, 0 ≤ g n) : isBigO f g ↔ ∃ c : ℝ, 0 < c ∧ ∃ n₀ : ℕ, ∀ n, n₀ ≤ n → 0 ≤ f n ∧ f n ≤ c * g n := by rw [Filter.eventually_atTop] at hf hg rcases hf with ⟨nf, hf⟩ rcases hg with ⟨ng, hg⟩ constructor · intro h rcases (isBigO_iff f g).mp h with ⟨c, hc, n₀, hn₀⟩ refine ⟨c, hc, max n₀ (max nf ng), ?_⟩ intro n hn have hn₀' : n₀ ≤ n := le_trans (le_max_left _ _) hn have hnf : nf ≤ n := le_trans (le_max_left nf ng) (le_trans (le_max_right n₀ _) hn) have hng : ng ≤ n := le_trans (le_max_right nf ng) (le_trans (le_max_right n₀ _) hn) have hf0 := hf n hnf have hg0 := hg n hng simpa [abs_of_nonneg hf0, abs_of_nonneg hg0] using And.intro hf0 (hn₀ n hn₀') · rintro ⟨c, hc, n₀, hn₀⟩ apply (isBigO_iff f g).mpr refine ⟨c, hc, max n₀ ng, ?_⟩ intro n hn have hn₀' : n₀ ≤ n := le_trans (le_max_left _ _) hn have hng : ng ≤ n := le_trans (le_max_right _ _) hn have hfg := hn₀ n hn₀' simpa [abs_of_nonneg hfg.1, abs_of_nonneg (hg n hng)] using hfg.2

CLRS's nonnegative witness form of big-Omega.

theorem isBigOmega_iff_clrs {f g : ℕ → ℝ} (hf : ∀ᶠ n in atTop, 0 ≤ f n) (hg : ∀ᶠ n in atTop, 0 ≤ g n) : isBigOmega f g ↔ ∃ c : ℝ, 0 < c ∧ ∃ n₀ : ℕ, ∀ n, n₀ ≤ n → 0 ≤ g n ∧ c * g n ≤ f n := by rw [Filter.eventually_atTop] at hf hg rcases hf with ⟨nf, hf⟩ rcases hg with ⟨ng, hg⟩ constructor · intro h rcases (isBigOmega_iff f g).mp h with ⟨c, hc, n₀, hn₀⟩ refine ⟨c, hc, max n₀ (max nf ng), ?_⟩ intro n hn have hn₀' : n₀ ≤ n := le_trans (le_max_left _ _) hn have hnf : nf ≤ n := le_trans (le_max_left nf ng) (le_trans (le_max_right n₀ _) hn) have hng : ng ≤ n := le_trans (le_max_right nf ng) (le_trans (le_max_right n₀ _) hn) have hf0 := hf n hnf have hg0 := hg n hng simpa [abs_of_nonneg hf0, abs_of_nonneg hg0] using And.intro hg0 (hn₀ n hn₀') · rintro ⟨c, hc, n₀, hn₀⟩ apply (isBigOmega_iff f g).mpr refine ⟨c, hc, max n₀ nf, ?_⟩ intro n hn have hn₀' : n₀ ≤ n := le_trans (le_max_left _ _) hn have hnf : nf ≤ n := le_trans (le_max_right _ _) hn have hfg := hn₀ n hn₀' simpa [abs_of_nonneg (hf n hnf), abs_of_nonneg hfg.1] using hfg.2

CLRS's two-sided nonnegative definition of Theta.

theorem isBigTheta_iff_clrs {f g : ℕ → ℝ} (hf : ∀ᶠ n in atTop, 0 ≤ f n) (hg : ∀ᶠ n in atTop, 0 ≤ g n) : isBigTheta f g ↔ ∃ c₁ c₂ : ℝ, 0 < c₁ ∧ 0 < c₂ ∧ ∃ n₀ : ℕ, ∀ n, n₀ ≤ n → 0 ≤ f n ∧ 0 ≤ g n ∧ c₁ * g n ≤ f n ∧ f n ≤ c₂ * g n := by rw [Filter.eventually_atTop] at hf hg rcases hf with ⟨nf, hf⟩ rcases hg with ⟨ng, hg⟩ constructor · intro h rcases (isBigTheta_iff_sharedThreshold f g).mp h with ⟨c₁, c₂, hc₁, hc₂, n₀, hn₀⟩ refine ⟨c₁, c₂, hc₁, hc₂, max n₀ (max nf ng), ?_⟩ intro n hn have hn₀' : n₀ ≤ n := le_trans (le_max_left _ _) hn have hnf : nf ≤ n := le_trans (le_max_left nf ng) (le_trans (le_max_right n₀ _) hn) have hng : ng ≤ n := le_trans (le_max_right nf ng) (le_trans (le_max_right n₀ _) hn) have hf0 := hf n hnf have hg0 := hg n hng have hb := hn₀ n hn₀' simpa [abs_of_nonneg hf0, abs_of_nonneg hg0] using And.intro hf0 (And.intro hg0 hb) · rintro ⟨c₁, c₂, hc₁, hc₂, n₀, hn₀⟩ apply (isBigTheta_iff_sharedThreshold f g).mpr refine ⟨c₁, c₂, hc₁, hc₂, n₀, ?_⟩ intro n hn have hb := hn₀ n hn simpa [abs_of_nonneg hb.1, abs_of_nonneg hb.2.1] using hb.2.2

CLRS's strict, eventually nonnegative definition of little-o.

theorem isLittleO_iff_clrs_strict {f g : ℕ → ℝ} (hf : ∀ᶠ n in atTop, 0 ≤ f n) (hg : ∀ᶠ n in atTop, 0 < g n) : isLittleO f g ↔ ∀ c : ℝ, 0 < c → ∃ n₀ : ℕ, ∀ n, n₀ ≤ n → 0 ≤ f n ∧ f n < c * g n := by rw [Filter.eventually_atTop] at hf hg rcases hf with ⟨nf, hf⟩ rcases hg with ⟨ng, hg⟩ constructor · intro h c hc rcases (isLittleO_iff f g).mp h (c / 2) (by positivity) with ⟨n₀, hn₀⟩ refine ⟨max n₀ (max nf ng), ?_⟩ intro n hn have hn₀' : n₀ ≤ n := le_trans (le_max_left _ _) hn have hnf : nf ≤ n := le_trans (le_max_left nf ng) (le_trans (le_max_right n₀ _) hn) have hng : ng ≤ n := le_trans (le_max_right nf ng) (le_trans (le_max_right n₀ _) hn) have hf0 := hf n hnf have hg0 := hg n hng have hb := hn₀ n hn₀' rw [abs_of_nonneg hf0, abs_of_pos hg0] at hb constructor · exact hf0 · nlinarith [mul_pos hc hg0] · intro h apply (isLittleO_iff f g).mpr intro c hc rcases h c hc with ⟨n₀, hn₀⟩ refine ⟨max n₀ ng, ?_⟩ intro n hn have hn₀' : n₀ ≤ n := le_trans (le_max_left _ _) hn have hng : ng ≤ n := le_trans (le_max_right _ _) hn have hb := hn₀ n hn₀' simpa [abs_of_nonneg hb.1, abs_of_pos (hg n hng)] using hb.2.le

CLRS's strict, eventually nonnegative definition of little-omega.

theorem isLittleOmega_iff_clrs_strict {f g : ℕ → ℝ} (hf : ∀ᶠ n in atTop, 0 < f n) (hg : ∀ᶠ n in atTop, 0 ≤ g n) : isLittleOmega f g ↔ ∀ c : ℝ, 0 < c → ∃ n₀ : ℕ, ∀ n, n₀ ≤ n → 0 ≤ g n ∧ c * g n < f n := by rw [Filter.eventually_atTop] at hf hg rcases hf with ⟨nf, hf⟩ rcases hg with ⟨ng, hg⟩ constructor · intro h c hc rcases (isLittleOmega_iff f g).mp h (2 * c) (by positivity) with ⟨n₀, hn₀⟩ refine ⟨max n₀ (max nf ng), ?_⟩ intro n hn have hn₀' : n₀ ≤ n := le_trans (le_max_left _ _) hn have hnf : nf ≤ n := le_trans (le_max_left nf ng) (le_trans (le_max_right n₀ _) hn) have hng : ng ≤ n := le_trans (le_max_right nf ng) (le_trans (le_max_right n₀ _) hn) have hf0 := hf n hnf have hg0 := hg n hng have hb := hn₀ n hn₀' rw [abs_of_pos hf0, abs_of_nonneg hg0] at hb constructor · exact hg0 · nlinarith [mul_nonneg hc.le hg0] · intro h apply (isLittleOmega_iff f g).mpr intro c hc rcases h c hc with ⟨n₀, hn₀⟩ refine ⟨max n₀ nf, ?_⟩ intro n hn have hn₀' : n₀ ≤ n := le_trans (le_max_left _ _) hn have hnf : nf ≤ n := le_trans (le_max_right _ _) hn have hb := hn₀ n hn₀' simpa [abs_of_pos (hf n hnf), abs_of_nonneg hb.1] using hb.2.le

Little-o is transitive.

theorem isLittleO_trans {f g h : ℕ → ℝ} (hfg : isLittleO f g) (hgh : isLittleO g h) : isLittleO f h := by unfold isLittleO at hfg hgh ⊢ exact hfg.trans hgh

Little-omega is transitive.

theorem isLittleOmega_trans {f g h : ℕ → ℝ} (hfg : isLittleOmega f g) (hgh : isLittleOmega g h) : isLittleOmega f h := by unfold isLittleOmega at hfg hgh ⊢ exact hgh.trans hfg
Real-domain variants

CLRS permits the independent variable to range over either naturals or reals. The discrete wrappers remain the default elsewhere in this repository; these definitions expose the corresponding real-at-infinity interface without duplicating Mathlib's mature witness theory.

def isBigOReal (f g : ℝ → ℝ) : Prop := f =O[atTop] gdef isBigOmegaReal (f g : ℝ → ℝ) : Prop := g =O[atTop] fdef isBigThetaReal (f g : ℝ → ℝ) : Prop := isBigOReal f g ∧ isBigOmegaReal f gdef isLittleOReal (f g : ℝ → ℝ) : Prop := f =o[atTop] gdef isLittleOmegaReal (f g : ℝ → ℝ) : Prop := g =o[atTop] ftheorem isLittleOReal_trans {f g h : ℝ → ℝ} (hfg : isLittleOReal f g) (hgh : isLittleOReal g h) : isLittleOReal f h := by unfold isLittleOReal at hfg hgh ⊢ exact hfg.trans hghtheorem isLittleOmegaReal_trans {f g h : ℝ → ℝ} (hfg : isLittleOmegaReal f g) (hgh : isLittleOmegaReal g h) : isLittleOmegaReal f h := by unfold isLittleOmegaReal at hfg hgh ⊢ exact hgh.trans hfgend Chapter03end CLRS
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 ntheorem 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

Scope and implementation notes

Imports
import CLRSLean.FourthEdition.Chapter_03.Section_03_1_Asymptotic_Notation import CLRSLean.FourthEdition.Chapter_03.Section_03_2_Asymptotic_Notation_Formal_Definitions import CLRSLean.FourthEdition.Chapter_03.Section_03_3_Standard_Notations_And_Common_Functions

Native fourth-edition chapter guide.

Current source

This guide presents each fourth-edition section through its own canonical reader page: §3.1 for asymptotic notation, §3.2 for the formal definitions, and §3.3 for standard notation and common functions. Declarations retain the CLRS.Chapter03 namespace; the legacy import CLRSLean.Chapter_03 forwards to this guide during the compatibility period.

Coverage boundary

The shared asymptotic-notation implementation supplies fourth-edition §§3.1--3.2. Its core defines the five asymptotic relations, while its textbook bridge proves their equivalence to the eventually nonnegative CLRS formulations, strict o/ω characterizations, transitivity, and real-domain variants.

The standard-functions implementation supplies §3.3 through small theorem modules. It includes the textbook floor, ceiling, remainder, exponential, logarithmic, iteration, Fibonacci, and factorial identities; real-exponent growth bridges; arbitrary nonzero-polynomial leading-term asymptotics; the extended growth hierarchy through n^(log n) and n^n; and the exact effective Robbins refinement of Stirling's formula.

See docs/clrs-fourth-edition-map.csv for the section-level mapping and docs/migrations/clrs4.md for compatibility and deprecation policy.

CLRS, fourth edition · Chapter 3 of 35