Averaging flat sources and their lossless witnesses

A uniform source on P is exactly the uniform mixture of its K-element subsets when 0 < K ≤ P.card. Double counting proves this identity for arbitrary finite sums, and therefore for seeded test probabilities with all source and seed multiplicities retained.

Nonnegative normalized mixtures preserve a common test-discrepancy bound. Consequently, lossless witnesses for every K-subset extend to larger flat supports as an explicit mixture of witnesses. Each component is uniform on exactly K outputs conditional on each seed; its support may depend on the component and seed. The mixture keeps the original uniform seed.

These are finite averaging identities. The decomposition of arbitrary capped weights into flat sources is exists_flat_mixture_of_capped_weights in Strong.FlatMixture. Empty seed types retain the zero convention of seededTestProb.

theorem Algebraic.Cutwidth.Extractor.sum_powersetCard_sum {α : Type u_1} {M : Type u_2} [AddCommMonoid M] (P : Finset α) {K : ℕ} (positive : 0 < K) (f : α → M) : ∑ S ∈ Finset.powersetCard K P, ∑ x ∈ S, f x = (P.card - 1).choose (K - 1) • ∑ x ∈ P, f x

Double counting over positive-size subsets, valid in any additive commutative monoid. The support may be empty or smaller than K.

theorem Algebraic.Cutwidth.Extractor.powersetCard_average {α : Type u_1} (P : Finset α) {K : ℕ} (positive : 0 < K) (size : K ≤ P.card) (f : α → ℝ) : (∑ S ∈ Finset.powersetCard K P, (∑ x ∈ S, f x) / ↑K) / ↑(Finset.powersetCard K P).card = (∑ x ∈ P, f x) / ↑P.card

Averaging the uniform averages of all K-subsets gives the uniform average over the original support.

theorem Algebraic.Cutwidth.Extractor.seededTestProb_powersetCard {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype Seed] (C : α → Seed → Ω) (P : Finset α) {K : ℕ} (positive : 0 < K) (size : K ≤ P.card) (T : Finset (Seed × Ω)) : seededTestProb (fun (x : ↥P) => C ↑x) T = (∑ S : ↥(Finset.powersetCard K P), seededTestProb (fun (x : ↥↑S) => C ↑x) T) / ↑(Finset.powersetCard K P).card

Every seeded test has the same probability under a flat support as under the uniform mixture of its K-subsets.

theorem Algebraic.Cutwidth.Extractor.seededMixtureTestProb_sub_le {ι : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype ι] [Fintype Seed] {Source : ι → Type u_4} {Target : ι → Type u_5} [(i : ι) → Fintype (Source i)] [(i : ι) → Fintype (Target i)] (w : ι → ℝ) (C : (i : ι) → Source i → Seed → Ω) (G : (i : ι) → Target i → Seed → Ω) (nonnegative : ∀ (i : ι), 0 ≤ w i) (mass : ∑ i : ι, w i = 1) {ε : ℝ} (close : ∀ (i : ι) (T : Finset (Seed × Ω)), |seededTestProb (C i) T - seededTestProb (G i) T| ≤ ε) (T : Finset (Seed × Ω)) : |seededMixtureTestProb w C T - seededMixtureTestProb w G T| ≤ ε

A common error bound on all seeded tests is preserved by a supplied nonnegative normalized mixture, using the same weights on both sides.

theorem Algebraic.Cutwidth.Extractor.exists_flat_mixture_of_exact_size {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype Seed] (C : α → Seed → Ω) (P : Finset α) {K : ℕ} (positive : 0 < K) (size : K ≤ P.card) {ε : ℝ} (lossless : ∀ S ⊆ P, S.card = K → ∃ (g : Seed → ↥S ↪ Ω), ∀ (T : Finset (Seed × Ω)), |seededTestProb (fun (x : ↥S) => C ↑x) T - seededTestProb (fun (x : ↥S) (y : Seed) => (g y) x) T| ≤ ε) : ∃ (g : (S : ↥(Finset.powersetCard K P)) → Seed → ↥↑S ↪ Ω), ∀ (T : Finset (Seed × Ω)), |seededTestProb (fun (x : ↥P) => C ↑x) T - seededMixtureTestProb (fun (x : ↥(Finset.powersetCard K P)) => (↑(Finset.powersetCard K P).card)⁻¹) (fun (S : ↥(Finset.powersetCard K P)) (x : ↥↑S) (y : Seed) => (g S y) x) T| ≤ ε

Witnesses on every K-subset give a mixture of K-flat conditional outputs for the larger support. The comparison keeps every seed unchanged.