English
The set of doubly stochastic matrices is exactly the convex hull of the permutation matrices. In particular, every doubly stochastic matrix is a convex combination of permutation matrices.
Русский
Множество двойственно стохастических матриц является точной выпуклой оболочкой перестановочных матриц. В частности, любая двойственно стохастическая матрица является выпуклой комбинацией перестановочных матриц.
LaTeX
$$$\\text{doublyStochastic } R n \;=\\; \\operatorname{convexHull}_R\\{\\sigma.student{permMatrix} R \\mid \\sigma : \\operatorname{Perm}(n)\\}$$$
Lean4
/-- **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 doublyStochastic_eq_convexHull_permMatrix :
doublyStochastic R n = convexHull R {σ.permMatrix R | σ : Equiv.Perm n} :=
by
refine (convexHull_min ?g1 convex_doublyStochastic).antisymm' fun M hM => ?g2
case g1 =>
rintro x ⟨h, rfl⟩
exact permMatrix_mem_doublyStochastic
case g2 =>
obtain ⟨w, hw1, hw2, hw3⟩ := exists_eq_sum_perm_of_mem_doublyStochastic hM
exact mem_convexHull_of_exists_fintype w (·.permMatrix R) hw1 hw2 (by simp) hw3
