Documentation

Formalizations.Combinatorics.SimpleGraph.MatchingPolynomial.HeilmannLiebBound

The Heilmann–Lieb root bound #

For a finite graph of maximum degree at most Δ ≥ 2, every root of the matching polynomial lies in [-2√(Δ - 1), 2√(Δ - 1)].

For a forest the matching polynomial is the characteristic polynomial of the adjacency matrix; a weighted Gershgorin (Collatz–Wielandt) bound with weight √(Δ - 1)^(-depth) bounds its eigenvalues by 2√(Δ - 1). The path tree T(G, u) is a forest of maximum degree at most Δ, and μ(G) divides μ(T(G, u)) for connected G, so the bound transfers; components handle the general case.

Main results #

References #

source
theorem SimpleGraph.collatzWielandt {W : Type u_2} [Fintype W] [DecidableEq W] (A : Matrix W W ℝ) (w : W → ℝ) (B : ℝ) (hw : ∀ (i : W), 0 < w i) (hA : ∀ (i j : W), 0 ≤ A i j) (hrow : ∀ (i : W), ∑ j : W, A i j * w j ≤ B * w i) (μ : ℝ) (hμ : A.charpoly.IsRoot μ) :
|μ| ≤ B

(1) Weighted Gershgorin / Collatz–Wielandt. A nonnegative matrix with a strictly positive test vector w whose weighted row sums satisfy ∑ⱼ Aᵢⱼ wⱼ ≤ B wᵢ has every real eigenvalue (root of A.charpoly) bounded by B in absolute value.

Proof = the weighted eigenvector argument (Collatz–Wielandt): a charpoly root yields an eigenvector v ≠ 0 (Matrix.exists_mulVec_eq_zero_iff via eval_charpoly); pick the coordinate k maximising |vⱼ|/wⱼ; then |μ|·|v_k| = |∑ⱼ A_kⱼ vⱼ| ≤ ∑ⱼ A_kⱼ wⱼ (|vⱼ|/wⱼ) ≤ (∑ⱼ A_kⱼ wⱼ)(|v_k|/w_k) ≤ B w_k (|v_k|/w_k) = B|v_k|, and |v_k| > 0.

source
theorem SimpleGraph.forest_bounded_of_weight {W : Type u_2} [Fintype W] [DecidableEq W] (F : SimpleGraph W) [DecidableRel F.Adj] (hF : F.IsAcyclic) (Δ : ℕ) (w : W → ℝ) (hw : ∀ (v : W), 0 < w v) (hrow : ∀ (v : W), ∑ u : W, adjMatrix ℝ F v u * w u ≤ bruhatTitsBound Δ * w v) :
MSS.BoundedBy F.matchingPoly (bruhatTitsBound Δ)

(2a) Forest bound from a test weight. Reduces the forest band bound to exhibiting a strictly positive weight w with ∑ᵤ A_vu wᵤ ≤ (bruhatTitsBound Δ)·w_v for all v: μ(F) = charpoly(A_F) is real-rooted, and collatzWielandt bounds its roots by bruhatTitsBound Δ. The adjacency matrix is nonnegative (adjMatrix_apply).

source
theorem SimpleGraph.rowsum_arith {W : Type u_2} [DecidableEq W] (N : Finset W) (δ : W → ℕ) (d : ℕ) (s : ℝ) (Δ : ℕ) (hs : 0 < s) (hs2 : s ^ 2 = ↑Δ - 1) (hΔ : 2 ≤ Δ) (hcard : N.card ≤ Δ) (hpm : ∀ u ∈ N, δ u = d + 1 ∨ δ u + 1 = d) (hpar : {u ∈ N | δ u + 1 = d}.card ≤ 1) :
∑ u ∈ N, s ^ (-↑(δ u)) ≤ 2 * s * s ^ (-↑d)

(2b-arith) The row-sum bound, pure arithmetic. With depth δ, base s = √(Δ−1) and weight wᵤ = s^(−δ u), given that every summand index u ∈ N is at depth d±1 (hpm), at most one is closer (hpar), and |N| ≤ Δ, the weighted neighbour sum is ≤ 2s · s^(−d) = bruhatTitsBound Δ · w_v. Closer terms equal s^(−d)·s, farther terms s^(−d)·s⁻¹; the count inequality a·(Δ−1) + b ≤ 2(Δ−1) (a ≤ 1, a+b ≤ Δ, Δ ≥ 2, i.e. (Δ−2)(1−a) ≥ 0) closes it.

source
theorem SimpleGraph.forest_adj_dist_pm_one {W : Type u_2} [Fintype W] [DecidableEq W] (F : SimpleGraph W) [DecidableRel F.Adj] (hF : F.IsAcyclic) (ρ : W) {u v : W} (huv : F.Adj u v) (hu : F.Reachable ρ u) :
F.dist ρ u = F.dist ρ v + 1 ∨ F.dist ρ u + 1 = F.dist ρ v

(2b-tree, Fact 1) Adjacent vertices differ in root-distance by exactly 1. For an acyclic F, a root ρ, an edge u ∼ v with u reachable from ρ: dist ρ u = dist ρ v + 1 or dist ρ u + 1 = dist ρ v. The ≤ 1 bounds are dist_le on the shortest path concatenated with the edge; the ≠ is bipartiteness (IsAcyclic.isBipartite): a Bool-colouring c has Even (dist ρ ·) ↔ (c ρ ↔ c ·) (even_length_iff_congr on shortest paths), and c u ≠ c v (Coloring.valid), so equal distances would force equal parities, contradiction.

