@[reducible, inline]

abbrev SelbergSpectralGap.SL2p (p : ℕ) [Fact (Nat.Prime p)] : Type

The group $\mathrm{SL}_2(\mathbb{F}_p)$ of $2 \times 2$ matrices with determinant $1$ over the finite field $\mathbb{Z}/p\mathbb{Z}$.

noncomputable def SelbergSpectralGap.selbergGeneratingSet (p : ℕ) [Fact (Nat.Prime p)] : Finset (SL2p p)

The Selberg generating set $A_{\operatorname{sel}} \subset \mathrm{SL}_2(\mathbb{F}_p)$, consisting of the four unipotent matrices $\begin{pmatrix} 1 & \pm 1 \\ 0 & 1 \end{pmatrix}$ and $\begin{pmatrix} 1 & 0 \\ \pm 1 & 1 \end{pmatrix}$.

noncomputable def SelbergSpectralGap.averagingOperator {G : Type u_1} [Group G] [Fintype G] (A : Finset G) : (G → ℝ) → G → ℝ

The averaging operator $T_A$ associated with a finite subset $A \subseteq G$ of a finite group: $(T_A f)(x) = \frac{1}{|A|} \sum_{a \in A} f(x \cdot a)$.

noncomputable def SelbergSpectralGap.l2Norm {G : Type u_1} [Fintype G] (f : G → ℝ) : ℝ

The $\ell^2$ norm of a function $f : G \to \mathbb{R}$ on a finite group $G$, defined as $\|f\|_{\ell^2} = \sqrt{\sum_{g \in G} f(g)^2}$.

def SelbergSpectralGap.HasMeanZero {G : Type u_1} [Fintype G] (f : G → ℝ) : Prop

A function $f : G \to \mathbb{R}$ on a finite group has mean zero if $\sum_{g \in G} f(g) = 0$, i.e. it is orthogonal to the constant function.

theorem selberg_spectral_gap : ∃ (c : ℝ), 0 < c ∧ ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (f : SelbergSpectralGap.SL2p p → ℝ), SelbergSpectralGap.HasMeanZero f → SelbergSpectralGap.l2Norm (SelbergSpectralGap.averagingOperator (SelbergSpectralGap.selbergGeneratingSet p) f) ≤ (1 - c) * SelbergSpectralGap.l2Norm f

Selberg's spectral gap theorem. There exists a universal constant $c > 0$ such that for every prime $p$, the averaging operator $T_A$ associated to the Selberg generating set $A = \left\{\begin{pmatrix} 1 & \pm 1 \\ 0 & 1 \end{pmatrix}, \begin{pmatrix} 1 & 0 \\ \pm 1 & 1 \end{pmatrix}\right\}$ on $\mathrm{SL}_2(\mathbb{F}_p)$ satisfies $\sigma_1(T_A) \le 1 - c$; equivalently, $\|T_A f\|_{\ell^2} \le (1-c)\|f\|_{\ell^2}$ for every mean-zero $f$.