Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Ferrers bound for spanning trees in bipartite graphs

Boon Suan Ho

Abstract

We prove Ehrenborg's conjecture that every connected bipartite graph $G$ with parts of size $m$ and $n$ has at most $\frac{1}{mn}\prod_{v\in V(G)} \operatorname{deg}(v)$ spanning trees, and that equality holds if and only if $G$ is a Ferrers graph. The proof is fully formalized in Lean 4.

The Ferrers bound for spanning trees in bipartite graphs

Abstract

We prove Ehrenborg's conjecture that every connected bipartite graph with parts of size and has at most spanning trees, and that equality holds if and only if is a Ferrers graph. The proof is fully formalized in Lean 4.
Paper Structure (5 sections, 13 theorems, 109 equations, 1 figure)

This paper contains 5 sections, 13 theorems, 109 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Determinant reduction
  3. Projection identities
  4. Proof of the theorem
  5. Proof of Ky Fan's maximum principle

Key Result

Corollary 1

Let $G=(X\sqcup Y,E)$ be a bipartite graph. Define where the sum ranges over all spanning trees $T$ of $G$ (so $P_G$ is the zero polynomial if $G$ is disconnected). Then, for every choice of nonnegative reals $z_v$$(v\in V(G))$, we have

Figures (1)

  • Figure 1: The edges of a Ferrers graph are in direct correspondence with the boxes in a Ferrers diagram. (Reproduced from David Eppstein, "Four open from IPAM" EppsteinIPAM, 2009, CC BY 4.0 license.)

Theorems & Definitions (27)

  • Corollary
  • Theorem 1
  • Theorem 2: Kirchhoff's matrix-tree theorem
  • Proposition 3: Schur complement determinant formula
  • Theorem 4: Ky Fan's maximum principle KyFan
  • proof
  • Definition 5
  • Proposition 6
  • proof
  • Remark 7
  • ...and 17 more