Documentation

Mathlib.Data.Matrix.DoublyStochastic

Doubly stochastic matrices #

Main definitions #

Main statements #

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

source
def doublyStochastic (R : Type u_3) (n : Type u_4) [Fintype n] [DecidableEq n] [OrderedSemiring 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
Instances For
    source
    theorem mem_doublyStochastic {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [OrderedSemiring 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
    source
    theorem mem_doublyStochastic_iff_sum {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [OrderedSemiring 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
    source
    theorem nonneg_of_mem_doublyStochastic {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [OrderedSemiring 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.

    source
    theorem sum_row_of_mem_doublyStochastic {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [OrderedSemiring 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.

    source
    theorem sum_col_of_mem_doublyStochastic {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [OrderedSemiring 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.

    source
    theorem mulVec_one_of_mem_doublyStochastic {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [OrderedSemiring 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.

    source
    theorem one_vecMul_of_mem_doublyStochastic {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [OrderedSemiring 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.

    source
    theorem le_one_of_mem_doublyStochastic {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [OrderedSemiring 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.

    source
    theorem convex_doublyStochastic {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [OrderedSemiring R] :
    Convex R ↑(doublyStochastic R n)

    The set of doubly stochastic matrices is convex.

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

    Any permutation matrix is doubly stochastic.

    source
    theorem exists_mem_doublyStochastic_eq_smul_iff {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [LinearOrderedSemifield 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.