Asymptotic notation for natural number functions

This module defines Complexity.BigO and Complexity.LittleO, thin adapters that lift Mathlib's Asymptotics.IsBigO and Asymptotics.IsLittleO to ℕ → ℕ functions (casting through ℝ).

The scoped notations f =O g and f =o g are available when Complexity is opened and read like standard complexity-theoretic asymptotic notation.

Main definitions

• BigO — f =O g means f(n) = O(g(n)) as n → ∞
• LittleO — f =o g means f(n) = o(g(n)) as n → ∞

Main results

BigO

• BigO.refl — reflexivity
• BigO.trans — transitivity
• BigO.of_le — pointwise ≤ implies big-O
• BigO.add — sum of big-O is big-O
• BigO.const_mul_left — constant multiple preserves big-O
• BigO.le_add_left / BigO.le_add_right — projections from a sum
• BigO.const_mul_add — c * f₁ + f₂ = O(T₁ + T₂)

LittleO

• LittleO.isBigO — little-o implies big-O
• LittleO.trans — transitivity
• LittleO.trans_bigO — mixed: o then O gives o
• BigO.trans_littleO — mixed: O then o gives o
• LittleO.add — sum of little-o is little-o
• LittleO.const_mul_left — constant multiple preserves little-o

def Complexity.BigO (f g : ℕ → ℕ) : Prop

f grows at most as fast as g asymptotically: f(n) = O(g(n)) as n → ∞. Lifts Mathlib's Asymptotics.IsBigO to ℕ → ℕ functions, avoiding repeated Nat.cast coercions in complexity class definitions.

Unfolding: f =O g ↔ ∃ C, ∀ᶠ n in atTop, ↑(f n) ≤ C * ↑(g n).

Equations

• Complexity.BigO f g = (fun (n : ℕ) => ↑(f n)) =O[Filter.atTop] fun (n : ℕ) => ↑(g n)

def Complexity.«term_=O_» : Lean.TrailingParserDescr

f grows at most as fast as g asymptotically: f(n) = O(g(n)) as n → ∞. Lifts Mathlib's Asymptotics.IsBigO to ℕ → ℕ functions, avoiding repeated Nat.cast coercions in complexity class definitions.

Unfolding: f =O g ↔ ∃ C, ∀ᶠ n in atTop, ↑(f n) ≤ C * ↑(g n).

Equations

• Complexity.«term_=O_» = Lean.ParserDescr.trailingNode `Complexity.«term_=O_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " =O ") (Lean.ParserDescr.cat `term 51))

def Complexity.LittleO (f g : ℕ → ℕ) : Prop

f grows strictly slower than g asymptotically: f(n) = o(g(n)) as n → ∞. Lifts Mathlib's Asymptotics.IsLittleO to ℕ → ℕ functions.

Unfolding: f =o g ↔ ∀ ε > 0, ∀ᶠ n in atTop, ↑(f n) ≤ ε * ↑(g n).

Equations

• Complexity.LittleO f g = (fun (n : ℕ) => ↑(f n)) =o[Filter.atTop] fun (n : ℕ) => ↑(g n)

def Complexity.«term_=o_» : Lean.TrailingParserDescr

f grows strictly slower than g asymptotically: f(n) = o(g(n)) as n → ∞. Lifts Mathlib's Asymptotics.IsLittleO to ℕ → ℕ functions.

Unfolding: f =o g ↔ ∀ ε > 0, ∀ᶠ n in atTop, ↑(f n) ≤ ε * ↑(g n).

Equations

• Complexity.«term_=o_» = Lean.ParserDescr.trailingNode `Complexity.«term_=o_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " =o ") (Lean.ParserDescr.cat `term 51))

theorem Complexity.BigO.refl (f : ℕ → ℕ) : BigO f f

Big-O is reflexive: f = O(f).

theorem Complexity.BigO.trans {f g h : ℕ → ℕ} (h₁ : BigO f g) (h₂ : BigO g h) : BigO f h

