### Abstract

Expander Graphs are low-degree graphs that are highly connected. They have diverse applications, for example in derandomization and pseudo-randomness, error-correcting codes, as well as pure mathematical subjects such as metric embeddings. This entry formalizes the concept and derives main theorems about them such as Cheeger's inequality or tail bounds on distribution of random walks on them. It includes a strongly explicit construction for every size and spectral gap. The latter is based on the Margulis-Gabber-Galil graphs and several graph operations that preserve spectral properties. The proofs are based on the survey papers/monographs by Hoory et al. and Vadhan, as well as results from Impagliazzo and Kabanets and Murtagh et al.

### License

BSD License

### Topics

- Computer science/Algorithms/Graph
- Computer science/Algorithms/Randomized
- Mathematics/Graph theory

### Session Expander_Graphs

- Constructive_Chernoff_Bound
- Extra_Congruence_Method
- Expander_Graphs_Multiset_Extras
- Expander_Graphs_Definition
- Expander_Graphs_TTS
- Expander_Graphs_Algebra
- Expander_Graphs_Eigenvalues
- Expander_Graphs_Cheeger_Inequality
- Expander_Graphs_MGG
- Expander_Graphs_Walks
- Expander_Graphs_Power_Construction
- Expander_Graphs_Strongly_Explicit

### Depends on

- Simultaneous diagonalization of pairwise commuting Hermitian matrices
- Formalization of Randomized Approximation Algorithms for Frequency Moments
- Graph Theory
- Perron-Frobenius Theorem for Spectral Radius Analysis
- Pólya’s Proof of the Weighted Arithmetic–Geometric Mean Inequality

### Used by

- Karatsuba Multiplication on Integers
- Distributed Distinct Elements

## Cite

×

Expander_Graphs-AFP

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

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Mar 16, 2023 : Isabelle2022