Pairwise independent families are universal

A pairwise independent (strongly universal) family with a uniform seed is 1 / |Y|-universal and, when Y is an additive group, 1 / |Y|-Δ-universal: for distinct inputs, the pair of hashes is uniform on Y × Y, so every relation h i x = g (h i x') with g : Y → Y holds on a 1 / |Y| fraction of the seeds [CW79], [WC81]. Every pairwise independent family of the library, such as the affine and Toeplitz families and polynomial hashing of degree at least one, is therefore universal and Δ-universal.

Main results

• Cslib.Probability.IsPairwiseIndependentHash.isUniversalHash: pairwise independence implies 1 / |Y|-universality.
• Cslib.Probability.IsPairwiseIndependentHash.isDeltaUniversalHash: pairwise independence implies 1 / |Y|-Δ-universality.

References

• J. L. Carter, M. N. Wegman, Universal Classes of Hash Functions
• M. N. Wegman, J. L. Carter, New Hash Functions and Their Use in Authentication and Set Equality

theorem Cslib.Probability.IsPairwiseIndependentHash.map_pair_eq_uniform {ι : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype ι] [Fintype Y] [DecidableEq Y] {h : ι → X → Y} [Nonempty ι] [Nonempty Y] (hh : IsPairwiseIndependentHash h) {x x' : X} (hx : x ≠ x') : PMF.map (fun (i : ι) => (h i x, h i x')) (PMF.uniformOfFintype ι) = PMF.uniformOfFintype (Y × Y)

For distinct inputs, the pair of hashes under a uniform seed is uniform on Y × Y.

theorem Cslib.Probability.IsPairwiseIndependentHash.toOuterMeasure_apply_eq_comp {ι : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype ι] [Fintype Y] [DecidableEq Y] {h : ι → X → Y} [Nonempty ι] (hh : IsPairwiseIndependentHash h) {x x' : X} (hx : x ≠ x') (g : Y → Y) : (PMF.uniformOfFintype ι).toOuterMeasure {i : ι | h i x = g (h i x')} = (↑(Fintype.card Y))⁻¹

For distinct inputs and any g : Y → Y, a uniform seed gives h i x = g (h i x') with probability exactly 1 / |Y|.

theorem Cslib.Probability.IsPairwiseIndependentHash.isUniversalHash {ι : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype ι] [Fintype Y] [DecidableEq Y] {h : ι → X → Y} [Nonempty ι] (hh : IsPairwiseIndependentHash h) : IsUniversalHash (PMF.uniformOfFintype ι) h (↑(Fintype.card Y))⁻¹

A pairwise independent family with a uniform seed is 1 / |Y|-universal.

theorem Cslib.Probability.IsPairwiseIndependentHash.isDeltaUniversalHash {ι : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype ι] [Fintype Y] [DecidableEq Y] {h : ι → X → Y} [AddGroup Y] [Nonempty ι] (hh : IsPairwiseIndependentHash h) : IsDeltaUniversalHash (PMF.uniformOfFintype ι) h (↑(Fintype.card Y))⁻¹

A pairwise independent family with a uniform seed, into an additive group, is 1 / |Y|-Δ-universal.