
Formalization
of
Randomized
Approximation
Algorithms
for
Frequency
Moments
Title: 
Formalization of Randomized Approximation Algorithms for Frequency Moments 
Author:

Emin Karayel

Submission date: 
20220408 
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 higherorder frequency moments that
provide information about the skew of the data stream. (The
kth frequency moment of a data stream is the sum
of the kth powers of the occurrence counts of each
element in the stream.) This entry formalizes three randomized
algorithms for the approximation of
F_{0},
F_{2} and
F_{k} for k ≥
3 based on [1,
2]
and verifies their expected accuracy, success probability and space
usage. 
BibTeX: 
@article{Frequency_MomentsAFP,
author = {Emin Karayel},
title = {Formalization of Randomized Approximation Algorithms for Frequency Moments},
journal = {Archive of Formal Proofs},
month = apr,
year = 2022,
note = {\url{https://isaafp.org/entries/Frequency_Moments.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Depends on: 
Bertrands_Postulate, Equivalence_Relation_Enumeration, Interpolation_Polynomials_HOL_Algebra, Lp, Median_Method, Prefix_Free_Code_Combinators, Universal_Hash_Families 
