Composition through seedwise flat mixtures

A fresh independent extractor seed first preserves the condenser's test error. Conditional flat witnesses then satisfy the strong extractor bound for each original seed, and averaging the normalized mixture preserves that bound. Both seeds are retained in the final tests.

theorem Algebraic.Cutwidth.Extractor.Internal.abs_uniform_average_sub_le {ι : Type u_1} [Fintype ι] [Nonempty ι] (p q : ι → ℝ) {ε : ℝ} (close : ∀ (i : ι), |p i - q i| ≤ ε) : |(∑ i : ι, p i) / ↑(Fintype.card ι) - (∑ i : ι, q i) / ↑(Fintype.card ι)| ≤ ε

theorem Algebraic.Cutwidth.Extractor.Internal.strong_extractor_embedding {α : Type u_1} {Fresh : Type u_2} {Z : Type u_3} {Ω : Type u_4} [Fintype α] [Nonempty α] [Fintype Fresh] [Fintype Ω] (g : α ↪ Z) (H : Z → Fresh → Ω) {K : ℕ} {ε : ℝ} (extract : FlatStrongSeededExtractor H K ε) (size : K ≤ Fintype.card α) (T : Finset (Fresh × Ω)) : |seededTestProb (fun (x : α) (a : Fresh) => H (g x) a) T - uniformSeededTestProb T| ≤ ε

theorem Algebraic.Cutwidth.Extractor.Internal.strong_extractor_seedwise_embedding {α : Type u_1} {Seed : Type u_2} {Fresh : Type u_3} {Z : Type u_4} {Ω : Type u_5} [Fintype α] [Nonempty α] [Fintype Seed] [Nonempty Seed] [Fintype Fresh] [Fintype Ω] (g : Seed → α ↪ Z) (H : Z → Fresh → Ω) {K : ℕ} {ε : ℝ} (extract : FlatStrongSeededExtractor H K ε) (size : K ≤ Fintype.card α) (T : Finset ((Seed × Fresh) × Ω)) : |seededTestProb (fun (x : α) (ya : Seed × Fresh) => H ((g ya.1) x) ya.2) T - uniformSeededTestProb T| ≤ ε

theorem Algebraic.Cutwidth.Extractor.Internal.seededMixtureTestProb_comp_pullback {ι : Type u_1} {Seed : Type u_2} {Fresh : Type u_3} {Z : Type u_4} {Ω : Type u_5} [Fintype ι] [Fintype Seed] [Fintype Fresh] [Fintype Z] {Source : ι → Type u_6} [(i : ι) → Fintype (Source i)] (w : ι → ℝ) (C : (i : ι) → Source i → Seed → Z) (H : Z → Fresh → Ω) (T : Finset ((Seed × Fresh) × Ω)) : seededMixtureTestProb w (fun (i : ι) (x : Source i) (ya : Seed × Fresh) => H (C i x ya.1) ya.2) T = (∑ a : Fresh, seededMixtureTestProb w C (compositionPullback H T a)) / ↑(Fintype.card Fresh)

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

theorem Algebraic.Cutwidth.Extractor.Internal.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 Ω] (C : α → Seed → Z) (H : Z → Fresh → Ω) {K : ℕ} (positive : 0 < K) {δ ε : ℝ} (extract : FlatStrongSeededExtractor H 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 (δ + ε)