Birkhoff decomposition of a capped probability vector

Rows in a fixed support repeat the probability vector. The remaining rows distribute its complement so that the matrix is doubly stochastic. Birkhoff's theorem then expresses the original vector as a mixture of permutation images of the fixed support.

This uses Mathlib's Birkhoff--von Neumann theorem, formalized by Bhavik Mehta in Mathlib.Analysis.Convex.Birkhoff.

theorem Algebraic.Cutwidth.Extractor.Internal.exists_permutation_flat_mixture {α : Type u_1} [Fintype α] (S : Finset α) (positive : 0 < S.card) (small : S.card < Fintype.card α) (p : α → ℝ) (nonnegative : ∀ (x : α), 0 ≤ p x) (mass : ∑ x : α, p x = 1) (cap : ∀ (x : α), ↑S.card * p x ≤ 1) : ∃ (w : Equiv.Perm α → ℝ), (∀ (σ : Equiv.Perm α), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm α, w σ = 1 ∧ ∀ (x : α), p x = ∑ σ : Equiv.Perm α, w σ * if x ∈ Finset.image (⇑σ) S then (↑S.card)⁻¹ else 0