Big-O is transitive: f = O(g) → g = O(h) → f = O(h).

theorem Complexity.BigO.of_le {f g : ℕ → ℕ} (h : ∀ (n : ℕ), f n ≤ g n) : BigO f g

Pointwise ≤ implies big-O.

theorem Complexity.BigO.add {f₁ f₂ g : ℕ → ℕ} (h₁ : BigO f₁ g) (h₂ : BigO f₂ g) : BigO (fun (n : ℕ) => f₁ n + f₂ n) g

Sum of two big-O functions: f₁ = O(g) → f₂ = O(g) → (f₁ + f₂) = O(g).

theorem Complexity.BigO.mul {f₁ f₂ g₁ g₂ : ℕ → ℕ} (h₁ : BigO f₁ g₁) (h₂ : BigO f₂ g₂) : BigO (fun (n : ℕ) => f₁ n * f₂ n) fun (n : ℕ) => g₁ n * g₂ n

Product of two big-O bounds: f₁ = O(g₁) → f₂ = O(g₂) → (f₁·f₂) = O(g₁·g₂).

theorem Complexity.BigO.const_mul_left (c : ℕ) {f g : ℕ → ℕ} (h : BigO f g) : BigO (fun (n : ℕ) => c * f n) g

Constant multiple preserves big-O.

theorem Complexity.LittleO.isBigO {f g : ℕ → ℕ} (h : LittleO f g) : BigO f g

Little-o implies big-O: if f = o(g) then f = O(g).

theorem Complexity.LittleO.trans {f g h : ℕ → ℕ} (h₁ : LittleO f g) (h₂ : LittleO g h) : LittleO f h

Little-o is transitive: f = o(g) → g = o(h) → f = o(h).

theorem Complexity.LittleO.trans_bigO {f g h : ℕ → ℕ} (h₁ : LittleO f g) (h₂ : BigO g h) : LittleO f h

Mixed transitivity: f = o(g) → g = O(h) → f = o(h).

theorem Complexity.BigO.trans_littleO {f g h : ℕ → ℕ} (h₁ : BigO f g) (h₂ : LittleO g h) : LittleO f h

Mixed transitivity: f = O(g) → g = o(h) → f = o(h).

theorem Complexity.LittleO.add {f₁ f₂ g : ℕ → ℕ} (h₁ : LittleO f₁ g) (h₂ : LittleO f₂ g) : LittleO (fun (n : ℕ) => f₁ n + f₂ n) g

Sum of two little-o functions: f₁ = o(g) → f₂ = o(g) → (f₁ + f₂) = o(g).

theorem Complexity.LittleO.const_mul_left (c : ℕ) {f g : ℕ → ℕ} (h : LittleO f g) : LittleO (fun (n : ℕ) => c * f n) g

Constant multiple preserves little-o.

theorem Complexity.BigO.le_add_left (T₁ T₂ : ℕ → ℕ) : BigO T₁ fun (n : ℕ) => T₁ n + T₂ n

T₁ is big-O of T₁ + T₂.

theorem Complexity.BigO.le_add_right (T₁ T₂ : ℕ → ℕ) : BigO T₂ fun (n : ℕ) => T₁ n + T₂ n

T₂ is big-O of T₁ + T₂.

theorem Complexity.BigO.const_mul_add (c : ℕ) {f₁ f₂ T₁ T₂ : ℕ → ℕ} (ho₁ : BigO f₁ T₁) (ho₂ : BigO f₂ T₂) : BigO (fun (n : ℕ) => c * f₁ n + f₂ n) fun (n : ℕ) => T₁ n + T₂ n

If f₁ =O T₁ and f₂ =O T₂, then c * f₁ + f₂ =O (T₁ + T₂).

theorem Complexity.BigO.le_max_left (T₁ T₂ : ℕ → ℕ) : BigO T₁ fun (n : ℕ) => max (T₁ n) (T₂ n)

T₁ is big-O of max T₁ T₂.

theorem Complexity.BigO.le_max_right (T₁ T₂ : ℕ → ℕ) : BigO T₂ fun (n : ℕ) => max (T₁ n) (T₂ n)

