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.

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.

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 doublyStochastic_eq_rowStochastic_inf_colStochastic {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [Semiring R] [PartialOrder R] [IsOrderedRing R] : doublyStochastic R n = Matrix.rowStochastic R n ⊓ Matrix.colStochastic R n

A matrix is doubly stochastic if and only if it is both row and column stochastic.

theorem mem_doublyStochastic_iff_mem_rowStochastic_and_mem_colStochastic {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 ↔ M ∈ Matrix.rowStochastic R n ∧ M ∈ Matrix.colStochastic R n

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.

@[simp]

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 transpose_mem_doublyStochastic_iff {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [Semiring R] [PartialOrder R] [IsOrderedRing R] {M : Matrix n n R} : M.transpose ∈ doublyStochastic R n ↔ M ∈ doublyStochastic R n

A matrix is doubly stochastic iff its transpose is doubly stochastic

theorem reindex_mem_doublyStochastic {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [Semiring R] [PartialOrder R] [IsOrderedRing R] {m : Type u_3} [Fintype m] [DecidableEq m] {M : Matrix n n R} {e₁ e₂ : n ≃ m} (hM : M ∈ doublyStochastic R n) : (Matrix.reindex e₁ e₂) M ∈ doublyStochastic R m

Reindexing a matrix preserves double stochasticity.

theorem reindex_mem_doublyStochastic_iff {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [Semiring R] [PartialOrder R] [IsOrderedRing R] {m : Type u_3} [Fintype m] [DecidableEq m] {M : Matrix n n R} {e₁ e₂ : n ≃ m} : (Matrix.reindex e₁ e₂) M ∈ doublyStochastic R m ↔ M ∈ doublyStochastic R n

Reindexing a matrix preserves double stochasticity.

theorem sum_mulVec_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} {x : n → R} (hA : M ∈ doublyStochastic R n) : ∑ i : n, M.mulVec x i = ∑ i : n, x i

Applying a doubly stochastic matrix to a vector preserves its sum.

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.