Monotone column permanent conjecture

DefinitionThe polynomial \(\operatorname{per}(A + xJ)\)#✓fully proved

For a real \(n \times n\) matrix \(A\), this is the polynomial \(\operatorname{per}(A + xJ) \in \mathbb{R}[x]\), where \(J\) is the \(n \times n\) all-ones matrix: the permanent of the \(n \times n\) matrix of polynomials whose \((i, j)\) entry is \(A_{ij} + x\).

noncomputable def permanentAddXJ {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) : Polynomial ℝ :=
  (A.map Polynomial.C + Matrix.of fun _ _ => Polynomial.X).permanent

Used by 1

Used byThe Haglund–Ono–Wagner monotone column permanent conjecture

DefinitionThe Haglund–Ono–Wagner monotone column permanent conjecture#✓fully proved

This is the statement that for every \(n \in \mathbb{N}\) and every real \(n \times n\) matrix \(A\) whose columns are weakly increasing (\(A_{ij} \le A_{i'j}\) whenever \(i \le i'\)), every complex root of the polynomial \(\operatorname{per}(A + xJ) \in \mathbb{R}[x]\) is real, where \(J\) is the \(n \times n\) all-ones matrix.

def monotoneColumnPermanentConjecture : Prop :=
  ∀ (n : ℕ) (A : Matrix (Fin n) (Fin n) ℝ), (∀ i i' j, i ≤ i' → A i j ≤ A i' j) →
    ((permanentAddXJ A).map (algebraMap ℝ ℂ)).IsRealRooted

Uses 2 · Used by 1

Statement usesThe polynomial \(\operatorname{per}(A + xJ)\) · Real-rooted polynomials

Used byBrändén–Haglund–Visontai–Wagner theorem (monotone column permanent conjecture)

TheoremBrändén–Haglund–Visontai–Wagner theorem (monotone column permanent conjecture)#●ready to prove

For every \(n \in \mathbb{N}\) and every real \(n \times n\) matrix \(A\) whose columns are weakly increasing (\(A_{ij} \le A_{i'j}\) whenever \(i \le i'\)), every complex root of the polynomial \(\operatorname{per}(A + xJ) \in \mathbb{R}[x]\) is real, where \(J\) is the \(n \times n\) all-ones matrix.

Brändén, Haglund, Visontai and Wagner prove the stronger statement that the multivariate polynomial \(\operatorname{per}(z_j + A_{ij})\), in one variable \(z_j\) for each column \(j\), is real stable.

public theorem_wanted monotoneColumnPermanentConjecture_holds : monotoneColumnPermanentConjecture

Sources

• R. P. Stanley, Positivity Problems and Conjectures in Algebraic Combinatorics (1999), Problem 24 (Haglund–Ono–Wagner monotone column permanent conjecture); resolution: P. Brändén, J. Haglund, M. Visontai and D. G. Wagner, Proof of the monotone column permanent conjecture, in Notions of Positivity and the Geometry of Polynomials, Trends Math., Birkhäuser (2011), 63-78, arXiv:1010.2565, Section 1 and abstract: for every n × n monotone column matrix A, per(zJₙ + A) is a polynomial in z with only real roots (the MCPC, Conjecture 2 of Haglund-Ono-Wagner), proved in full generality via the multivariate (real stable) version, https://arxiv.org/abs/1010.2565.

Uses 1

Statement usesThe Haglund–Ono–Wagner monotone column permanent conjecture

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.