Subset averaging and preservation of test discrepancy

Every point of a finite support lies in the same number of its subsets of a fixed positive size. Double counting gives exact averaging over these subsets. Nonnegative normalized mixtures preserve a common test-discrepancy bound by the triangle inequality.

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

theorem Algebraic.Cutwidth.Extractor.Internal.seededTestProb_eq_sum {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] (C : α → Seed → Ω) (T : Finset (Seed × Ω)) : seededTestProb C T = (∑ x : α, ↑{y : Seed | (y, C x y) ∈ T}.card) / (↑(Fintype.card α) * ↑(Fintype.card Seed))

theorem Algebraic.Cutwidth.Extractor.Internal.seededTestProb_support_eq_sum {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype Seed] (C : α → Seed → Ω) (P : Finset α) (T : Finset (Seed × Ω)) : seededTestProb (fun (x : ↥P) => C ↑x) T = (∑ x ∈ P, ↑{y : Seed | (y, C x y) ∈ T}.card) / (↑P.card * ↑(Fintype.card Seed))

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

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

theorem Algebraic.Cutwidth.Extractor.Internal.abs_mixture_sub_le {ι : Type u_1} [Fintype ι] (w p q : ι → ℝ) (nonnegative : ∀ (i : ι), 0 ≤ w i) (mass : ∑ i : ι, w i = 1) {ε : ℝ} (close : ∀ (i : ι), |p i - q i| ≤ ε) : |∑ i : ι, w i * p i - ∑ i : ι, w i * q i| ≤ ε

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

theorem Algebraic.Cutwidth.Extractor.Internal.seededTestProb_eq_uniformMixture {α : 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 = seededMixtureTestProb (fun (x : ↥(Finset.powersetCard K P)) => (↑(Finset.powersetCard K P).card)⁻¹) (fun (S : ↥(Finset.powersetCard K P)) (x : ↥↑S) => C ↑x) T

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