Theorem 2.5 — $b \le (1-a)/(1 + (\lambda_1/d)a\rho^2)$ for sets at distance $\rho > 1$

Let $G = (V, E)$ be a connected finite simple graph on $n \ge 2$ vertices, with maximum degree $d$ and algebraic connectivity $\lambda_1 = \lambda_1(G)$. Let $A, B \subseteq V$ and let $\rho > 1$ be an integer such that every vertex of $A$ is at graph distance at least $\rho$ from every vertex of $B$. With $a = |A|/n$ and $b = |B|/n$,

This is the one-step isoperimetric inequality: a set $A$ of relative size $a$ leaves only a small proportion of vertices at distance at least $\rho$ from it. Iterating it gives the concentration inequality of Theorem 2.6.

Formalization Note As in Lemma 2.1, $\rho$ is any integer lower bound for the pairwise distances, which is equivalent to the paper's exact distance since the bound weakens as $\rho$ decreases. $A$ and $B$ may be empty: then $a = 0$ (bound $1$) or $b = 0$, and the inequality holds as stated, so no nonemptiness hypothesis is needed. $d$ is Mathlib's SimpleGraph.maxDegree, which is at least $1$ for a connected graph with $n \ge 2$.