Negligible functions

Negligible bounds are nonnegative real-valued functions with Mathlib's superpolynomial decay at natural security parameters. This module supplies zero, addition, multiplication, fixed finite sums, eventual comparison, and polynomial-loss bounds for security games. Changing finitely many values preserves negligibility.

The decay bound may depend on the whole algorithm. Security definitions quantify over that algorithm before asserting negligibility; this module does not change that quantifier order.

def Cslib.Crypto.Negligible (ε : ℕ → NNReal) : Prop

An advantage is negligible when it decays faster than every inverse polynomial in the security parameter. The nonnegative codomain records that advantages are magnitudes; the decay condition is Mathlib's superpolynomial decay in the nonnegative reals.

theorem Cslib.Crypto.negligible_iff (ε : ℕ → NNReal) : Negligible ε ↔ ∀ (k : ℕ), ∀ δ > 0, ∃ (m : ℕ), ∀ n ≥ m, ↑n ^ k * ε n < δ

@[simp]

theorem Cslib.Crypto.negligible_zero : Negligible fun (x : ℕ) => 0

The zero advantage is negligible.

theorem Cslib.Crypto.Negligible.congr' {ε δ : ℕ → NNReal} (hε : Negligible ε) (h : ε =ᶠ[Filter.atTop] δ) : Negligible δ

Changing the value of a negligible bound at finitely many security parameters preserves negligibility.

theorem Cslib.Crypto.Negligible.add {ε δ : ℕ → NNReal} (hε : Negligible ε) (hδ : Negligible δ) : Negligible (ε + δ)

The sum of two negligible bounds is negligible.

theorem Cslib.Crypto.Negligible.mul {ε δ : ℕ → NNReal} (hε : Negligible ε) (hδ : Negligible δ) : Negligible (ε * δ)

The product of two negligible bounds is negligible.

theorem Cslib.Crypto.Negligible.sum {ι : Type u_1} (s : Finset ι) {ε : ι → ℕ → NNReal} (hε : ∀ i ∈ s, Negligible (ε i)) : Negligible (∑ i ∈ s, ε i)

A sum over a fixed finite set of negligible bounds is negligible.

theorem Cslib.Crypto.negligible_of_eventually_le {ε δ : ℕ → NNReal} (hδ : Negligible δ) (hle : ε ≤ᶠ[Filter.atTop] δ) : Negligible ε

An eventually smaller advantage is negligible.

theorem Cslib.Crypto.negligible_of_le {ε δ : ℕ → NNReal} (hδ : Negligible δ) (hle : ∀ (n : ℕ), ε n ≤ δ n) : Negligible ε

A pointwise smaller advantage is negligible.

theorem Cslib.Crypto.Negligible.polynomiallyBounded_mul {ε : ℕ → NNReal} {p : ℕ → ℕ} (hε : Negligible ε) (hp : PolynomiallyBounded p) : Negligible fun (n : ℕ) => ↑(p n) * ε n

Polynomially bounded factors preserve negligible decay.