Nonnegative sums of permutation matrices

Each permutation's weight bounds the entries on its diagonal in a nonnegative weighted sum of permutation matrices. This lets support arguments recover a whole permutation diagonal from a positive weight. A positively weighted combination of permutations, each lying in the support of a matrix K and together covering it, has the zero pattern of K.

theorem Equiv.Perm.permMatrix_nonneg {n : Type u_1} {R : Type u_2} [DecidableEq n] [Zero R] [One R] [Preorder R] [ZeroLEOneClass R] (σ : Perm n) (i j : n) : 0 ≤ permMatrix R σ i j

Every entry of a permutation matrix is nonnegative.

theorem Matrix.weight_le_sum_permMatrix {n : Type u_1} {R : Type u_2} [DecidableEq n] [Semiring R] [PartialOrder R] [IsOrderedRing R] (s : Finset (Equiv.Perm n)) (w : Equiv.Perm n → R) (hw : ∀ τ ∈ s, 0 ≤ w τ) {σ : Equiv.Perm n} (hσ : σ ∈ s) (k : n) : w σ ≤ (∑ τ ∈ s, w τ • Equiv.Perm.permMatrix R τ) k (σ k)

A nonnegative weighted sum of permutation matrices has entries on each included permutation diagonal at least as large as that permutation's weight.

theorem Matrix.sum_smul_permMatrix_apply_eq_zero_iff {n : Type u_1} {α : Type u_2} {R : Type u_3} [DecidableEq n] [Zero α] [Semiring R] [PartialOrder R] [IsOrderedRing R] {K : Matrix n n α} {s : Finset (Equiv.Perm n)} {w : Equiv.Perm n → R} (hw : ∀ σ ∈ s, 0 < w σ) (hsub : ∀ σ ∈ s, ∀ (k : n), K k (σ k) ≠ 0) (hcover : ∀ (i j : n), K i j ≠ 0 → ∃ σ ∈ s, σ i = j) (i j : n) : (∑ σ ∈ s, w σ • Equiv.Perm.permMatrix R σ) i j = 0 ↔ K i j = 0

A combination of permutation matrices over a set s of permutations with positive weights w, each of which stays inside the support of K and which together cover the support, has the zero pattern of K.