ε-Almost Universal Hashing

This file proves things about

• ε-almost-universal₂ (ε-AU₂), see HashFamily.almostUniversal2
• ε-almost-strongly-universal₂ (ε-ASU₂), see HashFamily.almostStronglyUniversal2
• uniformity, see HashFamily.uniform

These are relaxations of HashFamily.universal2 and HashFamily.stronglyUniversal2 where equality/bounds are replaced by ε. The definitions are in UniversalHashing.Basic.

Main results

• HashFamily.universal2_iff_probUniform (in Basic): universal2 ↔ almostUniversal2 (1 / |Output|).
• HashFamily.almostUniversal2_mono: ε-AU₂ is monotone in ε.
• HashFamily.almostStronglyUniversal2_mono: ε-ASU₂ is monotone in ε.
• HashFamily.almostUniversal2_of_almostStronglyUniversal2: almostStronglyUniversal2 ε implies almostUniversal2 ε.
• HashFamily.stronglyUniversal2_iff_almostStronglyUniversal2: stronglyUniversal2 ↔ almostStronglyUniversal2 (1 / |Output|).
• HashFamily.almostStronglyUniversal2_of_stronglyUniversal2: stronglyUniversal2 implies almostStronglyUniversal2 (1 / |Output|).
• HashFamily.uniform_of_stronglyUniversal2: stronglyUniversal2 implies uniform.
• HashFamily.almostStronglyUniversal2_eps_lower_bound: almostStronglyUniversal2 ε implies 1 / |Output| ≤ ε.

References

• [BKST15]: "On an almost-universal hash function family with applications to authentication and secrecy codes" by Khodakhast Bibak, Bruce M. Kapron, Venkatesh Srinivasan and László Tóth.
• [Sti94]: "Universal hashing and authentication codes" by Stinson, D. R.

theorem HashFamily.almostUniversal2_mono {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [DecidableEq Output] {ε₁ ε₂ : ℚ} (hε : ε₁ ≤ ε₂) (H : HashFamily Seed Input Output) (h : almostUniversal2 ε₁ H) : almostUniversal2 ε₂ H

theorem HashFamily.almostStronglyUniversal2_mono {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] {ε₁ ε₂ : ℚ} (hε : ε₁ ≤ ε₂) (H : HashFamily Seed Input Output) (h : almostStronglyUniversal2 ε₁ H) : almostStronglyUniversal2 ε₂ H

theorem HashFamily.almostUniversal2_of_almostStronglyUniversal2 {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] [Nonempty Seed] {ε : ℚ} (H : HashFamily Seed Input Output) (h : almostStronglyUniversal2 ε H) : almostUniversal2 ε H

theorem HashFamily.almostStronglyUniversal2_of_stronglyUniversal2 {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] [Nonempty Seed] (H : HashFamily Seed Input Output) (hsu : H.stronglyUniversal2) : almostStronglyUniversal2 (1 / ↑(Fintype.card Output)) H

theorem HashFamily.stronglyUniversal2_iff_almostStronglyUniversal2 {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] [Nonempty Seed] (H : HashFamily Seed Input Output) : H.stronglyUniversal2 ↔ almostStronglyUniversal2 (1 / ↑(Fintype.card Output)) H

stronglyUniversal2 is equivalent to almostStronglyUniversal2 (1 / |Output|). Since 1 / |Output| is the minimum possible ε for any ε-ASU₂ family (see almostStronglyUniversal2_eps_lower_bound), this characterizes strongly universal families as exactly those achieving the tightest possible near-independence bound.

theorem HashFamily.uniform_of_stronglyUniversal2 {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] [Nonempty Seed] [Nontrivial Input] (H : HashFamily Seed Input Output) (hsu : H.stronglyUniversal2) : H.uniform

theorem HashFamily.almostStronglyUniversal2_eps_lower_bound {Seed : Type u_1} {Input : Type u_2} {Output : Type u_3} [Fintype Seed] [Fintype Output] [DecidableEq Output] [Nonempty Seed] [Nontrivial Input] {ε : ℚ} (H : HashFamily Seed Input Output) (h : almostStronglyUniversal2 ε H) : 1 / ↑(Fintype.card Output) ≤ ε