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.
• extremePoints_doublyStochastic: The set of extreme points of the doubly stochastic matrices is the set of permutation matrices.

TODO

• 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] [Field R] [LinearOrder R] [IsStrictOrderedRing 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 a 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] [Field R] [LinearOrder R] [IsStrictOrderedRing 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.

theorem extremePoints_doublyStochastic {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [Field R] [LinearOrder R] [IsStrictOrderedRing R] : Set.extremePoints R ↑(doublyStochastic R n) = {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x}

The set of extreme points of the doubly stochastic matrices is the set of permutation matrices.

theorem Matrix.l2_opNorm_le_one_of_mem_doublyStochastic {n : Type u_2} [Fintype n] [DecidableEq n] {M : Matrix n n ℝ} (hM : M ∈ doublyStochastic ℝ n) : ‖M‖ ≤ 1