Condensing and then strongly extracting from flat mixtures

A condenser may approximate a mixture of flat distributions whose supports vary with its retained seed. A strong extractor applied with a fresh, independent seed extracts from every component. The two errors add, and the conclusion retains both seeds. Witness injections describe the ideal conditional sources; no injectivity of the actual condenser is assumed.

This is a finite mixture formulation of the condense-then-extract argument in Guruswami--Umans--Vadhan, Proposition 4.5 and Remark 5.15 (https://people.seas.harvard.edu/~salil/research/PVcondenser-jacm.pdf), and Chattopadhyay--Goodman--Liao, Lemma 4.9 (https://eccc.weizmann.ac.il/report/2021/075/download/). The hypotheses supply the condenser witnesses and the extractor guarantee. They do not construct an extractor, prove seed-length bounds, or decompose arbitrary weighted sources into flat distributions.

theorem Algebraic.Cutwidth.Extractor.seededTestProb_comp_of_flat_mixture {α : Type u_1} {ι : Type u_2} {Seed : Type u_3} {Fresh : Type u_4} {Z : Type u_5} {Ω : Type u_6} [Fintype α] [Fintype ι] [Fintype Seed] [Nonempty Seed] [Fintype Fresh] [Nonempty Fresh] [Fintype Z] [Fintype Ω] {Source : ι → Type u_7} [(i : ι) → Fintype (Source i)] (C : α → Seed → Z) (H : Z → Fresh → Ω) (w : ι → ℝ) (g : (i : ι) → Seed → Source i ↪ Z) (nonnegative : ∀ (i : ι), 0 ≤ w i) (mass : ∑ i : ι, w i = 1) {K : ℕ} (positive : 0 < K) (size : ∀ (i : ι), K ≤ Fintype.card (Source i)) {δ ε : ℝ} (extract : FlatStrongSeededExtractor H K ε) (close : ∀ (T : Finset (Seed × Z)), |seededTestProb C T - seededMixtureTestProb w (fun (i : ι) (x : Source i) (y : Seed) => (g i y) x) T| ≤ δ) (T : Finset ((Seed × Fresh) × Ω)) : |seededTestProb (fun (x : α) (ya : Seed × Fresh) => H (C x ya.1) ya.2) T - uniformSeededTestProb T| ≤ δ + ε

Extraction after a supplied normalized mixture of seedwise flat witnesses. Each component has at least K points, and its support may depend on the condenser seed. Tests retain both independent seeds; their errors add.

theorem Algebraic.Cutwidth.Extractor.FlatStrongSeededExtractor.comp_of_flat_mixture {α : Type u_1} {Seed : Type u_2} {Fresh : Type u_3} {Z : Type u_4} {Ω : Type u_5} [Fintype Seed] [Nonempty Seed] [Fintype Fresh] [Nonempty Fresh] [Fintype Z] [Fintype Ω] {H : Z → Fresh → Ω} {K : ℕ} {δ ε : ℝ} (extract : FlatStrongSeededExtractor H K ε) (C : α → Seed → Z) (positive : 0 < K) (lossless : ∀ (P : Finset α), P.Nonempty → K ≤ P.card → ∃ (g : (S : ↥(Finset.powersetCard K P)) → Seed → ↥↑S ↪ Z), ∀ (T : Finset (Seed × Z)), |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| ≤ δ) : FlatStrongSeededExtractor (fun (x : α) (ya : Seed × Fresh) => H (C x ya.1) ya.2) K (δ + ε)

The subset-mixture witness contract of a lossless condenser composes with a strong extractor. The resulting extractor retains both independent seeds.