Negligible function

Conjectura.Defs.ComputerScience.Complexity.Negligible

/-
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
-/
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Order.Filter.AtTopBot.Defs

/-! # Negligible function -/

namespace Conjectura.Complexity

/-- 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 : ℝ) ^ k

end Conjectura.Complexity