Heron–Rota–Welsh conjecture

DefinitionRank of a set in a matroid, as a natural number#✓fully proved

For a matroid \(M\) and a set \(X\), this is the rank \(r(X)\) of \(X\) in \(M\), the size of a largest independent set of \(M\) contained in \(X\), taken as a natural number; it is \(0\) when this rank is infinite.

noncomputable def finRank {α : Type*} (M : Matroid α) (X : Set α) : ℕ :=
  (M.eRk X).toNat

Used by 2

Used byAbsolute coefficients of the characteristic polynomial of a matroid · Coefficients of the characteristic polynomial of a matroid

DefinitionCoefficients of the characteristic polynomial of a matroid#✓fully proved

Let \(M\) be a finite matroid on the ground set \(E\) with rank function \(r\), and let \(\chi_M(\lambda) = \sum_{I \subseteq E} (-1)^{|I|} \lambda^{r(E) - r(I)}\) be its characteristic polynomial. For a natural number \(j\), this is the integer coefficient of \(\lambda^j\) in \(\chi_M\), that is, the sum of \((-1)^{|I|}\) over the subsets \(I \subseteq E\) with \(r(E) - r(I) = j\).

noncomputable def charPolyCoeff {α : Type*} (M : Matroid α) [M.Finite] (j : ℕ) : ℤ :=
  ∑ I ∈ M.ground_finite.toFinset.powerset.filter
      (fun I : Finset α => finRank M M.E - finRank M (I : Set α) = j), (-1) ^ I.card

Uses 1 · Used by 1

Statement usesRank of a set in a matroid, as a natural number

Used byAbsolute coefficients of the characteristic polynomial of a matroid

DefinitionAbsolute coefficients of the characteristic polynomial of a matroid#✓fully proved

Let \(M\) be a finite matroid on the ground set \(E\) with rank function \(r\) and characteristic polynomial \(\chi_M(\lambda) = \sum_{I \subseteq E} (-1)^{|I|} \lambda^{r(E) - r(I)}\). For a natural number \(k\), \(w_k(M)\) is the absolute value of the coefficient of \(\lambda^{r(E) - k}\) in \(\chi_M\) when \(k \le r(E)\), and \(w_k(M) = 0\) when \(k > r(E)\).

noncomputable def charPolyAbsCoeff {α : Type*} (M : Matroid α) [M.Finite] (k : ℕ) : ℕ :=
  if k ≤ finRank M M.E then (charPolyCoeff M (finRank M M.E - k)).natAbs else 0

Uses 2 · Used by 1

Statement usesCoefficients of the characteristic polynomial of a matroid · Rank of a set in a matroid, as a natural number

Used byLog-concavity of the characteristic polynomial of a matroid, statement

DefinitionLog-concavity of the characteristic polynomial of a matroid, statement#✓fully proved

For every finite matroid \(M\) on a ground set \(E\) with rank function \(r\), let \(w_k(M)\) be the absolute value of the coefficient of \(\lambda^{r(E) - k}\) in the characteristic polynomial \(\chi_M(\lambda) = \sum_{I \subseteq E} (-1)^{|I|} \lambda^{r(E) - r(I)}\) when \(k \le r(E)\), and \(w_k(M) = 0\) when \(k > r(E)\). Then \(w_{k-1}(M) \, w_{k+1}(M) \le w_k(M)^2\) for every natural number \(k \ge 1\).

This is part (a) of Stanley's Problem 25 (Read–Hoggar–Rota–Heron–Welsh).

def characteristicPolynomialLogConcave : Prop :=
  ∀ (α : Type) (M : Matroid α) [M.Finite] (k : ℕ), 1 ≤ k →
    charPolyAbsCoeff M (k - 1) * charPolyAbsCoeff M (k + 1) ≤ charPolyAbsCoeff M k ^ 2

Uses 1 · Used by 1

Statement usesAbsolute coefficients of the characteristic polynomial of a matroid

Used byAdiprasito–Huh–Katz theorem (Heron–Rota–Welsh conjecture)

TheoremAdiprasito–Huh–Katz theorem (Heron–Rota–Welsh conjecture)#●ready to prove

For every finite matroid \(M\) on a ground set \(E\) with rank function \(r\), let \(w_k(M)\) be the absolute value of the coefficient of \(\lambda^{r(E) - k}\) in the characteristic polynomial \(\chi_M(\lambda) = \sum_{I \subseteq E} (-1)^{|I|} \lambda^{r(E) - r(I)}\) when \(k \le r(E)\), and \(w_k(M) = 0\) when \(k > r(E)\). Then \(w_{k-1}(M) \, w_{k+1}(M) \le w_k(M)^2\) for every natural number \(k \ge 1\).

Huh had proved the case of graphs and realizable matroids in characteristic \(0\).

public theorem_wanted characteristicPolynomialLogConcave_holds : characteristicPolynomialLogConcave

Sources

• R. P. Stanley, Positivity Problems and Conjectures in Algebraic Combinatorics (1999), Problem 25 (Read–Hoggar–Welsh–Mason conjectures); resolution: K. Adiprasito, J. Huh and E. Katz, Hodge theory for combinatorial geometries, Ann. of Math. 188 (2018), 381-452, arXiv:1511.02888; J. Huh, Milnor numbers of projective hypersurfaces and the chromatic polynomial of graphs, J. Amer. Math. Soc. 25 (2012), 907-927 (graphs), Theorem 9.9(2) (arXiv numbering): for every matroid M the coefficients of the characteristic polynomial form a log-concave sequence; §1, Conjecture 1.1 defines χ_M and w_k as above, https://arxiv.org/abs/1511.02888.

Uses 1

Statement usesLog-concavity of the characteristic polynomial of a matroid, statement

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.