Negligible function
Negligibledef
A function is negligible when it eventually falls below every inverse polynomial. In cryptography this is the formal meaning of "an adversary's success probability is too small to matter".
def Negligible (f : ℕ → ℝ) : Prop :=
∀ k : ℕ, ∀ᶠ n in Filter.atTop, |f n| ≤ 1 / (n : ℝ) ^ kimport Conjectura.Defs.ComputerScience.Complexity.Negligible · maintainer — open · raw source
Copyright (c) 2026 The Conjectura Authors. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: The Conjectura Authors