Count-Min fixed-query accuracy

For a fixed insertion-only weighted stream and a fixed queried item, independently sampled universal-hash rows give Count-Min its one-sided additive-error guarantee [CM05], Section 4.1, Theorem 1. The stream and query are fixed before the hash seeds are sampled. This theorem makes no claim about adaptively selected queries or updates.

The collision noise in one row has mean at most total stream mass divided by the bucket count. Markov's inequality bounds one bad row; independent uniform row seeds raise its failure bound to the number of rows. In particular, 2 ≤ w * ε gives failure at most 2⁻ᵈ.

Main results

• Cslib.CountMin.expect_noise_le: expected single-row collision noise.
• Cslib.CountMin.dens_noise_gt_le: single-row tail bound.
• Cslib.CountMin.dens_estimate_gt_le: independent-row amplification at an absolute threshold.
• Cslib.CountMin.dens_estimate_error_le: relative additive error for a fixed query.
• Cslib.CountMin.dens_estimate_error_le_inv_two_pow: the base-two parameter guarantee.

References

• G. Cormode, S. Muthukrishnan, An Improved Data Stream Summary: The Count-Min Sketch and its Applications, Section 4.1, Theorem 1.

theorem Cslib.CountMin.expect_noise_le {X : Type u_1} {Seed : Type u_2} [DecidableEq X] [Fintype Seed] [Nonempty Seed] {w : ℕ} (hash : Seed → X → Fin w) (hh : Probability.IsTwoUniversal (Probability.PMF.uniformOfFintype Seed) hash) (s : List (X × ℕ)) (x : X) : (Finset.univ.expect fun (seed : Seed) => ↑(noise (hash seed) s x)) ≤ ↑(mass s) / ↑w

The expected collision noise of one universal-hash row is at most total mass divided by the number of buckets. No finiteness assumption on the item universe is needed.

theorem Cslib.CountMin.dens_noise_gt_le {X : Type u_1} {Seed : Type u_2} [DecidableEq X] [Fintype Seed] [Nonempty Seed] {w : ℕ} (hash : Seed → X → Fin w) (hh : Probability.IsTwoUniversal (Probability.PMF.uniformOfFintype Seed) hash) (s : List (X × ℕ)) (x : X) {t : ℝ} (ht : 0 < t) : ↑{seed : Seed | t < ↑(noise (hash seed) s x)}.dens ≤ ↑(mass s) / (↑w * t)

Markov's inequality bounds the fraction of seeds whose collision noise exceeds t.

theorem Cslib.CountMin.dens_estimate_gt_le {X : Type u_1} {Seed : Type u_2} [DecidableEq X] [Fintype Seed] [Nonempty Seed] {d w : ℕ} [NeZero d] (hash : Seed → X → Fin w) (hh : Probability.IsTwoUniversal (Probability.PMF.uniformOfFintype Seed) hash) (s : List (X × ℕ)) (x : X) {t : ℝ} (ht : 0 < t) : ↑{seeds : Fin d → Seed | ↑(frequency s x) + t < ↑(estimate (fun (r : Fin d) => hash (seeds r)) (run (fun (r : Fin d) => hash (seeds r)) s) x)}.dens ≤ (↑(mass s) / (↑w * t)) ^ d

Count-Min can exceed a fixed absolute additive threshold only when every independent row exceeds that threshold.

theorem Cslib.CountMin.dens_estimate_error_le {X : Type u_1} {Seed : Type u_2} [DecidableEq X] [Fintype Seed] [Nonempty Seed] {d w : ℕ} [NeZero d] [NeZero w] (hash : Seed → X → Fin w) (hh : Probability.IsTwoUniversal (Probability.PMF.uniformOfFintype Seed) hash) (s : List (X × ℕ)) (x : X) {ε : ℝ} (hε : 0 < ε) : ↑{seeds : Fin d → Seed | ↑(frequency s x) + ε * ↑(mass s) < ↑(estimate (fun (r : Fin d) => hash (seeds r)) (run (fun (r : Fin d) => hash (seeds r)) s) x)}.dens ≤ (↑w * ε)⁻¹ ^ d

A fixed Count-Min query has additive error at most ε * mass s except on a fraction (w * ε)⁻ᵈ of the independently sampled uniform hash banks.

theorem Cslib.CountMin.dens_estimate_error_le_inv_two_pow {X : Type u_1} {Seed : Type u_2} [DecidableEq X] [Fintype Seed] [Nonempty Seed] {d w : ℕ} [NeZero d] [NeZero w] (hash : Seed → X → Fin w) (hh : Probability.IsTwoUniversal (Probability.PMF.uniformOfFintype Seed) hash) (s : List (X × ℕ)) (x : X) {ε : ℝ} (hε : 0 < ε) (hw : 2 ≤ ↑w * ε) : ↑{seeds : Fin d → Seed | ↑(frequency s x) + ε * ↑(mass s) < ↑(estimate (fun (r : Fin d) => hash (seeds r)) (run (fun (r : Fin d) => hash (seeds r)) s) x)}.dens ≤ (2 ^ d)⁻¹

With at least 2 / ε buckets, each additional independent row halves the failure bound.