T₂ is big-O of max T₁ T₂.

theorem Complexity.BigO.max_le_add (T₁ T₂ : ℕ → ℕ) : BigO (fun (n : ℕ) => max (T₁ n) (T₂ n)) fun (n : ℕ) => T₁ n + T₂ n

max T₁ T₂ =O (T₁ + T₂).

theorem Complexity.BigO.self_le_add_const (f : ℕ → ℕ) (c : ℕ) : BigO f fun (n : ℕ) => f n + c

Any function is big-O of itself-plus-constant: f =O (fun n => f n + c).

theorem Complexity.BigO.pow_le_pow_succ (k : ℕ) : BigO (fun (x : ℕ) => x ^ k) fun (x : ℕ) => x ^ (k + 1)

n^k is big-O of n^(k+1) on sequences with n ≥ 1.

theorem Complexity.BigO.pow_le_pow_right {j k : ℕ} (hjk : j ≤ k) : BigO (fun (x : ℕ) => x ^ j) fun (x : ℕ) => x ^ k

n^j =O n^k when j ≤ k (on sequences with n ≥ 1).

theorem Complexity.BigO.const_le_pow (c k : ℕ) : BigO (fun (x : ℕ) => c) fun (x : ℕ) => x ^ k

A constant function is big-O of n^k (eventually n^k ≥ 1).

theorem Complexity.BigO.pow_add_pow (j k : ℕ) : BigO (fun (n : ℕ) => n ^ j + n ^ k) fun (x : ℕ) => x ^ max j k

n^j + n^k =O n^(max j k) on sequences with n ≥ 1.

theorem Complexity.BigO.pow_polynomial_bound {f : ℕ → ℕ} {k : ℕ} (h : BigO f fun (x : ℕ) => x ^ k) : ∃ (p : Polynomial ℕ), ∀ (n : ℕ), f n ≤ Polynomial.eval n p

From f =O (·^k) to an explicit polynomial bound. If f : ℕ → ℕ is big-O of n^k, then there exists a polynomial p in Polynomial ℕ with f n ≤ p.eval n for every n (not just eventually).

The standard big-O definition gives only an asymptotic bound; this lemma turns that into an everywhere-bound by (i) extracting a real constant C and threshold N such that f n ≤ C · n^k for n ≥ N, (ii) rounding C up to a natural number, and (iii) adding a constant term that dominates f on the initial segment [0, N).

This is the bridge from big-O hypotheses to the explicit Polynomial ℕ shape expected by definitions like PolyBalanced and by time-bound packaging in the WitnessNTMConstruction construction.

theorem Complexity.BigO.of_polynomial_bound {f : ℕ → ℕ} (p : Polynomial ℕ) (h : ∀ (n : ℕ), f n ≤ Polynomial.eval n p) : BigO f fun (x : ℕ) => x ^ p.natDegree

From a polynomial bound to =O (·^deg). If f : ℕ → ℕ is pointwise bounded by a polynomial p, then f =O (·^p.natDegree).

Companion to BigO.pow_polynomial_bound; the pair lets you convert freely between the big-O form used by complexity classes and the explicit Polynomial ℕ shape used in PolyBalanced and in running-time packaging for composite machines.

theorem Complexity.BigO.exists_nat_bound {f g : ℕ → ℕ} (h : BigO f g) : ∃ (c : ℕ) (N : ℕ), ∀ (n : ℕ), N ≤ n → f n ≤ c * g n

Extract a natural-number constant and threshold from a big-O bound: f =O g yields c and N with f n ≤ c * g n for all n ≥ N.

theorem Complexity.LittleO.pow_lt_pow {p q : ℕ} (hpq : p < q) : LittleO (fun (n : ℕ) => (n + 1) ^ p) fun (n : ℕ) => (n + 1) ^ q

Strict power gap, shifted to the everywhere-positive base n + 1: (n + 1)^p = o((n + 1)^q) when p < q.