### 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.

### License

BSD License

### Topics

- Computer science/Algorithms/Approximation
- Computer science/Algorithms/Randomized

### Related publications

- Karayel, E. (2022). Formalization of Randomized Approximation Algorithms for Frequency Moments. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.ITP.2022.21

### Session Frequency_Moments

- Frequency_Moments_Preliminary_Results
- Frequency_Moments
- K_Smallest
- Landau_Ext
- Probability_Ext
- Product_PMF_Ext
- Frequency_Moment_0
- Frequency_Moment_2
- Frequency_Moment_k

### Depends on

- Bertrand’s postulate
- Enumeration of Equivalence Relations
- Interpolation Polynomials (in HOL-Algebra)
- Lp spaces
- Median Method
- A Combinator Library for Prefix-Free Codes
- Universal Hash Families

### Used by

- Approximate Model Counting
- Expander Graphs

## Cite

×

Frequency_Moments-AFP

    @article{Frequency_Moments-AFP,
      author  = {Emin Karayel},
      title   = {Formalization of Randomized Approximation Algorithms for Frequency Moments},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Frequency_Moments.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Apr 19, 2022 : Isabelle2021-1