Special matrices

Classes of matrices defined by their structure or entries: Toeplitz, Hankel and circulant matrices, Hadamard and sign matrices, combinatorial matrices, nonnegative, doubly stochastic and totally positive matrices.

• Circulant matrices
• Hadamard matrices
• Hankel matrices
• Hurwitz transform of sequences
• M-matrices and Hurwitz stability
• Matrix scaling to doubly stochastic form
• Pascal-like matrices
• Perron–Frobenius theorem
• Principal minors of the Fourier matrix
• Toeplitz matrices
• Toeplitz–Hessenberg determinants
• Total positivity
• Zagier's matrix and Bernoulli numbers

TheoremHadamard bound for zero-one determinants#✓fully proved

Let \(n \ge 1\) and let \(B\) be an \(n \times n\) real matrix each of whose entries is \(0\) or \(1\). Then

\[|\det B| \le 2^{-n} (n+1)^{(n+1)/2}.\]

The bound comes from bordering and signing \(2B\) to obtain an \((n+1) \times (n+1)\) matrix with entries \(\pm 1\) whose determinant is \(2^n \det B\), and applying Hadamard's determinant inequality.

theorem hadamard_zero_one_determinant_bound (n : ℕ)
    (B : Matrix (Fin n) (Fin n) ℝ) (hn : 0 < n)
    (hB : ∀ i j, B i j = 0 ∨ B i j = 1) :
    |B.det| ≤ ((2 : ℝ)⁻¹) ^ n *
      Real.rpow ((n : ℝ) + 1) (((n : ℝ) + 1) / 2)

Sources

• Richard P. Brent and Adam B. Yedidia, "Computation of Maximal Determinants of Binary Circulant Matrices," Journal of Integer Sequences 21 (2018), Article 18.5.6. https://cs.uwaterloo.ca/journals/JIS/VOL21/Brent/brent11.tex, lines 226–238.

TheoremThe van der Waerden permanent bound#✓fully proved

For every integer \(n \ge 1\) and every doubly stochastic real \(n \times n\) matrix \(A\) (nonnegative entries, every row and every column summing to \(1\)), the permanent of \(A\) is at least \(n!/n^n\).

public theorem van_der_waerden_permanent {n : ℕ} (hn : 0 < n)
    (A : Matrix (Fin n) (Fin n) ℝ)
    (hA : A ∈ doublyStochastic ℝ (Fin n)) :
    ((n.factorial : ℝ) / (n : ℝ) ^ n) ≤ A.permanent

Sources

• G. P. Egorychev, Adv. Math. 42 (1981), 299-305, DOI 10.1016/0001-8708(81)90044-X; D. I. Falikman, Math. Notes 29 (1981), 475-479, DOI 10.1007/BF01163285.

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.