Unfolding the definitions of \(\beta \) and \(\gamma \) and simplifying the field expressions, the equality holds by algebraic manipulation.

We observe that \(0 \leq \lambda _2^2\) (since it is a square), \(0 {\lt} s - \lambda _2\) (since \(\lambda _2 {\lt} s\)), and hence \(0 \leq 4s(s-\lambda _2)a\) by positivity (since \(s {\gt} 0\), \(s - \lambda _2 {\gt} 0\), \(a \geq 0\)). The result follows by linear arithmetic from these three facts.

We proceed by cases on whether \(\lambda _2 \geq 0\) or \(\lambda _2 {\lt} 0\).

Case 1: \(\lambda _2 \geq 0\). We apply the fact that \(\lambda _2 \leq \sqrt{D}\) whenever \(\lambda _2^2 \leq D\) and \(D \geq 0\). Since \(4s(s-\lambda _2)a \geq 0\) (using \(s {\gt} 0\), \(s - \lambda _2 {\gt} 0\), \(a \geq 0\)), we have \(\lambda _2^2 \leq \lambda _2^2 + 4s(s-\lambda _2)a\), from which the result follows.

Case 2: \(\lambda _2 {\lt} 0\). Since \(\sqrt{\cdot } \geq 0\), we have \(\lambda _2 {\lt} 0 \leq \sqrt{\lambda _2^2 + 4s(s-\lambda _2)a}\).

Unfolding the definition, \(\gamma (s, \lambda _2, a) = (\sqrt{\lambda _2^2 + 4s(s-\lambda _2)a} - \lambda _2) / (2(s-\lambda _2))\). The numerator is nonneg by the lemma \(\sqrt{\lambda _2^2 + 4s(s-\lambda _2)a} \geq \lambda _2\), and the denominator \(2(s - \lambda _2) {\gt} 0\) since \(\lambda _2 {\lt} s\). Hence the quotient is nonneg.

Unfolding the definition and substituting \(a = 0\), we compute:

using \(\sqrt{\lambda _2^2} = \lambda _2\) (since \(\lambda _2 \geq 0\)) by simplification.

Unfolding the definitions and cross-multiplying by \(2(s - \lambda _2) {\gt} 0\), it suffices to show

where \(D = \lambda _2^2 + c\alpha \), \(\tilde{D} = \lambda _2^2 + c\tilde{\alpha }\), and \(c = 4s(s-\lambda _2) {\gt} 0\).

Set \(u = \sqrt{\tilde{D}}\) and \(v = \sqrt{D}\). Both are nonneg, and \(\lambda _2 \leq u \leq v\) (by the lemma \(\sqrt{\cdot } \geq \lambda _2\) and monotonicity of square root: \(\tilde{D} \leq D\) since \(c {\gt} 0\) and \(\tilde{\alpha } \leq \alpha \)). In particular, \((u - \lambda _2)(v - \lambda _2) \geq 0\).

It suffices to show \((v - \lambda _2)\tilde{\alpha } \leq (u - \lambda _2)\alpha \), which in turn follows from the intermediate claim

since adding \((u - \lambda _2)\tilde{\alpha }\) to both sides yields the desired inequality.

We prove this intermediate claim by cases on whether \(v + u {\gt} 0\) or \(v + u = 0\).

Case 1: \(v + u {\gt} 0\). We multiply through by \(v + u\) and compute:

using \(u \leq v\) and \(u - \lambda _2 \geq 0\) and \(\alpha - \tilde{\alpha } \geq 0\). Then \((u-\lambda _2)(v+\lambda _2)(\alpha -\tilde{\alpha }) \leq (u-\lambda _2)(\alpha -\tilde{\alpha })(v+u)\) using \(\lambda _2 \leq u\). Dividing by \(v + u {\gt} 0\) gives the claim.

Case 2: \(v + u = 0\). Since \(u, v \geq 0\), we have \(u = v = 0\). Then \(\lambda _2 \leq u = 0\), so \(\lambda _2 \leq 0\). Setting \(u = v = 0\) and simplifying, both sides reduce to \(0 \leq (-\lambda _2)(\alpha - \tilde{\alpha })\), which holds since \(-\lambda _2 \geq 0\) and \(\alpha - \tilde{\alpha } \geq 0\).

This follows immediately from the handshaking lemma twice_card_edgeFinset_eq, which gives \(2|E(G)| = s\, |V|\), by linear arithmetic.

