### Abstract

This entry formalizes a randomized cardinality estimation data structure with asymptotically optimal space usage. It is inspired by the streaming algorithm presented by Błasiok in 2018. His work closed the gap between the best-known lower bound and upper bound after a long line of research started by Flajolet and Martin in 1984 and was to first to apply expander graphs (in addition to hash families) to the problem. The formalized algorithm has two improvements compared to the algorithm by Błasiok. It supports operation in parallel mode, and it relies on a simpler pseudo-random construction avoiding the use of code based extractors.

### License

BSD License

### Topics

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

### Session Distributed_Distinct_Elements

- Distributed_Distinct_Elements_Preliminary
- Pseudorandom_Combinators
- Distributed_Distinct_Elements_Balls_and_Bins
- Distributed_Distinct_Elements_Tail_Bounds
- Distributed_Distinct_Elements_Inner_Algorithm
- Distributed_Distinct_Elements_Accuracy_Without_Cutoff
- Distributed_Distinct_Elements_Cutoff_Level
- Distributed_Distinct_Elements_Accuracy
- Distributed_Distinct_Elements_Outer_Algorithm

### Depends on

- Discrete Summation
- Expander Graphs
- Stirling’s formula

### Used by

- Derandomization with Conditional Expectations

## Cite

×

Distributed_Distinct_Elements-AFP

    @article{Distributed_Distinct_Elements-AFP,
      author  = {Emin Karayel},
      title   = {Distributed Distinct Elements},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/Distributed_Distinct_Elements.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Apr 6, 2023 : Isabelle2022