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