Set \(S = \Gamma (E)\), \(n = |V|\), and \(\tilde{\alpha } = |E|/|E(G)|\).

First, \(S\) is nonempty: take any edge \(e \in E\); writing \(e = \{ a, b\} \), the vertex \(a\) satisfies \(a \in \Gamma (E)\) by the membership criterion mem_incidentVertices.

Moreover, \(E \subseteq \operatorname {inducedEdges}(G, S)\) by the lemma subset_inducedEdges_incidentVertices.

We consider two cases based on whether \(S = V\) or \(S \subsetneq V\).

Case 1: \(|S| = |V|\) (i.e., \(S\) is all of \(V\)). We must show \(\gamma (s, \lambda _2, \tilde{\alpha })\, n \leq |S| = n\), i.e., \(\gamma (s,\lambda _2,\tilde{\alpha }) \leq 1\). Unfolding the definition, this is \(\sqrt{\lambda _2^2 + 4s(s-\lambda _2)\tilde{\alpha }} - \lambda _2 \leq 2(s-\lambda _2)\), i.e., \(\sqrt{\lambda _2^2 + 4s(s-\lambda _2)\tilde{\alpha }} \leq 2s - \lambda _2\). Since \(\tilde{\alpha } \leq 1\) (as \(|E| \leq |E(G)|\)), we have \(\lambda _2^2 + 4s(s-\lambda _2)\tilde{\alpha } \leq \lambda _2^2 + 4s(s-\lambda _2) = (2s - \lambda _2)^2\). Taking square roots and using \(2s - \lambda _2 \geq 0\), we conclude \(\sqrt{\lambda _2^2 + 4s(s-\lambda _2)\tilde{\alpha }} \leq 2s - \lambda _2\).

Case 2: \(|S| {\lt} |V|\). Let \(\gamma ' = |S|/n\). Apply the Alon–Chung theorem (alonChung) to \(G\) and \(S\):

Since \(|E| \leq |\operatorname {inducedEdges}(G,S)|\), we obtain \(\tilde{\alpha } \leq \gamma '^2 + \tfrac {\lambda _2}{s}\gamma '(1-\gamma ')\).

It remains to show \(\gamma (s,\lambda _2,\tilde{\alpha }) \leq \gamma '\). Unfolding, this is

Let \(R = \lambda _2 + 2(s-\lambda _2)\gamma '\). We verify \(R {\gt} 0\): since \(\tilde{\alpha } {\gt} 0\) and \(\tilde{\alpha } \leq \alpha (\gamma ')\), the quantity \(\alpha (\gamma ') {\gt} 0\), which implies \(\gamma ' + \tfrac {\lambda _2}{s}(1-\gamma ') {\gt} 0\), and hence \(\lambda _2 + (s-\lambda _2)\gamma ' {\gt} 0\); adding \((s-\lambda _2)\gamma ' {\gt} 0\) gives \(R {\gt} 0\).

Squaring both sides (both nonneg), we need \(\lambda _2^2 + 4s(s-\lambda _2)\tilde{\alpha } \leq R^2 = \lambda _2^2 + 4(s-\lambda _2)\lambda _2\gamma ' + 4(s-\lambda _2)^2\gamma '^2\), i.e.,

Dividing by \(4(s-\lambda _2) {\gt} 0\), this becomes \(s\tilde{\alpha } \leq s\, \alpha (\gamma ')\), which follows from \(\tilde{\alpha } \leq \alpha (\gamma ')\) by multiplying by \(s {\gt} 0\). Taking square roots gives the desired inequality, completing the proof.

We first handle the edge case \(E = \emptyset \): the bound \(|\Gamma (\emptyset )| \geq \beta \cdot 0 = 0\) holds trivially by simp.

Assume \(E \neq \emptyset \). Let \(n = |V|\), \(\tilde{\alpha } = |E|/|E(G)|\). We have \(0 {\lt} \tilde{\alpha } \leq \alpha \) (the upper bound since \(|E| \leq \alpha |E(G)|\)).

Step 1 (lower bound via \(\gamma \)). By Lemma 354,

Step 2 (concavity). By Lemma 352 (with \(\tilde{\alpha } \leq \alpha \)),

Step 3 (handshaking). By Lemma 353, \(|E(G)| = \tfrac {s}{2}n\), so

Combining. Using Lemma 347 (\(\beta = 2\gamma (\alpha )/(s\alpha )\)), we compute:

where the first inequality uses Step 2 and \(\alpha {\gt} 0\), and the last uses Step 1.