Count-Min sketches for weighted insertion streams

An update (x, c) adds the natural-number weight c to one bucket in each hash row. The counter table is a vector of vectors, so updates materialize a finite table instead of retaining a chain of functional updates. A point query takes the minimum of the counters addressed by the queried item. It never underestimates the true frequency.

The exact bucket invariant identifies this executable update-and-fold algorithm with sums of stream weights. Tables built with the same hashes merge by entrywise addition. Every counter is bounded by the total inserted weight. These are semantic and numerical guarantees; this module does not assign machine running times to Lean operations or certify their heap consumption.

Main definitions

• Cslib.CountMin.frequency, Cslib.CountMin.mass: weighted frequency and total stream mass.
• Cslib.CountMin.bucket, Cslib.CountMin.noise: exact bucket and collision sums.
• Cslib.CountMin.Table, Cslib.CountMin.update, Cslib.CountMin.run: stored counters and the executable streaming algorithm.
• Cslib.CountMin.estimate: the minimum of a nonempty collection of hash rows.
• Cslib.CountMin.merge: entrywise addition of tables using the same hashes.

Main results

• Cslib.CountMin.bucket_hash_eq_frequency_add_noise: a queried counter is frequency plus noise.
• Cslib.CountMin.run_get: every stored counter equals its bucket sum.
• Cslib.CountMin.frequency_le_estimate_run: no underestimation.
• Cslib.CountMin.run_get_le_mass: each counter is at most the total stream weight.
• Cslib.CountMin.run_append: concatenation of streams agrees with merging their tables.

References

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

def Cslib.CountMin.mass {X : Type u_1} (s : List (X × ℕ)) : ℕ

Total weight inserted by a stream.

def Cslib.CountMin.frequency {X : Type u_1} [DecidableEq X] (s : List (X × ℕ)) (x : X) : ℕ

Total weight inserted at the queried item.

def Cslib.CountMin.bucket {X : Type u_1} {w : ℕ} (h : X → Fin w) (s : List (X × ℕ)) (b : Fin w) : ℕ

The weight in one bucket of a hash row.

def Cslib.CountMin.noise {X : Type u_1} {w : ℕ} [DecidableEq X] (h : X → Fin w) (s : List (X × ℕ)) (x : X) : ℕ

Weight contributed by other items colliding with the query in one hash row.

@[simp]

theorem Cslib.CountMin.mass_nil {X : Type u_1} : mass [] = 0

@[simp]

theorem Cslib.CountMin.mass_cons {X : Type u_1} (u : X × ℕ) (s : List (X × ℕ)) : mass (u :: s) = u.2 + mass s

@[simp]

theorem Cslib.CountMin.frequency_nil {X : Type u_1} [DecidableEq X] (x : X) : frequency [] x = 0

@[simp]

theorem Cslib.CountMin.frequency_cons {X : Type u_1} [DecidableEq X] (u : X × ℕ) (s : List (X × ℕ)) (x : X) : frequency (u :: s) x = (if u.1 = x then u.2 else 0) + frequency s x

@[simp]

theorem Cslib.CountMin.bucket_nil {X : Type u_1} {w : ℕ} (h : X → Fin w) (b : Fin w) : bucket h [] b = 0

@[simp]

theorem Cslib.CountMin.bucket_cons {X : Type u_1} {w : ℕ} (h : X → Fin w) (u : X × ℕ) (s : List (X × ℕ)) (b : Fin w) : bucket h (u :: s) b = (if h u.1 = b then u.2 else 0) + bucket h s b

@[simp]

theorem Cslib.CountMin.noise_nil {X : Type u_1} {w : ℕ} [DecidableEq X] (h : X → Fin w) (x : X) : noise h [] x = 0

@[simp]

theorem Cslib.CountMin.noise_cons {X : Type u_1} {w : ℕ} [DecidableEq X] (h : X → Fin w) (u : X × ℕ) (s : List (X × ℕ)) (x : X) : noise h (u :: s) x = (if u.1 ≠ x ∧ h u.1 = h x then u.2 else 0) + noise h s x

@[simp]

theorem Cslib.CountMin.mass_append {X : Type u_1} (s t : List (X × ℕ)) : mass (s ++ t) = mass s + mass t

@[simp]

theorem Cslib.CountMin.frequency_append {X : Type u_1} [DecidableEq X] (s t : List (X × ℕ)) (x : X) : frequency (s ++ t) x = frequency s x + frequency t x

@[simp]

theorem Cslib.CountMin.bucket_append {X : Type u_1} {w : ℕ} (h : X → Fin w) (s t : List (X × ℕ)) (b : Fin w) : bucket h (s ++ t) b = bucket h s b + bucket h t b

@[simp]

theorem Cslib.CountMin.noise_append {X : Type u_1} {w : ℕ} [DecidableEq X] (h : X → Fin w) (s t : List (X × ℕ)) (x : X) : noise h (s ++ t) x = noise h s x + noise h t x

theorem Cslib.CountMin.bucket_hash_eq_frequency_add_noise {X : Type u_1} {w : ℕ} [DecidableEq X] (h : X → Fin w) (s : List (X × ℕ)) (x : X) : bucket h s (h x) = frequency s x + noise h s x

