Counting low-order parity tests and their bad seeds #
Every nonempty set of at most t coordinates is the range of a t-tuple:
enumerate it and repeat any member in the spare positions. The number of
tuples therefore bounds the number of tests, including at zero coordinates
or zero order. Two finite union bounds then control the common bad-seed set.
theorem
Algebraic.Cutwidth.Extractor.Internal.card_parityTests_le_pow
(ι : Type u_1)
[Fintype ι]
(t : ℕ)
:
theorem
Algebraic.Cutwidth.Extractor.Internal.card_parityBadSeeds_le
{ι : Type u_1}
{Choice : Type u_2}
{Seed : Type u_3}
[Fintype ι]
[Fintype Choice]
[Fintype Seed]
(bad : Finset ι → Choice → Finset Seed)
(t : ℕ)
{η : ℝ}
(hη : 0 ≤ η)
(bound : ∀ U ∈ parityTests ι t, ∀ (z : Choice), ↑(bad U z).card ≤ η * ↑(Fintype.card Seed))
:
↑(parityBadSeeds bad t).card ≤ ↑(Fintype.card ι) ^ t * ↑(Fintype.card Choice) * η * ↑(Fintype.card Seed)