Documentation

Complexity.Probability.KWiseIndependent.Polynomial

The polynomial k-wise independent hash family #

For a finite field F, the polynomials of degree less than k, evaluated as maps F → F and indexed by their coefficient vectors c : Fin k → F (Cslib.Probability.polynomialHash), form a k-wise independent hash family (Cslib.Probability.isKWiseIndependentHash_polynomialHash) Vadhan, Section 3.5.5: by Lagrange interpolation, every assignment of values to at most k points is attained by a polynomial of degree less than k, and evaluation depends additively on the coefficients, so the surjectivity criterion Cslib.Probability.isKWiseIndependentHash_of_surjective applies. The seed consists of k field elements. For k = 2 these are the affine maps x ↦ c₀ + c₁ x of Cslib.Probability.isPairwiseIndependentHash_affineHash in dimension one.

Main definitions #

Main results #

References #

source
def Cslib.Probability.polynomialHash {F : Type u_1} [Semiring F] {k : ℕ} (c : Fin k → F) (x : F) :
F

The polynomial hash with coefficient vector c : Fin k → F: the value at x of the polynomial ∑ j < k, c j X ^ j, of degree less than k.

Instances For
    source
    theorem Cslib.Probability.polynomialHash_add {F : Type u_1} [Semiring F] {k : ℕ} (c d : Fin k → F) :
    polynomialHash (c + d) = polynomialHash c + polynomialHash d

    The polynomial hash is additive in its coefficient vector.

    source
    theorem Cslib.Probability.polynomialHash_eq_eval {F : Type u_1} [Semiring F] {k : ℕ} (P : Polynomial F) (hP : P.natDegree < k) (x : F) :
    polynomialHash (fun (j : Fin k) => P.coeff ↑j) x = Polynomial.eval x P

    The polynomial hash with coefficients c evaluates any polynomial of degree less than k whose coefficients are c.

    source
    theorem Cslib.Probability.isKWiseIndependentHash_polynomialHash {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (k : ℕ) :
    IsKWiseIndependentHash k polynomialHash

    The polynomial hash family is k-wise independent Vadhan, Section 3.5.5: over a finite field F, the polynomials of degree less than k with uniformly random coefficients take independent uniform values at any k distinct points.