From polynomial expansion to seed-preserving flat condensation

The power-of-two map has the same neighbors as the GUV graph. Its expansion loss divided by the field cardinality bounds every seeded test discrepancy from a distribution uniform on one equally sized set in each seed fiber. The witness may depend on the source support.

theorem Algebraic.Cutwidth.Extractor.Internal.polynomialCondenser_flat_lossless {F : Type u_1} [Field F] [Fintype F] {r m : ℕ} (E : Polynomial F) (monic : E.Monic) (irreducible : Irreducible E) (degree : 1 < E.natDegree) (fieldSize : 2 ^ r ≤ Fintype.card F) (P : Finset (Polynomial F)) (nonempty : P.Nonempty) (source : ∀ f ∈ P, f.degree < E.degree) (size : P.card ≤ (2 ^ r) ^ m) : ∃ (g : F → ↥P ↪ Fin m → F), ∀ (T : Finset (F × (Fin m → F))), |seededTestProb (fun (f : ↥P) => polynomialCondenser E r m ↑f) T - seededTestProb (fun (f : ↥P) (y : F) => (g y) f) T| ≤ ↑((E.natDegree - 1) * (2 ^ r - 1) * m) / ↑(Fintype.card F)

theorem Algebraic.Cutwidth.Extractor.Internal.polynomialCondenser_flat_mixture {F : Type u_1} [Field F] [Fintype F] {r m K : ℕ} (E : Polynomial F) (monic : E.Monic) (irreducible : Irreducible E) (degree : 1 < E.natDegree) (fieldSize : 2 ^ r ≤ Fintype.card F) (P : Finset (Polynomial F)) (source : ∀ f ∈ P, f.degree < E.degree) (positive : 0 < K) (threshold : K ≤ P.card) (capacity : K ≤ (2 ^ r) ^ m) : ∃ (g : (S : ↥(Finset.powersetCard K P)) → F → ↥↑S ↪ Fin m → F), ∀ (T : Finset (F × (Fin m → F))), |seededTestProb (fun (f : ↥P) => polynomialCondenser E r m ↑f) T - seededMixtureTestProb (fun (x : ↥(Finset.powersetCard K P)) => (↑(Finset.powersetCard K P).card)⁻¹) (fun (S : ↥(Finset.powersetCard K P)) (f : ↥↑S) (y : F) => (g S y) f) T| ≤ ↑((E.natDegree - 1) * (2 ^ r - 1) * m) / ↑(Fintype.card F)