English
Let M be a doubly stochastic matrix of size n with entries in a field R. Then M can be written as a convex combination of permutation matrices. More precisely, there exists a function w from the permutation group on n to R with w(σ) ≥ 0 for all σ, the sum over all σ of w(σ) equals 1, and M equals the sum over σ of w(σ) times the permutation matrix corresponding to σ.
Русский
Пусть M — двойственно стохастическая матрица размера n над полем R. Тогда M является выпуклой комбинацией перестановочных матриц. Точнее, существует отображение w: Perm(n) → R, такое что ∀σ w(σ) ≥ 0, ∑σ w(σ) = 1, и M = ∑σ w(σ) P_σ, где P_σ — перестановочная матрица, соответствующая σ.
LaTeX
$$$\\exists w : \\operatorname{Perm}(n) \\to \\mathbb{R},\\ (\\forall \\sigma,\\ w(\\sigma) \\ge 0) \\land (\\sum_{\\sigma} w(\\sigma) = 1) \\land (\\sum_{\\sigma} w(\\sigma)\\, P_{\\sigma} = M)$$$
Lean4
/-- 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 exists_eq_sum_perm_of_mem_doublyStochastic (hM : M ∈ doublyStochastic R n) :
∃ w : Equiv.Perm n → R, (∀ σ, 0 ≤ w σ) ∧ ∑ σ, w σ = 1 ∧ ∑ σ, w σ • σ.permMatrix R = M :=
by
rcases isEmpty_or_nonempty n
case inl => exact ⟨fun _ => 1, by simp, by simp, Subsingleton.elim _ _⟩
obtain ⟨w, hw1, hw3⟩ := doublyStochastic_sum_perm_aux M 1 (by simp) ⟨M, hM, by simp⟩
refine ⟨w, hw1, ?_, hw3⟩
inhabit n
have : ∑ j, ∑ σ : Equiv.Perm n, w σ • σ.permMatrix R default j = 1 :=
by
simp only [← smul_apply (m := n), ← Finset.sum_apply, hw3]
rw [sum_row_of_mem_doublyStochastic hM]
simpa [sum_comm (γ := n), Equiv.toPEquiv_apply] using this
