Row- and Column-stochastic matrices

A square matrix M is row-stochastic if all its entries are non-negative and M *ᵥ 1 = 1. Likewise, M is column-stochastic if all its entries are non-negative and 1 ᵥ* M = 1. This file defines these concepts and provides basic API for them.

Note that doubly stochastic matrices (i.e. matrices that are both row- and column-stochastic) are defined in Mathlib/Analysis/Convex/DoublyStochasticMatrix.lean.

Main definitions

• rowStochastic: row-stochastic matrices indexed by n with entries in R, as a submonoid of Matrix n n R.
• colStochastic R n: column-stochastic matrices indexed by n with entries in R, as a submonoid of Matrix n n R.

def Matrix.rowStochastic (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 row stochastic iff all entries are nonnegative, and right multiplication by the vector of all 1s gives the vector of all 1s.

Equations

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

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

theorem Matrix.mem_rowStochastic_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 ∈ rowStochastic R n ↔ (∀ (i j : n), 0 ≤ M i j) ∧ ∀ (i : n), ∑ j : n, M i j = 1

A square matrix is row stochastic if each element is non-negative and row sums to one.

theorem Matrix.nonneg_of_mem_rowStochastic {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 ∈ rowStochastic R n) {i j : n} : 0 ≤ M i j

Every entry of a row stochastic matrix is nonnegative.

theorem Matrix.sum_row_of_mem_rowStochastic {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 ∈ rowStochastic R n) (i : n) : ∑ j : n, M i j = 1

Each row sum of a row stochastic matrix is 1.

theorem Matrix.one_vecMul_of_mem_rowStochastic {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 ∈ rowStochastic R n) : M.mulVec 1 = 1

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

theorem Matrix.le_one_of_mem_rowStochastic {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 ∈ rowStochastic R n) {i j : n} : M i j ≤ 1

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

theorem Matrix.nonneg_vecMul_of_mem_rowStochastic {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} (hM : M ∈ rowStochastic R n) (hx : ∀ (i : n), 0 ≤ x i) (j : n) : 0 ≤ vecMul x M j

Left multiplication of a row stochastic matrix by a non-negative vector gives a non-negative vector

theorem Matrix.nonneg_mulVec_of_mem_rowStochastic {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} (hM : M ∈ rowStochastic R n) (hx : ∀ (i : n), 0 ≤ x i) (j : n) : 0 ≤ M.mulVec x j

Right multiplication of a row stochastic matrix by a non-negative vector gives a non-negative vector

theorem Matrix.vecMul_dotProduct_one_eq_one_rowStochastic {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} (hM : M ∈ rowStochastic R n) (hx : x ⬝ᵥ 1 = 1) : vecMul x M ⬝ᵥ 1 = 1

Left left-multiplication by row stochastic preserves ℓ₁ norm

theorem Matrix.convex_rowStochastic {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [Semiring R] [PartialOrder R] [IsOrderedRing R] : Convex R ↑(rowStochastic R n)

The set of row stochastic matrices is convex.

@[simp]

theorem Matrix.permMatrix_mem_rowStochastic {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 σ ∈ rowStochastic R n

Any permutation matrix is row stochastic.

def Matrix.colStochastic (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 column stochastic iff all entries are nonnegative, and left multiplication by the vector of all 1s gives the vector of all 1s.

Equations

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

theorem Matrix.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 ∈ colStochastic R n ↔ (∀ (i j : n), 0 ≤ M i j) ∧ vecMul 1 M = 1

theorem Matrix.mem_colStochastic_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 ∈ colStochastic R n ↔ (∀ (i j : n), 0 ≤ M i j) ∧ ∀ (j : n), ∑ i : n, M i j = 1

A matrix is column stochastic if each column sums to one.

theorem Matrix.nonneg_of_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} (hM : M ∈ colStochastic R n) {i j : n} : 0 ≤ M i j

Every entry of a column stochastic matrix is nonnegative.

theorem Matrix.sum_col_of_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} (hM : M ∈ colStochastic R n) (i : n) : ∑ j : n, M j i = 1

Each column sum of a column stochastic matrix is 1.

theorem Matrix.one_vecMul_of_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} (hM : M ∈ colStochastic R n) : vecMul 1 M = 1

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

theorem Matrix.le_one_of_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} (hM : M ∈ colStochastic R n) {i j : n} : M j i ≤ 1

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

theorem Matrix.nonneg_mulVec_of_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} {x : n → R} (hM : M ∈ colStochastic R n) (hx : ∀ (i : n), 0 ≤ x i) (j : n) : 0 ≤ M.mulVec x j

Right multiplication of a column stochastic matrix by a non-negative vector gives a non-negative vector.

theorem Matrix.nonneg_vecMul_of_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} {x : n → R} (hM : M ∈ colStochastic R n) (hx : ∀ (i : n), 0 ≤ x i) (j : n) : 0 ≤ vecMul x M j

Left multiplication of a column stochastic matrix by a non-negative vector gives a non-negative vector.

theorem Matrix.mulVec_dotProduct_one_eq_one_colStochastic {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} (hM : M ∈ colStochastic R n) (hx : 1 ⬝ᵥ x = 1) : 1 ⬝ᵥ M.mulVec x = 1

Left left-multiplication by column stochastic preserves ℓ₁ norm

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

Applying a column-stochastic matrix to a vector preserves its sum.

theorem Matrix.convex_colStochastic {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [Semiring R] [PartialOrder R] [IsOrderedRing R] : Convex R ↑(colStochastic R n)

The set of column stochastic matrices is convex.

@[simp]

theorem Matrix.permMatrix_mem_colStochastic {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 σ ∈ colStochastic R n

Any permutation matrix is column stochastic.

theorem Matrix.transpose_mem_rowStochastic_iff_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.transpose ∈ rowStochastic R n ↔ M ∈ colStochastic R n

The transpose of a matrix is row stochastic matrix if it is column stochastic.

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

The transpose of a matrix is column stochastic matrix if it is row stochastic.

theorem Matrix.reindex_mem_rowStochastic {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 ∈ rowStochastic R n) : (reindex e₁ e₂) M ∈ rowStochastic R m

Reindexing a matrix preserves row-stochasticity.

theorem Matrix.reindex_mem_rowStochastic_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} : (reindex e₁ e₂) M ∈ rowStochastic R m ↔ M ∈ rowStochastic R n

Reindexing a matrix preserves row-stochasticity.

theorem Matrix.reindex_mem_colStochastic_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} : (reindex e₁ e₂) M ∈ colStochastic R m ↔ M ∈ colStochastic R n

Reindexing a matrix preserves column-stochasticity.

theorem Matrix.reindex_mem_colStochastic {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} : M ∈ colStochastic R n → (reindex e₁ e₂) M ∈ colStochastic R m

Reindexing a matrix preserves column-stochasticity.