Skip to content
  1. CLRS-Lean
  2. Chapters 1–35 · CLRS Fourth Edition
  3. Chapter 3. Characterizing Running Times
  4. 3.2. Asymptotic Notation: Formal Definitions
Browse chapters
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