# 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

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' := ⋯ }

## Instances For

Every entry of a doubly stochastic matrix is nonnegative.

Each row sum of a doubly stochastic matrix is 1.

Each column sum of a doubly stochastic matrix is 1.

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

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

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

The set of doubly stochastic matrices is convex.

Any permutation matrix is doubly stochastic.

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.