Remark 2.3 — $\lambda_1 \le \frac{n}{n-1}\min_v d(v)$

Proved

AlonMilman.Diameter.remark_2_3

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

graph-theoryp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1spectral-graph-theory

Let $G = (V, E)$ be a connected finite simple graph on $n \ge 2$ vertices, $d(v)$ the degree of $v$ , and $\lambda_1 = \lambda_1(G)$ the second-smallest eigenvalue of its Laplacian. Then

\lambda_1 \le \frac{n}{n-1}\,\min\{d(v) : v \in V\}.

In the proof of Theorem 2.6 this gives $\sqrt{2d/\lambda_1} \ge 1$ , where $d$ is the maximum degree; the bound itself goes back to Fiedler.

Formalization Note $\min_v d(v)$ is Mathlib's SimpleGraph.minDegree; $n$ and the degree are cast to $\mathbb R$ .

Preamble

import Mathlib
import Definitions.Def_AlonMilman_Diameter_lambda1

Formal statement

namespace AlonMilman.Diameter

theorem remark_2_3 {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.Connected) (hn : 2 ≤ Fintype.card V) :
    lambda1 G ≤
      ((Fintype.card V : ℝ) / ((Fintype.card V : ℝ) - 1)) * (G.minDegree : ℝ) := by sorry

end AlonMilman.Diameter

Source

Alon, Milman, λ1, Isoperimetric Inequalities for Graphs, and Superconcentrators, J. Combin. Theory Ser. B 38 (1985), p. 78, Remark 2.3 (first sentence)

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Remark 2.3 — λ1≤nn−1min⁡vd(v)\lambda_1 \le \frac{n}{n-1}\min_v d(v)λ1​≤n−1n​minv​d(v)

Remark 2.3 — $\lambda_1 \le \frac{n}{n-1}\min_v d(v)$