### Abstract

In 1999 Alon et. al. introduced the still active research topic of
approximating the frequency moments of a data stream using randomized
algorithms with minimal space usage. This includes the problem of
estimating the cardinality of the stream elements - the zeroth
frequency moment. But, also higher-order frequency moments that
provide information about the skew of the data stream. (The

BSD License*k*-th frequency moment of a data stream is the sum of the*k*-th powers of the occurrence counts of each element in the stream.) This entry formalizes three randomized algorithms for the approximation of*F*,_{0}*F*and_{2}*F*for_{k}*k ≥ 3*based on [1, 2] and verifies their expected accuracy, success probability and space usage.### Depends On

- Bertrands_Postulate
- Equivalence_Relation_Enumeration
- Interpolation_Polynomials_HOL_Algebra
- Lp
- Prefix_Free_Code_Combinators
- Median_Method
- Universal_Hash_Families