A queried bucket consists of the query's frequency and nonnegative collision noise.

theorem Cslib.CountMin.frequency_le_mass {X : Type u_1} [DecidableEq X] (s : List (X × ℕ)) (x : X) : frequency s x ≤ mass s

A frequency cannot exceed the total inserted weight.

theorem Cslib.CountMin.bucket_le_mass {X : Type u_1} {w : ℕ} (h : X → Fin w) (s : List (X × ℕ)) (b : Fin w) : bucket h s b ≤ mass s

Every bucket is bounded by the total inserted weight.

theorem Cslib.CountMin.noise_le_mass {X : Type u_1} {w : ℕ} [DecidableEq X] (h : X → Fin w) (s : List (X × ℕ)) (x : X) : noise h s x ≤ mass s

Collision noise is bounded by the total inserted weight.

@[reducible, inline]

abbrev Cslib.CountMin.Table (d w : ℕ) : Type

A stored array of d rows of w natural-number counters.

def Cslib.CountMin.zero (d w : ℕ) : Table d w

The initial table has every counter zero.

def Cslib.CountMin.get {d w : ℕ} (t : Table d w) (r : Fin d) (b : Fin w) : ℕ

Read one stored counter.

def Cslib.CountMin.update {X : Type u_1} {d w : ℕ} (h : Fin d → X → Fin w) (t : Table d w) (u : X × ℕ) : Table d w

Add the update weight to the addressed counter in every row.

def Cslib.CountMin.run {X : Type u_1} {d w : ℕ} (h : Fin d → X → Fin w) (s : List (X × ℕ)) : Table d w

Process the stream in order, keeping only the current counter table.

def Cslib.CountMin.merge {d w : ℕ} (a b : Table d w) : Table d w

Merge tables formed with the same hash bank by adding corresponding counters.

def Cslib.CountMin.estimate {X : Type u_1} {d w : ℕ} [NeZero d] (h : Fin d → X → Fin w) (t : Table d w) (x : X) : ℕ

Take the minimum of the counters addressed by a query, using at least one row.

@[simp]

theorem Cslib.CountMin.get_zero {d w : ℕ} (r : Fin d) (b : Fin w) : get (zero d w) r b = 0

@[simp]

theorem Cslib.CountMin.get_merge {d w : ℕ} (a c : Table d w) (r : Fin d) (b : Fin w) : get (merge a c) r b = get a r b + get c r b

theorem Cslib.CountMin.get_update {X : Type u_1} {d w : ℕ} (h : Fin d → X → Fin w) (t : Table d w) (u : X × ℕ) (r : Fin d) (b : Fin w) : get (update h t u) r b = get t r b + if h r u.1 = b then u.2 else 0

An update changes just its addressed bucket in each row.

theorem Cslib.CountMin.foldl_update_get {X : Type u_1} {d w : ℕ} (h : Fin d → X → Fin w) (s : List (X × ℕ)) (t : Table d w) (r : Fin d) (b : Fin w) : get (List.foldl (update h) t s) r b = get t r b + bucket (h r) s b

An arbitrary starting table gains exactly the stream's bucket weights.

theorem Cslib.CountMin.run_get {X : Type u_1} {d w : ℕ} (h : Fin d → X → Fin w) (s : List (X × ℕ)) (r : Fin d) (b : Fin w) : get (run h s) r b = bucket (h r) s b

Every stored counter equals its exact weighted bucket sum.

theorem Cslib.CountMin.run_get_le_mass {X : Type u_1} {d w : ℕ} (h : Fin d → X → Fin w) (s : List (X × ℕ)) (r : Fin d) (b : Fin w) : get (run h s) r b ≤ mass s

Stored counters never exceed the total stream weight.

theorem Cslib.CountMin.estimate_le_get {X : Type u_1} {d w : ℕ} [NeZero d] (h : Fin d → X → Fin w) (t : Table d w) (x : X) (r : Fin d) : estimate h t x ≤ get t r (h r x)

A query is no larger than any of its addressed row counters.

theorem Cslib.CountMin.estimate_run_le_bucket {X : Type u_1} {d w : ℕ} [NeZero d] (h : Fin d → X → Fin w) (s : List (X × ℕ)) (x : X) (r : Fin d) : estimate h (run h s) x ≤ bucket (h r) s (h r x)

A query on a processed stream is bounded by the exact bucket sum in every row.

theorem Cslib.CountMin.frequency_le_estimate_run {X : Type u_1} {d w : ℕ} [DecidableEq X] [NeZero d] (h : Fin d → X → Fin w) (s : List (X × ℕ)) (x : X) : frequency s x ≤ estimate h (run h s) x

A Count-Min point query never underestimates the inserted frequency.

theorem Cslib.CountMin.run_append {X : Type u_1} {d w : ℕ} (h : Fin d → X → Fin w) (s t : List (X × ℕ)) : run h (s ++ t) = merge (run h s) (run h t)

Concatenating streams agrees exactly with merging tables using the same hash bank.

theorem Cslib.CountMin.run_append_singleton {X : Type u_1} {d w : ℕ} (h : Fin d → X → Fin w) (s : List (X × ℕ)) (u : X × ℕ) : run h (s ++ [u]) = update h (run h s) u

Appending one update performs one update on the current table.