source
theorem SimpleGraph.exists_isPath_length_eq_dist {W : Type u_2} [DecidableEq W] (F : SimpleGraph W) {ρ x : W} (hr : F.Reachable ρ x) :
∃ (p : F.Walk ρ x), p.IsPath ∧ p.length = F.dist ρ x

A shortest walk is a path: there is a p : Walk ρ x with p.IsPath and p.length = dist ρ x (bypass of any minimal-length walk).

source
theorem SimpleGraph.forest_le_one_parent {W : Type u_2} [Fintype W] [DecidableEq W] (F : SimpleGraph W) [DecidableRel F.Adj] (hF : F.IsAcyclic) (ρ v : W) :
{u ∈ F.neighborFinset v | F.dist ρ u + 1 = F.dist ρ v}.card ≤ 1

(2b-tree, Fact 2) At most one neighbour is one step closer to the root. For an acyclic F and any ρ, v, at most one neighbour u of v has dist ρ u + 1 = dist ρ v. Two such u₁, u₂ give two shortest paths ρ → v ending in the edges s(v,u₁), s(v,u₂); by path_unique these paths coincide, and IsPath.eq_penultimate_of_mem_edges makes both u₁ and u₂ the (unique) penultimate vertex, so u₁ = u₂.

source
def SimpleGraph.forest_bounded_target :
Prop

(2) Forest adjacency eigenvalue bound. Type-polymorphic so it applies to the path tree T(G,u) (whose vertex type differs from V). Reduced by forest_bounded_of_weight to constructing a test weight + proving the row-sum bound.

Hypothesis 2 ≤ Δ is necessary: for Δ = 1, bruhatTitsBound 1 = 0, but a single edge K₂ (maximum degree 1) has μ = X² − 1 with roots ±1, so the band [0,0] is violated. Heilmann–Lieb 2√(Δ−1) holds for Δ ≥ 2 (for Δ ≤ 1 the graph is a matching, roots in {−1,0,1}).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem SimpleGraph.forest_bounded_proof :
    forest_bounded_target

    (2) Forest adjacency eigenvalue bound. Assembles all of (2): root each component at (connectedComponentMk v).out, weight w v = (√(Δ−1))^(−dist(r v, v)) (positive since Δ ≥ 2), convert the adjacency row sum to a neighbour sum, rewrite each neighbour's weight using r u = r v (connectedComponentMk_eq_of_adj), and apply rowsum_arith fed by Fact 1 (forest_adj_dist_pm_one) and Fact 2 (forest_le_one_parent); close with forest_bounded_of_weight (which routes through collatzWielandt + matchingPoly_forest_eq_charpoly).

    source
    theorem SimpleGraph.pathTree_degree_le {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {Δ : ℕ} (hdeg : ∀ (v : V), G.degree v ≤ Δ) (u : V) (p : G.PathFrom u) :
    (G.pathTree u).degree p ≤ Δ

    (4) Path-tree degree bound. deg_{T(G,u)}(p) ≤ deg_G(p.endpoint) ≤ Δ. The map b ↦ b.endpoint injects the path-tree neighbours of p into the G-neighbours of p's endpoint: every neighbour b (a child Grows p b or the parent Grows b p) has b.1 ∈ N_G(p.1); and it is injective — two children with the same endpoint have the same (forced) walk, the parent is unique (Grows.parent_unique), and a child and the parent cannot share an endpoint (the child's endpoint is off p's support, the parent's is on it).

    source
    theorem SimpleGraph.connected_matchingPoly_bounded {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (Δ : ℕ) (hΔ : 2 ≤ Δ) (hdeg : ∀ (v : V), G.degree v ≤ Δ) (hG : G.Connected) :
    MSS.BoundedBy G.matchingPoly (bruhatTitsBound Δ)

    (3) Transfer — connected case. μ(G) divides μ(T(G,u)), and the path tree T(G,u) is a forest of maximum degree ≤ Δ (pathTree_degree_le, pathTree_isAcyclic), so its matching polynomial is in the Ramanujan band (forest_bounded_proof); BoundedBy.of_dvd transfers the band to μ(G). The matchingPoly_inst_irrel rewrite aligns the Σ-paths Fintype/DecidableRel instances (the lemma-(e) whnf wall).

    source
    theorem SimpleGraph.matchingPoly_bounded {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (Δ : ℕ) (hΔ : 2 ≤ Δ) (hdeg : ∀ (v : V), G.degree v ≤ Δ) :
    MSS.BoundedBy G.matchingPoly (bruhatTitsBound Δ)

    Heilmann–Lieb root bound — general case. For ANY finite graph G with 2 ≤ Δ and maximum degree ≤ Δ, every root of μ(G) lies in the Ramanujan band [−2√(Δ−1), 2√(Δ−1)]. Reduces to the connected case over components: μ(G) = ∏_C μ(G[C.supp]), each induced component is connected (maximal_connected_induce_supp) with degree ≤ Δ (its G-neighbours stay in the component, so degree_induce_of_neighborSet_subset gives equality), and BoundedBy multiplies.