Bourgain–Gamburd: spectral gap for dense subgroups of $SU(d)$ with algebraic entries

Open

SpectralGapConjecture.bourgain_gamburd_SUd

by Lucas · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

additive-combinatoricsgroup-theoryspectral-gap

Let $d \ge 2$ and $n \ge 2$ , and let $\mu_d$ be the normalized Haar measure on $SU(d)$ . Let $g_1,\dots,g_n\in SU(d)$ satisfy:

every entry of every $g_j$ is an algebraic number;
the subgroup of $SU(d)$ generated by $g_1,\dots,g_n$ is dense in $SU(d)$ .

Then the Hecke operator $(z_g f)(x) = \sum_{j=1}^{n}\bigl(f(g_jx) + f(g_j^{-1}x)\bigr)$ on $L^2(SU(d),\mu_d)$ has a spectral gap:

\lambda_1(z_g) < 2n .

This extends the $SU(2)$ theorem of Bourgain–Gamburd to all $SU(d)$ and replaces freeness by density.

Formalization Note. The source assumes the generated group is Zariski dense in $SL_d(\mathbb C)$ ; by the source's footnote 1 this is equivalent to topological density in $SU(d)$ , which is what is stated here.

Preamble

import Mathlib
import Definitions.Def_SpectralGapConjecture_HeckeSU

open MeasureTheory

Formal statement

namespace SpectralGapConjecture

theorem bourgain_gamburd_SUd (d : ℕ) (hd : 2 ≤ d) (n : ℕ) (hn : 2 ≤ n) (g : Fin n → SU d)
    (halg : ∀ j a b, IsAlgebraic ℚ ((g j : Matrix (Fin d) (Fin d) ℂ) a b))
    (hdense : Dense ((Subgroup.closure (Set.range g) : Subgroup (SU d)) : Set (SU d))) :
    HasSpectralGap (haarSU d) g := by sorry

end SpectralGapConjecture

Source

J. Bourgain, A. Gamburd, A spectral gap theorem in SU(d), J. Eur. Math. Soc. 14 (2012), arXiv:1108.6264, Theorem 1 and footnote 1, p. 2

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Bourgain–Gamburd: spectral gap for dense subgroups of SU(d)SU(d)SU(d) with algebraic entries

Bourgain–Gamburd: spectral gap for dense subgroups of $SU(d)$ with algebraic entries