The seed tests used by low-order parity reduction

The bad-seed union in Chattopadhyay and Liao, Extractors for Sum of Two Sources (2021), Lemma 5.4 ranges over nonempty coordinate subsets of size at most t and over every candidate seed. Keeping this union explicit lets one somewhere sampler supply all the required parity tests simultaneously.

noncomputable def Algebraic.Cutwidth.Extractor.parityTests (ι : Type u_1) [Fintype ι] (t : ℕ) : Finset (Finset ι)

The nonempty coordinate sets of size at most t.

Equations

• Algebraic.Cutwidth.Extractor.parityTests ι t = {U : Finset ι | U.Nonempty ∧ U.card ≤ t}

noncomputable def Algebraic.Cutwidth.Extractor.parityBadSeeds {ι : Type u_1} {Choice : Type u_2} {Seed : Type u_3} [Fintype ι] [Fintype Choice] (bad : Finset ι → Choice → Finset Seed) (t : ℕ) : Finset Seed

All bad seeds for all low-order parity tests and all candidate positions.

Equations

• Algebraic.Cutwidth.Extractor.parityBadSeeds bad t = (Algebraic.Cutwidth.Extractor.parityTests ι t).biUnion fun (U : Finset ι) => Finset.univ.biUnion (bad U)