Theorems
Lindström–Gessel–Viennot and total positivity
The Lindström–Gessel–Viennot lemma expresses a minor of a path-network matrix as a signed count of families of vertex-disjoint paths. When every crossing family cancels against another, only nonintersecting families survive, and the minor is a sum of nonnegative path weights.
Building on the path-cancellation proof in the LeanLGV library:
- Total nonnegativity: a finite path network with nonnegative weights and ordered cancellation certificates for every pair of increasing row and column selections has a totally nonnegative matrix.
- Pólya frequency sequences: if every strictly increasing Toeplitz minor of a sequence is realized by such a network, then the sequence is a Pólya frequency sequence.
- Chip networks: for words of nonnegative lower-bidiagonal chips $G$ and $K$, with $K$ strictly lower triangular, the repeated-chip kernel sequence is a Pólya frequency sequence. The associated kernel row, in the sense of Brändén and Saud Leite, is a PF polynomial.
- Path counting: weighted paths of exact length $n$ are counted by the $n$-th power of the edge-sum matrix.
References
B. Lindström, “On the vector representations of induced matroids,” Bull. London Math. Soc. 5 (1973), 85–90. I. Gessel and G. Viennot, “Binomial determinants, paths, and hook length formulae,” Adv. Math. 58 (1985), 300–321. The kernel rows connect to the Brändén–Saud Leite page.
≔ Definitions
Index set of a Toeplitz minor
structure StrictToeplitzMinorIndex (n : ℕ) where
sourceRow : Fin n → ℕ
sinkColumn : Fin n → ℕ
sourceRow_strictMono : StrictMono sourceRow
sinkColumn_strictMono : StrictMono sinkColumn
Lower-bidiagonal chip
structure Chip (R : Type*) (N : ℕ) where
diagonal : Fin (N + 1) → R
subdiagonal : Fin N → R
Matrix of a word of chips
def wordMatrix {R : Type*} [Semiring R] (word : List (Chip R N)) :
Matrix (Fin (N + 1)) (Fin (N + 1)) R :=
(word.map Chip.matrix).prod
Repeated-chip kernel sequence
def kernelSequence (G K : List (Chip ℝ N)) (q : ℕ) : ℝ :=
(wordMatrix G * (wordMatrix K * wordMatrix G) ^ q) (Fin.last N) 0
⊢ Theorems
Path networks give totally nonnegative matrices
theorem matrix_isTotallyNonneg_of_orderedCertificates
{R : Type u} {ι : Type v}
[CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [PartialOrder ι]
(N : LGV.FinitePathNetwork R ι)
(certificate : ∀ {n : ℕ} {rows cols : Fin n → ι},
StrictMono rows → StrictMono cols →
OrderedCancellationCertificate (N.reindex rows cols))
(hweight : ∀ {s t : ι} (p : N.Path s t), 0 ≤ N.weight p) :
N.matrix.IsTotallyNonneg
Path networks give Pólya frequency sequences
theorem isPolyaFreqSeq_of_minorOrderedCertificates
{a : ℕ → ℝ}
(network : ∀ {n : ℕ}, StrictToeplitzMinorIndex n →
LGV.FinitePathNetwork ℝ (Fin n))
(hmatrix : ∀ {n : ℕ} (I : StrictToeplitzMinorIndex n),
(network I).matrix = I.toeplitzSubmatrix a)
(certificate : ∀ {n : ℕ} (I : StrictToeplitzMinorIndex n),
LGV.FinitePathNetwork.OrderedCancellationCertificate (network I))
(hweight : ∀ {n : ℕ} (I : StrictToeplitzMinorIndex n)
{s t : Fin n} (p : (network I).Path s t),
0 ≤ (network I).weight p) :
IsPolyaFreqSeq a
Repeated-chip kernel sequences are PF
theorem kernelSequence_isPolyaFreqSeq
(G K : List (Chip ℝ N))
(hG : ∀ c ∈ G, c.IsNonnegative)
(hK : ∀ c ∈ K, c.IsNonnegative)
(hKstrict : ∀ i j, i.val ≤ j.val → wordMatrix K i j = 0) :
IsPolyaFreqSeq (kernelSequence G K)
Repeated-chip kernel rows are PF polynomials
theorem kernelRow_isPFPolynomial
(G K : List (Chip ℝ N))
(hG : ∀ c ∈ G, c.IsNonnegative)
(hK : ∀ c ∈ K, c.IsNonnegative)
(hKstrict : ∀ i j, i.val ≤ j.val → wordMatrix K i j = 0) :
IsPFPolynomial
(BrandenLeite.kernelRow (wordMatrix G) (wordMatrix K) (Fin.last N))
Paths of length n and powers of the edge matrix
theorem sum_weight_exactLength_eq_edgeSumMatrix_pow
[Semiring R] [Fintype V] [DecidableEq V] [∀ a b : V, Fintype (a ⟶ b)]
(w : ∀ {a b : V}, (a ⟶ b) → R) (a b : V) (n : ℕ) :
∑ p : ExactLength a b n, p.1.weight w = (edgeSumMatrix w ^ n) a b
Lean source RealRooted/Challenges/LGV.lean at revision 5827550b.