4. Streaming and Sketching
A frequency sketch processes updates while keeping a table of counters. A query estimates how much weight an item has received. Count-Min provides a useful first example: its estimate is always at least the true frequency, and independently sampled hash rows bound the probability of a large overestimate.
This chapter uses weighted insertions. An event (x, c) adds the natural number c to item x;
the stream is a List (X × ℕ). The list describes the input to the correctness theorem. The
stored table contains only counters, and Cslib.DataStructure.CountMin.update can process
one new event from the current table.
import CslibFrontier.DataStructure.CountMin.LinearHash import CslibFrontier.DataStructure.CountMin.Program open Cslib.DataStructure.CountMin