Birkhoff's theorem

Main statements

• doublyStochastic_eq_sum_perm: If M is a doubly stochastic matrix, then it is a convex combination of permutation matrices.
• doublyStochastic_eq_convexHull_perm: The set of doubly stochastic matrices is the convex hull of the permutation matrices.

TODO

• Show that the extreme points of doubly stochastic matrices are the permutation matrices.
• Show that for x y : n → R, x is majorized by y if and only if there is a doubly stochastic matrix M such that M *ᵥ y = x.

Tags

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

theorem exists_eq_sum_perm_of_mem_doublyStochastic {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [LinearOrderedField R] {M : Matrix n n R} (hM : M ∈ doublyStochastic R n) : ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ = 1 ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

If M is a doubly stochastic matrix, then it is an convex combination of permutation matrices. Note doublyStochastic_eq_convexHull_permMatrix shows doublyStochastic n is exactly the convex hull of the permutation matrices, and this lemma is instead most useful for accessing the coefficients of each permutation matrices directly.

theorem doublyStochastic_eq_convexHull_permMatrix {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [LinearOrderedField R] : ↑(doublyStochastic R n) = (convexHull R) {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x}

Birkhoff's theorem The set of doubly stochastic matrices is the convex hull of the permutation matrices. Note exists_eq_sum_perm_of_mem_doublyStochastic gives a convex weighting of each permutation matrix directly. To show doublyStochastic n is convex, use convex_doublyStochastic.