Chapter 37 lemma: Bregman-Minc permanent upper bound

Proved

BookSixth.permanent_bregman_minc_upper

by WillR · Sep 17, 2026 · Mathlib c5ea003 (Lean v4.30.0)

proofs-from-the-booksixth-edition

Bregman's theorem (Minc conjecture): the permanent of a $0$ - $1$ matrix with row sums $r_i$ is at most $\prod_i (r_i!)^{1/r_i}$ . This is the permanent estimate behind the upper counting bound of Chapter 37, Theorem 2.

Preamble

import Mathlib
import Definitions.Def_BookSixth
open scoped BigOperators
open BookSixth

Formal statement

theorem BookSixth.permanent_bregman_minc_upper (n : ℕ) (M : Matrix (Fin n) (Fin n) ℝ) (r : Fin n → ℕ) (h01 : ∀ i j, M i j = 0 ∨ M i j = 1) (hrow : ∀ i, ∑ j, M i j = (r i : ℝ)) :
    Matrix.permanent M ≤ ∏ i, ((r i).factorial : ℝ) ^ ((1 : ℝ) / (r i : ℝ)) := by sorry

Source

Aigner and Ziegler, Proofs from THE BOOK, Sixth Edition (2018), Chapter 37, permanent upper bound used for Theorem 2, p. 266. https://doi.org/10.1007/978-3-662-57265-8_37

View graph