Negligible Functions

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

Main Results

• negligible_zero, negligible_of_zero: The zero function is negligible.
• negligible_of_le: Monotonicity — bounded by negligible is negligible.
• negligible_add: Sum of negligible functions is negligible.
• negligible_sum: Finite sum of negligible functions is negligible.
• negligible_const_mul: Constant multiple of negligible is negligible.

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

theorem negligible_of_le {f g : ℕ → ENNReal} (hfg : ∀ (n : ℕ), f n ≤ g n) (hg : negligible g) : negligible f

Negligibility is monotone: if f ≤ g pointwise and g is negligible, then f is.

theorem negligible_add {f g : ℕ → ENNReal} (hf : negligible f) (hg : negligible g) : negligible (f + g)

Sum of two negligible functions is negligible.

theorem negligible_const_mul {f : ℕ → ENNReal} (hf : negligible f) {c : ENNReal} (hc : c ≠ ⊤) : negligible fun (n : ℕ) => c * f n

Constant multiple of a negligible function is negligible (requires c ≠ ⊤ because multiplication by ⊤ is discontinuous at 0 in ℝ≥0∞).

theorem negligible_sum {ι : Type u_1} {s : Finset ι} {f : ι → ℕ → ENNReal} (h : ∀ i ∈ s, negligible (f i)) : negligible fun (n : ℕ) => ∑ i ∈ s, f i n

A finite sum of negligible functions is negligible.

theorem negligible_pow_mul {f : ℕ → ENNReal} (hf : negligible f) (d : ℕ) : negligible fun (n : ℕ) => ↑n ^ d * f n

If f is negligible, then fun n => (↑n)^d * f n is negligible for any fixed d. Absorbs polynomial powers of the parameter into the superpolynomial decay.

theorem negligible_polynomial_mul {f : ℕ → ENNReal} (hf : negligible f) (p : Polynomial ℕ) : negligible fun (n : ℕ) => ↑(Polynomial.eval n p) * f n

If f is negligible, then fun n => ↑(p.eval n) * f n is negligible for any polynomial p. This is the key lemma for handling polynomial-loss security reductions.