Eq. (2.1) — Rayleigh's principle: $(Qf, f) \ge \lambda_1 \|f\|^2$ for $f \perp \mathbf 1$

Let $G = (V, E)$ be a connected finite simple graph on $n \ge 2$ vertices, with Laplacian $Q$ and algebraic connectivity $\lambda_1 = \lambda_1(G)$. Let $L^2(V)$ be the space of real functions on $V$ with scalar product $(f, g) = \sum_{v} f(v) g(v)$ and norm $\|f\| = \sqrt{(f,f)}$. If $f \in L^2(V)$ is orthogonal to the constants, i.e. $\sum_{v \in V} f(v) = 0$, then

This is the variational side of $\lambda_1$: it converts the spectral definition into a lower bound for the quadratic form $(Qf, f) = \sum_{\{u,v\} \in E} (f(u) - f(v))^2$, and it is the only place where the eigenvalue enters the proof of Lemma 2.1.

Formalization Note $(f, g)$ is dotProduct (⬝ᵥ) and $Qf$ is G.lapMatrix ℝ *ᵥ f. $\lambda_1$ is defined spectrally (the mission's lambda1), so the statement is not definitional.