Lower companion of the Courant–Fischer bridge #
le_algConn_of_forall: if the Laplacian quadratic form dominates c · ‖x‖² for
every x orthogonal to the all-ones vector (∑ i, x i = 0), then c ≤ algConn G.
This is the reverse direction used to certify the lower bound algConn ≥ 2.
theorem
ACMax.le_algConn_of_forall
{V : Type u_1}
[Fintype V]
[Nonempty V]
[Nontrivial V]
(G : SimpleGraph V)
(c : ℝ)
(h : ∀ (x : V → ℝ), ∑ i : V, x i = 0 → c * ∑ i : V, x i ^ 2 ≤ x ⬝ᵥ (SimpleGraph.lapMatrix ℝ G).mulVec x)
: