Brégman's theorem on permanents of (0,1)-matrices

For an n × n (0,1)-matrix with non-zero row sums rᵢ, per A ≤ ∏ᵢ (rᵢ!)^(1/rᵢ) (Brégman 1973, conjectured by Minc; Theorem of the Day). Proof: Schrijver's induction in logarithmic form, P log P ≤ P Σᵢ log(rᵢ!)/rᵢ for P = per A (zero rows allowed), from a single Jensen inequality for x log x, the fibres of σ ↦ σ(i) (permanents of minors), the counts r_k − 1 and n − r_k over a fixed permutation, and log r + (n − r)F(r) + (r − 1)F(r − 1) = nF(r).

Main results

• Bregman.log_bound: P log P ≤ P Σᵢ log(rᵢ!)/rᵢ for every (0,1)-matrix (zero rows allowed)
• Bregman.permanent_le: Brégman: per A ≤ ∏ᵢ (rᵢ!)^(1/rᵢ)

References

• R. Whitty, Theorem of the Day, «Bregman's Theorem» (CombinatorialTheory/Bregman).
• L. M. Brégman, Some properties of nonnegative matrices and their permanents, Soviet Math. Dokl. 14 (1973); A. Schrijver, A short proof of Minc's conjecture, J. Combin. Theory Ser. A 25 (1978) 80–83.

Fibres of σ ↦ σ i and minors

def Bregman.adm {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (A : I → J → ℕ) : Finset (I ≃ J)

The admissible bijections of a (0,1)-matrix.

Equations

• Bregman.adm A = {σ : I ≃ J | ∀ (i : I), A i (σ i) = 1}

def Bregman.minor {I : Type u_1} {J : Type u_2} (A : I → J → ℕ) (i : I) (j : J) : { k : I // k ≠ i } → { l : J // l ≠ j } → ℕ

The minor of A obtained by deleting row i and column j.

Equations

• Bregman.minor A i j k l = A ↑k ↑l

def Bregman.extendEquiv {I : Type u_1} {J : Type u_2} [DecidableEq I] [DecidableEq J] (i : I) (j : J) (τ : { k : I // k ≠ i } ≃ { l : J // l ≠ j }) : I ≃ J

Extend a bijection of the minors to a bijection sending i to j.

Equations

• Bregman.extendEquiv i j τ = (Equiv.optionSubtypeNe i).symm.trans (τ.optionCongr.trans (Equiv.optionSubtypeNe j))

theorem Bregman.extendEquiv_self {I : Type u_1} {J : Type u_2} [DecidableEq I] [DecidableEq J] (i : I) (j : J) (τ : { k : I // k ≠ i } ≃ { l : J // l ≠ j }) : (extendEquiv i j τ) i = j

theorem Bregman.extendEquiv_of_ne {I : Type u_1} {J : Type u_2} [DecidableEq I] [DecidableEq J] (i : I) (j : J) (τ : { k : I // k ≠ i } ≃ { l : J // l ≠ j }) (k : I) (hk : k ≠ i) : (extendEquiv i j τ) k = ↑(τ ⟨k, hk⟩)

def Bregman.restrictEquiv {I : Type u_1} {J : Type u_2} (σ : I ≃ J) (i : I) (j : J) (h : σ i = j) : { k : I // k ≠ i } ≃ { l : J // l ≠ j }

Restrict a bijection with σ i = j to the minors.

Equations

• Bregman.restrictEquiv σ i j h = σ.subtypeEquiv ⋯

theorem Bregman.fiber_card {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (A : I → J → ℕ) (hA : ∀ (i : I) (j : J), A i j ≤ 1) (i : I) (j : J) : {σ ∈ adm A | σ i = j}.card = A i j * (adm (minor A i j)).card

(F1) The fibre {σ admissible | σ i = j} has a_{ij} * per(minor) elements.

theorem Bregman.sum_adm_eq {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (A : I → J → ℕ) (hA : ∀ (i : I) (j : J), A i j ≤ 1) (i : I) (G : J → ℝ) : ∑ σ ∈ adm A, G (σ i) = ∑ j : J, ↑(A i j) * ↑(adm (minor A i j)).card * G j

(F3) Summing over admissible σ a function of σ i: group by the fibres.

theorem Bregman.card_adm_eq {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (A : I → J → ℕ) (hA : ∀ (i : I) (j : J), A i j ≤ 1) (i : I) : ↑(adm A).card = ∑ j : J, ↑(A i j) * ↑(adm (minor A i j)).card

(F2) The number of admissible bijections splits along row i.

theorem Bregman.card_subtype_ne {I : Type u_1} [Fintype I] [DecidableEq I] (i : I) : Fintype.card { k : I // k ≠ i } = Fintype.card I - 1

Analytic lemmas

noncomputable def Bregman.Phi (x : ℝ) : ℝ

Φ(x) = x log x.

Equations

• Bregman.Phi x = x * Real.log x

noncomputable def Bregman.F (m : ℕ) : ℝ

F(m) = log(m!) / m.

Equations

• Bregman.F m = Real.log ↑m.factorial / ↑m

theorem Bregman.mul_F (m : ℕ) : ↑m * F m = Real.log ↑m.factorial

theorem Bregman.L2 (r : ℕ) (hr : 1 ≤ r) (N : ℝ) : Real.log ↑r + (N - ↑r) * F r + (↑r - 1) * F (r - 1) = N * F r

(L2) log r + (N - r) F(r) + (r - 1) F(r - 1) = N F(r).

theorem Bregman.jensen {ι : Type u_1} (t : Finset ι) (a c : ι → ℝ) (ha : ∀ j ∈ t, 0 ≤ a j) (hc : ∀ j ∈ t, 0 ≤ c j) (r : ℝ) (hr : 0 < r) (hsum : ∑ j ∈ t, a j = r) (hP : 0 < ∑ j ∈ t, a j * c j) : Phi (∑ j ∈ t, a j * c j) ≤ (∑ j ∈ t, a j * c j) * Real.log r + ∑ j ∈ t, a j * Phi (c j)

(J) Jensen for x log x with weights a_j / r.

Row counts

theorem Bregman.row_count {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [DecidableEq I] (A : I → J → ℕ) (hA : ∀ (i : I) (j : J), A i j ≤ 1) (σ : I ≃ J) (hσ : ∀ (i : I), A i (σ i) = 1) (k : I) : ∑ i ∈ Finset.univ.erase k, F (∑ j : J, A k j - A k (σ i)) = (↑(Fintype.card I) - ↑(∑ j : J, A k j)) * F (∑ j : J, A k j) + (↑(∑ j : J, A k j) - 1) * F (∑ j : J, A k j - 1)

(C2) For an admissible σ and a row k: Σ_{i ≠ k} F(r_k - a_{k,σ i}) = (N - r_k) F(r_k) + (r_k - 1) F(r_k - 1).

theorem Bregman.minor_sum_F {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (A : I → J → ℕ) (i : I) (j : J) : ∑ k : { k : I // k ≠ i }, F (∑ l : { l : J // l ≠ j }, minor A i j k l) = ∑ k ∈ Finset.univ.erase i, F (∑ l : J, A k l - A k j)

Sum of F over the rows of a minor.

noncomputable def Bregman.Gfun {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [DecidableEq I] (A : I → J → ℕ) (i : I) (j : J) : ℝ

The i-th row bound after the induction hypothesis.

Equations

• Bregman.Gfun A i j = ∑ k ∈ Finset.univ.erase i, Bregman.F (∑ l : J, A k l - A k j)

theorem Bregman.double_sum {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (A : I → J → ℕ) (hA : ∀ (i : I) (j : J), A i j ≤ 1) : ∑ i : I, ∑ σ ∈ adm A, Gfun A i (σ i) = ↑(adm A).card * ∑ k : I, ((↑(Fintype.card I) - ↑(∑ j : J, A k j)) * F (∑ j : J, A k j) + (↑(∑ j : J, A k j) - 1) * F (∑ j : J, A k j - 1))

The double sum over admissible bijections and rows.

The logarithmic bound (Schrijver)

theorem Bregman.log_bound_aux (n : ℕ) {I : Type u} {J : Type v} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (A : I → J → ℕ) : (∀ (i : I) (j : J), A i j ≤ 1) → Fintype.card I = n → Phi ↑(adm A).card ≤ ↑(adm A).card * ∑ i : I, F (∑ j : J, A i j)

Induction on the number of rows (arbitrary column type J).

theorem Bregman.log_bound {I : Type u} {J : Type v} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (A : I → J → ℕ) (hA : ∀ (i : I) (j : J), A i j ≤ 1) : ↑(adm A).card * Real.log ↑(adm A).card ≤ ↑(adm A).card * ∑ i : I, Real.log ↑(∑ j : J, A i j).factorial / ↑(∑ j : J, A i j)

Logarithmic Brégman bound (Schrijver; zero rows allowed): for the number P of bijections I ≃ J picking a 1 in every row of the (0,1)-matrix A, P log P ≤ P Σᵢ log(rᵢ!)/rᵢ.

Brégman's theorem

theorem Bregman.permanent_eq_card {n : ℕ} (A : Matrix (Fin n) (Fin n) ℕ) (hA : ∀ (i j : Fin n), A i j ≤ 1) : A.permanent = (adm A).card

The permanent of a (0,1)-matrix counts the admissible bijections.

theorem Bregman.permanent_le (n : ℕ) (A : Matrix (Fin n) (Fin n) ℕ) (hA : ∀ (i j : Fin n), A i j ≤ 1) : ↑A.permanent ≤ ∏ i : Fin n, ↑(∑ j : Fin n, A i j).factorial ^ (1 / ↑(∑ j : Fin n, A i j))

Brégman's theorem (Minc's conjecture). For an n × n (0,1)-matrix A with row sums rᵢ = Σⱼ A i j, the permanent satisfies per A ≤ ∏ᵢ (rᵢ!)^(1/rᵢ). The classical statement asks for non-zero row sums; none is needed here: a zero row makes per A = 0, and with 1/0 = 0 its factor is (0!)^0 = 1.