Decomposing a capped finite source into flat sources

A nonnegative probability vector with every point mass at most 1 / K is exactly a normalized nonnegative mixture of uniform K-element supports. The weights are indexed by those supports, so repeated components have already been combined. The hypotheses imply that the finite ambient type has at least K elements; no separate cardinality assumption is needed.

The proof completes the probability vector to a doubly stochastic matrix and applies the Birkhoff--von Neumann theorem from Mathlib, formalized by Bhavik Mehta in Mathlib.Analysis.Convex.Birkhoff. This is a finite existence theorem, without a computational claim for the mixture weights.

theorem Algebraic.Cutwidth.Extractor.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

A normalized source capped at 1 / K is an exact convex mixture of uniform supports of cardinality K. The positive threshold excludes division by zero; empty ambient types cannot satisfy normalization.