Uniform random functions as Δ-universal hash families

A uniformly random function into a finite additive group has uniform differences at distinct inputs. Negating the complete function preserves its uniform law, and hence the same bound. These are information-theoretic laws; they make no efficient-sampling claim.

Main results

• Cslib.Probability.isDeltaUniversalHash_uniformOfFintype: uniform functions are Δ-universal.
• Cslib.Probability.isDeltaUniversalHash_neg_uniformOfFintype: negated uniform functions satisfy the same bound.

theorem Cslib.Probability.isDeltaUniversalHash_uniformOfFintype {X : Type u_1} {G : Type u_2} [Fintype X] [DecidableEq X] [AddGroup G] [Fintype G] [Nonempty G] : IsDeltaUniversalHash (PMF.uniformOfFintype (X → G)) id (↑(Fintype.card G))⁻¹

A uniformly random function from a finite domain X into a finite additive group G is |G|⁻¹-almost-Δ-universal.

theorem Cslib.Probability.isDeltaUniversalHash_neg_uniformOfFintype {X : Type u_1} {G : Type u_2} [Fintype X] [DecidableEq X] [AddGroup G] [Fintype G] [Nonempty G] : IsDeltaUniversalHash (PMF.uniformOfFintype (X → G)) (fun (f : X → G) (x : X) => -f x) (↑(Fintype.card G))⁻¹

The negated uniform random function f ↦ (fun x => -f x) from a finite domain X into a finite additive group G is |G|⁻¹-almost-Δ-universal.