noncomputable def BregmanMinc.rowSum (n : ℕ) (A : Matrix (Fin n) (Fin n) ℝ) (i : Fin n) : ℕ

The row sum $d_i$ of row $i$ of a $0/1$-matrix $A$: the number of columns $j$ with $A_{ij}=1$.

theorem BregmanMinc.bregman_minc_log_bound (n : ℕ) (A : Matrix (Fin n) (Fin n) ℝ) (hA : ∀ (i j : Fin n), A i j = 0 ∨ A i j = 1) (hP : 0 < A.permanent) : Real.log A.permanent ≤ ∑ i : Fin n, 1 / ↑(rowSum n A i) * Real.log ↑(rowSum n A i).factorial

Logarithmic form of the Brégman-Minc inequality (Theorem 10.2.1): for a $0/1$-matrix $A$ with positive permanent, $\log \operatorname{per} A \le \sum_i \frac{1}{d_i} \log(d_i!)$.

theorem BregmanMinc.bregman_minc_inequality (n : ℕ) (A : Matrix (Fin n) (Fin n) ℝ) (hA : ∀ (i j : Fin n), A i j = 0 ∨ A i j = 1) : A.permanent ≤ ∏ i : Fin n, ↑(rowSum n A i).factorial ^ (1 / ↑(rowSum n A i))

The Brégman-Minc inequality (Theorem 10.2.1): for any $n \times n$ matrix $A$ with $0/1$ entries, $\operatorname{per} A \le \prod_i (d_i!)^{1/d_i}$ where $d_i$ is the $i$-th row sum.

noncomputable def BregmanMinc.rowSumGen {V : Type u_1} [Fintype V] [DecidableEq V] (A : Matrix V V ℝ) (i : V) : ℕ

Row sum of a $0/1$-matrix indexed by an arbitrary finite type $V$: the number of $j$ with $A_{ij}=1$.

theorem BregmanMinc.bregman_minc_inequality_gen {V : Type u_1} [Fintype V] [DecidableEq V] (A : Matrix V V ℝ) (hA : ∀ (i j : V), A i j = 0 ∨ A i j = 1) : A.permanent ≤ ∏ i : V, ↑(rowSumGen A i).factorial ^ (1 / ↑(rowSumGen A i))

Brégman-Minc inequality for matrices indexed by an arbitrary finite type $V$: $\operatorname{per} A \le \prod_{i \in V} (d_i!)^{1/d_i}$ for $0/1$-matrices $A$.

noncomputable def KahnLovasz.numPerfectMatchings {V : Type u_1} (G : SimpleGraph V) : ℕ

The number of perfect matchings of a simple graph $G$.

theorem KahnLovasz.matching_sq_le_permanent {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ↑(numPerfectMatchings G) ^ 2 ≤ (SimpleGraph.adjMatrix ℝ G).permanent

Bridge step toward the Kahn-Lovász bound: the squared count of perfect matchings is at most the permanent of the adjacency matrix, i.e. $|\mathcal{M}(G)|^2 \le \operatorname{per}(A_G)$.

theorem KahnLovasz.adjMatrix_rowSumGen_eq_degree {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) : BregmanMinc.rowSumGen (SimpleGraph.adjMatrix ℝ G) v = G.degree v

The row sum of the adjacency matrix of $G$ at vertex $v$ equals the graph-theoretic degree $\deg_G(v)$.

theorem KahnLovasz.kahn_lovasz_inequality {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ↑(numPerfectMatchings G) ≤ ∏ v : V, ↑(G.degree v).factorial ^ (1 / (2 * ↑(G.degree v)))

The Kahn-Lovász inequality (Corollary 10.2.2): the number of perfect matchings of $G$ satisfies $|\mathcal{M}(G)| \le \prod_v (\deg(v)!)^{1/(2\deg(v))}$.