Negligible functions

A function f : ℕ → ℝ is negligible if it vanishes faster than any inverse polynomial. This is the standard notion used in cryptographic definitions.

def Complexity.Negligible (f : ℕ → ℝ) : Prop

A function f : ℕ → ℝ is negligible if for every c, |f(n)| < 1/n^c for all sufficiently large n. The threshold N is required to be positive, ensuring n > 0 and 1/n^c is well-defined.

Equations

• Complexity.Negligible f = ∀ (c : ℕ), ∃ (N : ℕ), 0 < N ∧ ∀ n ≥ N, |f n| < 1 / ↑n ^ c