Theorems · Theorem · linear algebra

exists_eq_sum_perm_of_mem_doublyStochastic

∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Field R] [inst_3 : LinearOrder R]
  [inst_4 : IsStrictOrderedRing R] {M : Matrix n n R},
  M ∈ doublyStochastic R n →
    ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ = 1 ∧ ∑ σ, 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.

Defined in

Mathlib.Analysis.Convex.Birkhoff

Cited by

1 results in Mathlib

Foundations

Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableEqFieldLinearOrderIsStrictOrderedRing