Documentation

UniversalHashing.Matrix

Proof that Binary Matrix-vector multiplication (using all matrices) is a Universal-2 hash function: matrix_mulVec_isUniversal2

(This family is very big and therefore not useful in practice)

source
def mulVecMat {๐•œ : Type u_1} [Field ๐•œ] {n : Type u_3} [Fintype n] (m : Type u_4) [Fintype m] [DecidableEq m] (v : n โ†’ ๐•œ) :
Matrix m n ๐•œ โ†’โ‚—[๐•œ] m โ†’ ๐•œ

Given a vector v, the linear map mapping a matrix M to M *แตฅ v.

Equations
Instances For
    source
    theorem mulVecMat_surjective {๐•œ : Type u_1} [Field ๐•œ] {n : Type u_3} [Fintype n] (m : Type u_4) [Fintype m] [DecidableEq m] {v : n โ†’ ๐•œ} (vne0 : v โ‰  0) :
    Function.Surjective โ‡‘(mulVecMat m v)
    source
    theorem finrank_ker_mulVecLin {๐•œ : Type u_1} [Field ๐•œ] {n : Type u_3} [Fintype n] (m : Type u_4) [Fintype m] [DecidableEq m] {v : n โ†’ ๐•œ} (hv : v โ‰  0) :
    Fintype.card m + Module.finrank ๐•œ โ†ฅ(mulVecMat m v).ker = Fintype.card m * Fintype.card n

    finrank of the kernel of M โ†ฆ M.mulVec v for nonzero v.

    source
    theorem card_eq_two_pow_finrank (p : โ„•) [Fact (Nat.Prime p)] (V : Type u_1) [AddCommGroup V] [Module (ZMod p) V] [FiniteDimensional (ZMod p) V] [Fintype V] :
    Fintype.card V = p ^ Module.finrank (ZMod p) V
    source
    theorem h_card_matrices (p : โ„•) [Fact (Nat.Prime p)] (m n : โ„•) :
    Fintype.card (Matrix (Fin m) (Fin n) (ZMod p)) = p ^ (m * n)

    There are 2 ^ (m * n) binary mxn matrices.

    source
    theorem finrank_matrix (p : โ„•) [Fact (Nat.Prime p)] (m n : โ„•) :
    Module.finrank (ZMod p) (Matrix (Fin m) (Fin n) (ZMod p)) = m * n
    source
    theorem card_in_range_eq_card_ker (p : โ„•) [Fact (Nat.Prime p)] (m n : โ„•) (v : Fin n โ†’ ZMod p) (w : Fin m โ†’ ZMod p) :
    (w โˆˆ Set.range fun (M : Matrix (Fin m) (Fin n) (ZMod p)) => M.mulVec v) โ†’ Fintype.card โ†‘{M : Matrix (Fin m) (Fin n) (ZMod p) | M.mulVec v = w} = Fintype.card โ†‘{M : Matrix (Fin m) (Fin n) (ZMod p) | M.mulVec v = 0}
    source
    theorem mulVecMat_ZModp_card_ker {p : โ„•} [Fact (Nat.Prime p)] (m : โ„•) {n : โ„•} (v : Fin n โ†’ ZMod p) :
    Fintype.card โ†‘{M : Matrix (Fin m) (Fin n) (ZMod p) | M.mulVec v = 0} * Fintype.card โ†‘(Set.range fun (M : Matrix (Fin m) (Fin n) (ZMod p)) => M.mulVec v) = p ^ (m * n)
    source
    theorem card_ker_pow_dim {p : โ„•} [Fact (Nat.Prime p)] (a : โ„•) {b : โ„•} {v : Fin b โ†’ ZMod p} (hv : v โ‰  0) :
    Fintype.card โ†‘{M : Matrix (Fin a) (Fin b) (ZMod p) | M.mulVec v = 0} = p ^ (a * (b - 1))
    source
    def matHash (q m n : โ„•) :
    HashFamily (Matrix (Fin m) (Fin n) (ZMod q)) (Fin n โ†’ ZMod q) (Fin m โ†’ ZMod q)

    Hash by matrix-times-vector modulo q

    Equations
    Instances For
      source
      theorem matHash_universal2atHash_universal2 (p : โ„•) [Fact (Nat.Prime p)] (a b : โ„•) :
      (matHash p a b).universal2

      Matrix-vector multiplication (using all matrices modulo p) is Universal2.

      source
      theorem matHash_not_strongly_universal_n (a b : โ„•) (ha : a > 0) (hb : b > 0) :
      ยฌHashFamily.stronglyUniversal_n 2 (matHash 2 a b)

      Counterexample: Binary Matrix-vector multiplication (using binary matrices) is not strongly-Universal-2.