k-wise independent hash families

A family of functions h i : X → Y, indexed by a seed i drawn uniformly from a finite type ι, is k-wise independent (Cslib.Probability.IsKWiseIndependentHash) if for every set T of at most k points the restriction of h i to T is uniformly distributed on T → Y: the values at any k distinct points are independent and uniform Vadhan, Section 3.5.5; Wegman and Carter call such families strongly universal_k [WC81]. For k ≥ 2 they are pairwise independent in the sense of Cslib.Probability.IsPairwiseIndependentHash, and 2-wise independence is exactly pairwise independence with a seed (Cslib.Probability.isKWiseIndependentHash_two_iff). As in the pairwise case, probabilities over the seed are densities Finset.dens and averages are uniform expectations 𝔼 i.

Every function of at most k values has the same average as for a truly random function (Cslib.Probability.IsKWiseIndependentHash.expect_restrict); in particular the average of a product of functions of the values at k points is the product of their averages (Cslib.Probability.IsKWiseIndependentHash.expect_prod). Expanding the 2 m-th power of a sum of centered bounded scores, a tuple of points contributes only when every point occurs at least twice, so at most m distinct points occur. This gives the 2 m-th moment bound 𝔼 (∑ x ∈ S, Z x) ^ (2 m) ≤ m ^ (2 m) |S| ^ m, and Markov's inequality gives the tail bound Pr[|∑ x ∈ S, Z x| ≥ a] ≤ (m² |S| / a²) ^ m. This is the k-th moment method for limited independence of Bellare and Rompel [BR94], whose sharper counting of the contributing tuples gives a better constant.

Main definitions

• Cslib.Probability.IsKWiseIndependentHash: k-wise independent hash families.

Main results

• Cslib.Probability.IsKWiseIndependentHash.expect_restrict, Cslib.Probability.IsKWiseIndependentHash.expect_prod: functions of at most k values average as for a truly random function.
• Cslib.Probability.IsKWiseIndependentHash.isPairwiseIndependentHash, Cslib.Probability.isKWiseIndependentHash_two_iff: for k ≥ 2 the family is pairwise independent, and 2-wise independence is pairwise independence with a seed.
• Cslib.Probability.isKWiseIndependentHash_of_surjective: an additive family whose restrictions to sets of at most k points are onto is k-wise independent.
• Cslib.Probability.IsKWiseIndependentHash.expect_sum_pow_le: the 2 m-th moment bound.
• Cslib.Probability.IsKWiseIndependentHash.dens_filter_le_abs_sum, Cslib.Probability.IsKWiseIndependentHash.dens_filter_le_abs_sum_sub_expect: the tail bounds for centered scores in [-1, 1] and for scores in [0, 1].

References

• S. P. Vadhan, Pseudorandomness, Section 3.5
• M. Bellare, J. Rompel, Randomness-efficient oblivious sampling
• M. N. Wegman, J. L. Carter, New hash functions and their use in authentication and set equality

structure Cslib.Probability.IsKWiseIndependentHash {ι : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype ι] [Fintype Y] [DecidableEq Y] (k : ℕ) (h : ι → X → Y) : Prop

A family of functions h i : X → Y, indexed by a seed i : ι drawn uniformly at random, is k-wise independent if for every set T of at most k points the restriction of h i to T is uniformly distributed on T → Y: a 1 / |Y| ^ #T fraction of the seeds restricts to each y : T → Y. Taking T = ∅ forces a seed to exist.

The usual definition asks this only for sets of exactly k points. When X has at least k elements the two agree, since a set of fewer points extends to one of k points and the restriction to the smaller set is a marginal; when X has fewer than k elements the usual definition is vacuous, while this one still asks for uniformity on all of X.

• dens_filter_restrict_eq {T : Finset X} (hT : T.card ≤ k) (y : ↥T → Y) : {i : ι | T.restrict (h i) = y}.dens = (↑(Fintype.card Y) ^ T.card)⁻¹

  The values at any set of at most k points are independent and uniform.

theorem Cslib.Probability.IsKWiseIndependentHash.nonempty {ι : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype ι] [Fintype Y] [DecidableEq Y] {k : ℕ} {h : ι → X → Y} (hh : IsKWiseIndependentHash k h) : Nonempty ι

A k-wise independent family has a seed.

theorem Cslib.Probability.IsKWiseIndependentHash.mono {ι : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype ι] [Fintype Y] [DecidableEq Y] {k : ℕ} {h : ι → X → Y} (hh : IsKWiseIndependentHash k h) {k' : ℕ} (hk : k' ≤ k) : IsKWiseIndependentHash k' h

A k-wise independent family is k'-wise independent for every k' ≤ k.

theorem Cslib.Probability.IsKWiseIndependentHash.expect_restrict {ι : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype ι] [Fintype Y] [DecidableEq Y] {k : ℕ} {h : ι → X → Y} {𝕜 : Type u_4} [Semifield 𝕜] [CharZero 𝕜] [DecidableEq X] (hh : IsKWiseIndependentHash k h) {T : Finset X} (hT : T.card ≤ k) (F : (↥T → Y) → 𝕜) : (Finset.univ.expect fun (i : ι) => F (T.restrict (h i))) = Finset.univ.expect fun (y : ↥T → Y) => F y

Restrictions are uniform: a function of the values of a k-wise independent family at a set T of at most k points has the same average as on a uniformly random y : T → Y.

