# Theory Expander_Graphs_MGG

section ‹Margulis Gabber Galil Construction\label{sec:margulis}›
text ‹This section formalizes the Margulis-Gabber-Galil expander graph, which is defined on the
product space $\mathbb Z_n \times \mathbb Z_n$. The construction is an adaptation of graph
introduced by Margulis~\cite{margulis1973}, for which he gave a non-constructive proof of its
spectral gap. Later Gabber and Galil~\cite{gabber1981} adapted the graph and derived an explicit
spectral gap, i.e., that the second largest eigenvalue is bounded by $\frac{5}{8} \sqrt{2}$. The
proof was later improved by Jimbo and Marouka~\cite{jimbo1987} using Fourier Analysis.
Hoory et al.~\cite[\S 8]{hoory2006} present a slight simplification of that proof (due to Boppala)
which this formalization is based on.›
theory Expander_Graphs_MGG
imports
"HOL-Analysis.Complex_Transcendental"
"HOL-Decision_Procs.Approximation"
Expander_Graphs_Definition
begin