Negligible bounds and real-valued estimates

The security-game API uses nonnegative advantages. Real-valued estimates, including the pinned finite PRG API, express the same decay after coercion. A positive constant advantage cannot be negligible.

Main results

• Cslib.Crypto.negligible_iff_coe: pass between nonnegative and real-valued decay bounds.
• Cslib.Crypto.Negligible.eventually_le_inv_polynomial: compare with positive polynomial losses.
• Cslib.Crypto.negligible_geometric: geometric decay of nonnegative error bounds.
• Cslib.Crypto.not_negligible_const: constant nonzero success contradicts security.
• Cslib.Crypto.Negligible.comp_of_polynomial_bound: polynomially related parameters.
• Cslib.Crypto.Negligible.div_const: division of the parameter by a positive constant.
• Cslib.Crypto.Negligible.sqrt: taking square roots preserves negligible decay.

References

The geometric, constant and inverse-polynomial bounds are adapted from Crypto/Negligible.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the current upstream nonnegative API.

theorem Cslib.Crypto.negligible_iff_coe {ε : ℕ → NNReal} : Negligible ε ↔ Asymptotics.SuperpolynomialDecay Filter.atTop (fun (n : ℕ) => ↑n) fun (n : ℕ) => ↑(ε n)

Nonnegative advantages decay negligibly exactly when their real coercions do.

theorem Cslib.Crypto.negligible_geometric {ratio : NNReal} (h : ratio < 1) : Negligible fun (n : ℕ) => ratio ^ n

Geometric decay with a nonnegative ratio strictly below one is negligible.

theorem Cslib.Crypto.not_negligible_const {c : NNReal} (hc : c ≠ 0) : ¬Negligible fun (x : ℕ) => c

A constant nonzero advantage is not negligible.

theorem Cslib.Crypto.Negligible.eventually_le_inv_polynomial {ε : ℕ → NNReal} (hε : Negligible ε) {p : ℕ → ℕ} (hp : PolynomiallyBounded p) (hpos : ∀ (n : ℕ), 0 < p n) : ∀ᶠ (n : ℕ) in Filter.atTop, ↑(ε n) ≤ 1 / ↑(p n)

Negligible success is eventually smaller than the reciprocal of any positive polynomially bounded loss. The real coercion permits comparison with analytic bounds.

theorem Cslib.Crypto.Negligible.comp_of_polynomial_bound {ε : ℕ → NNReal} {index bound : ℕ → ℕ} (hε : Negligible ε) (hindex : Filter.Tendsto index Filter.atTop Filter.atTop) (hbound : PolynomiallyBounded bound) (hle : ∀ᶠ (n : ℕ) in Filter.atTop, n ≤ bound (index n)) : Negligible fun (n : ℕ) => ε (index n)

Negligible decay survives reindexing when the new parameter tends to infinity and the old parameter is polynomially bounded in it. The reindexing function need not be computable.

theorem Cslib.Crypto.Negligible.div_const {ε : ℕ → NNReal} (hε : Negligible ε) {divisor : ℕ} (hpos : 0 < divisor) : Negligible fun (n : ℕ) => ε (n / divisor)

Dividing the security parameter by a fixed positive natural preserves negligible decay.

theorem Cslib.Crypto.Negligible.sqrt {ε : ℕ → NNReal} (hε : Negligible ε) : Negligible fun (n : ℕ) => NNReal.sqrt (ε n)

Taking a square root preserves negligible decay.

theorem Cslib.Crypto.Negligible.shift {ε : ℕ → NNReal} (hε : Negligible ε) (c : ℕ) : Negligible fun (n : ℕ) => ε (n + c)

Shifting the security parameter by a fixed additive offset preserves negligibility.