theorem Cslib.Probability.IsKWiseIndependentHash.expect_prod {ι : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype ι] [Fintype Y] [DecidableEq Y] {k : ℕ} {h : ι → X → Y} {𝕜 : Type u_4} [Semifield 𝕜] [CharZero 𝕜] (hh : IsKWiseIndependentHash k h) {T : Finset X} (hT : T.card ≤ k) (f : X → Y → 𝕜) : (Finset.univ.expect fun (i : ι) => ∏ x ∈ T, f x (h i x)) = ∏ x ∈ T, Finset.univ.expect fun (y : Y) => f x y

Products of values average to products of averages: for a k-wise independent family and a set T of at most k points, the average of ∏ x ∈ T, f x (h i x) is ∏ x ∈ T, 𝔼 y, f x y.

theorem Cslib.Probability.IsKWiseIndependentHash.isPairwiseIndependentHash {ι : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype ι] [Fintype Y] [DecidableEq Y] {k : ℕ} {h : ι → X → Y} (hh : IsKWiseIndependentHash k h) (hk : 2 ≤ k) : IsPairwiseIndependentHash h

A k-wise independent family with k ≥ 2 is pairwise independent.

theorem Cslib.Probability.isKWiseIndependentHash_two_iff {ι : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype ι] [Fintype Y] [DecidableEq Y] {h : ι → X → Y} : IsKWiseIndependentHash 2 h ↔ IsPairwiseIndependentHash h ∧ Nonempty ι

Pairwise independence is 2-wise independence: a family is 2-wise independent exactly when it is pairwise independent and has a seed. So the pairwise independent families, such as Cslib.Probability.isPairwiseIndependentHash_affineHash, carry the k-wise API for k = 2.

theorem Cslib.Probability.IsKWiseIndependentHash.expect_sum_pow_le {ι : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype ι] [Fintype Y] [DecidableEq Y] {h : ι → X → Y} {m : ℕ} (hh : IsKWiseIndependentHash (2 * m) h) (S : Finset X) (Z : X → Y → ℝ) (hZ : ∀ x ∈ S, (Finset.univ.expect fun (y : Y) => Z x y) = 0) (hZ₁ : ∀ x ∈ S, ∀ (y : Y), |Z x y| ≤ 1) : (Finset.univ.expect fun (i : ι) => (∑ x ∈ S, Z x (h i x)) ^ (2 * m)) ≤ ↑m ^ (2 * m) * ↑S.card ^ m

The 2 m-th moment bound for limited independence: for a 2 m-wise independent family and scores Z x : Y → ℝ with average 0 and values in [-1, 1] at the points x of a finite set S, the 2 m-th moment of ∑ x ∈ S, Z x (h i x) is at most m ^ (2 m) * #S ^ m. Expanding the power, only tuples of points in which every point occurs at least twice contribute, and these tuples have at most m distinct entries.

theorem Cslib.Probability.IsKWiseIndependentHash.dens_filter_le_abs_sum {ι : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype ι] [Fintype Y] [DecidableEq Y] {h : ι → X → Y} {m : ℕ} (hh : IsKWiseIndependentHash (2 * m) h) (S : Finset X) (Z : X → Y → ℝ) (hZ : ∀ x ∈ S, (Finset.univ.expect fun (y : Y) => Z x y) = 0) (hZ₁ : ∀ x ∈ S, ∀ (y : Y), |Z x y| ≤ 1) {a : ℝ} (ha : 0 < a) : ↑{i : ι | a ≤ |∑ x ∈ S, Z x (h i x)|}.dens ≤ (↑m ^ 2 * ↑S.card / a ^ 2) ^ m

The tail bound for limited independence: for a 2 m-wise independent family and scores Z x : Y → ℝ with average 0 and values in [-1, 1] at the points of a finite set S, the sum ∑ x ∈ S, Z x (h i x) has absolute value at least a > 0 with probability at most (m² #S / a²) ^ m.

theorem Cslib.Probability.IsKWiseIndependentHash.dens_filter_le_abs_sum_sub_expect {ι : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype ι] [Fintype Y] [DecidableEq Y] {h : ι → X → Y} {m : ℕ} (hh : IsKWiseIndependentHash (2 * m) h) (S : Finset X) (g : X → Y → ℝ) (hg : ∀ x ∈ S, ∀ (y : Y), g x y ∈ Set.Icc 0 1) {a : ℝ} (ha : 0 < a) : ↑{i : ι | a ≤ |∑ x ∈ S, (g x (h i x) - Finset.univ.expect fun (y : Y) => g x y)|}.dens ≤ (↑m ^ 2 * ↑S.card / a ^ 2) ^ m

The tail bound for limited independence, for scores in [0, 1]: for a 2 m-wise independent family and scores g x : Y → [0, 1], the sum ∑ x ∈ S, g x (h i x) deviates from its mean ∑ x ∈ S, 𝔼 y, g x y by at least a > 0 with probability at most (m² #S / a²) ^ m.

theorem Cslib.Probability.isKWiseIndependentHash_of_surjective {ι : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype ι] [Fintype Y] [DecidableEq Y] {k : ℕ} [AddGroup ι] [AddGroup Y] (g : ι →+ X → Y) (hg : ∀ (T : Finset X), T.card ≤ k → Function.Surjective fun (i : ι) => T.restrict (g i)) : IsKWiseIndependentHash k fun (i : ι) => g i

The surjectivity criterion: let the seeds ι form a finite additive group and let the functions g i : X → Y into a finite additive group depend additively on i. If for every set T of at most k points the restrictions of the g i to T take every value in T → Y, then the family is k-wise independent.