# 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`

.