Doubly stochastic matrices

Main definitions

• doublyStochastic: a square matrix is doubly stochastic if all entries are nonnegative, and left or right multiplication by the vector of all 1s gives the vector of all 1s. Equivalently, all row and column sums are equal to 1.

Main statements

• convex_doublyStochastic: The set of doubly stochastic matrices is convex.
• permMatrix_mem_doublyStochastic: Any permutation matrix is doubly stochastic.

TODO

Define the submonoids of row-stochastic and column-stochastic matrices. Show that the submonoid of doubly stochastic matrices is the meet of them, or redefine it as such.

Tags

Doubly stochastic, Birkhoff's theorem, Birkhoff-von Neumann theorem

def doublyStochastic (R : Type u_3) (n : Type u_4) [Fintype n] [DecidableEq n] [Semiring R] [PartialOrder R] [IsOrderedRing R] : Submonoid (Matrix n n R)

A square matrix is doubly stochastic iff all entries are nonnegative, and left or right multiplication by the vector of all 1s gives the vector of all 1s.

Equations

• doublyStochastic R n = { carrier := {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M.mulVec 1 = 1 ∧ Matrix.vecMul 1 M = 1}, mul_mem' := ⋯, one_mem' := ⋯ }

theorem mem_doublyStochastic {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [Semiring R] [PartialOrder R] [IsOrderedRing R] {M : Matrix n n R} : M ∈ doublyStochastic R n ↔ (∀ (i j : n), 0 ≤ M i j) ∧ M.mulVec 1 = 1 ∧ Matrix.vecMul 1 M = 1

theorem mem_doublyStochastic_iff_sum {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [Semiring R] [PartialOrder R] [IsOrderedRing R] {M : Matrix n n R} : M ∈ doublyStochastic R n ↔ (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = 1) ∧ ∀ (j : n), ∑ i : n, M i j = 1

theorem nonneg_of_mem_doublyStochastic {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [Semiring R] [PartialOrder R] [IsOrderedRing R] {M : Matrix n n R} (hM : M ∈ doublyStochastic R n) {i j : n} : 0 ≤ M i j

Every entry of a doubly stochastic matrix is nonnegative.

theorem sum_row_of_mem_doublyStochastic {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [Semiring R] [PartialOrder R] [IsOrderedRing R] {M : Matrix n n R} (hM : M ∈ doublyStochastic R n) (i : n) : ∑ j : n, M i j = 1

Each row sum of a doubly stochastic matrix is 1.

theorem sum_col_of_mem_doublyStochastic {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [Semiring R] [PartialOrder R] [IsOrderedRing R] {M : Matrix n n R} (hM : M ∈ doublyStochastic R n) (j : n) : ∑ i : n, M i j = 1

Each column sum of a doubly stochastic matrix is 1.

theorem mulVec_one_of_mem_doublyStochastic {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [Semiring R] [PartialOrder R] [IsOrderedRing R] {M : Matrix n n R} (hM : M ∈ doublyStochastic R n) : M.mulVec 1 = 1

A doubly stochastic matrix multiplied with the all-ones column vector is 1.

theorem one_vecMul_of_mem_doublyStochastic {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [Semiring R] [PartialOrder R] [IsOrderedRing R] {M : Matrix n n R} (hM : M ∈ doublyStochastic R n) : Matrix.vecMul 1 M = 1

The all-ones row vector multiplied with a doubly stochastic matrix is 1.

theorem le_one_of_mem_doublyStochastic {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [Semiring R] [PartialOrder R] [IsOrderedRing R] {M : Matrix n n R} (hM : M ∈ doublyStochastic R n) {i j : n} : M i j ≤ 1

Every entry of a doubly stochastic matrix is less than or equal to 1.

theorem convex_doublyStochastic {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [Semiring R] [PartialOrder R] [IsOrderedRing R] : Convex R ↑(doublyStochastic R n)

The set of doubly stochastic matrices is convex.

theorem permMatrix_mem_doublyStochastic {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [Semiring R] [PartialOrder R] [IsOrderedRing R] {σ : Equiv.Perm n} : Equiv.Perm.permMatrix R σ ∈ doublyStochastic R n

Any permutation matrix is doubly stochastic.

theorem exists_mem_doublyStochastic_eq_smul_iff {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [Semifield R] [LinearOrder R] [IsStrictOrderedRing R] {M : Matrix n n R} {s : R} (hs : 0 ≤ s) : (∃ M' ∈ doublyStochastic R n, M = s • M') ↔ (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s

A matrix is s times a doubly stochastic matrix iff all entries are nonnegative, and all row and column sums are equal to s.

This lemma is useful for the proof of Birkhoff's theorem - in particular because it allows scaling by nonnegative factors rather than positive ones only.