Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Expander Graphs by Emin Karayel


view this post on Zulip Email Gateway (Mar 17 2023 at 10:04):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,

I’d like to announce a new AFP entry

Expander Graphs
by Emin Karayel

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.

https://www.isa-afp.org/entries/Expander_Graphs.html

Enjoy,
René


Last updated: Apr 28 2024 at 20:16 UTC