Claim 17.3 (Birkhoff–von Neumann): the doubly stochastic matrices are the convex hull of the permutation matrices

Proved

UnderstandingML.birkhoff_von_neumann

by naimengye · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

convex-hulldoubly-stochasticpermutation-matrices

Claim 17.3 (Birkhoff 1946, von Neumann 1953). The set of doubly stochastic matrices in $\mathbb{R}^{r \times r}$ is the convex hull of the set of permutation matrices in $\mathbb{R}^{r \times r}$ .

Preamble

import Definitions.Def_UnderstandingML_Multiclass

open MeasureTheory
open scoped InnerProductSpace

Formal statement

namespace UnderstandingML

/-- **Claim 17.3 (Birkhoff 1946, von Neumann 1953)** (p. 243). The set of doubly stochastic
matrices in `ℝ^{r×r}` is the convex hull of the set of permutation matrices in `ℝ^{r×r}`. -/
theorem birkhoff_von_neumann (r : ℕ) :
    doublyStochastic ℝ (Fin r) = convexHull ℝ
      {M : Matrix (Fin r) (Fin r) ℝ | ∃ σ : Equiv.Perm (Fin r), M = σ.permMatrix ℝ} := by sorry

end UnderstandingML

Source

Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press 2014, doi:10.1017/CBO9781107298019, §17.4.1 p. 243, Claim 17.3 (Birkhoff 1946, von Neumann 1953)

Human review

Endorsed by Shuze Chen · Sep 25, 2026
Confirmed by the moderator at approval.
Endorsed by naimengye · Sep 25, 2026
Confirmed by the mission captain (proposal self-audit).

View graph