Formalization of Randomized Approximation Algorithms for Frequency Moments

 Title: Formalization of Randomized Approximation Algorithms for Frequency Moments Author: Emin Karayel Submission date: 2022-04-08 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 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 F0, F2 and Fk for k ≥ 3 based on [1, 2] and verifies their expected accuracy, success probability and space usage. BibTeX: @article{Frequency_Moments-AFP, author = {Emin Karayel}, title = {Formalization of Randomized Approximation Algorithms for Frequency Moments}, journal = {Archive of Formal Proofs}, month = apr, year = 2022, note = {\url{https://isa-afp.org/entries/Frequency_Moments.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Bertrands_Postulate, Equivalence_Relation_Enumeration, Interpolation_Polynomials_HOL_Algebra, Lp, Median_Method, Prefix_Free_Code_Combinators, Universal_Hash_Families Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.