Negligible Functions

This file defines a simple wrapper around SuperpolynomialDecay for function from ℕ → ℝ≥0∞, as this is usually the situation for cryptographic reductions.

Adding a general API might be useful, but usually unfolding to SuperpolynomialDecay is fine.

def negligible (f : ℕ → ENNReal) : Prop

A function f is negligible if it decays faster than any polynomial function.

@[simp]

def negligible_iff (f : ℕ → ENNReal) : negligible f ↔ Asymptotics.SuperpolynomialDecay Filter.atTop (fun (x : ℕ) => ↑x) f

theorem negligible_zero : negligible 0

theorem negligible_of_zero {f : ℕ → ENNReal} (hf : ∀ (n : ℕ), f n = 0) : negligible f