Mixture weights on fixed-cardinality supports

The cap and normalization imply that the requested support size fits the ambient finite type. At full cardinality every coordinate is uniform. At smaller cardinality, the permutation mixture from Birkhoff is pushed forward to the finite type of supports, adding weights when images coincide.

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