Small covers by shifted distinctness tests

Explicit finite bounds for the covering argument of Lecomte and Ramakrishnan, Sections 3 and 4. A test accepting at least a 1/q fraction of the seeds at every valid input has a cover of size q * (n + 1) when there are at most 2^n valid inputs, by the union bound (Cslib.exists_cover_of_density). We sample all shift vectors and reject those with the wrong sum, rather than sampling only sum-compatible vectors as in the paper. The resulting density k! / k^k still gives the required exponential bound, using k^k ≤ 3^k * k!.

Main results

• Cslib.Circuits.Boolean.ShallowSymmetric.exists_shiftTest_cover, Cslib.Circuits.Boolean.ShallowSymmetric.exists_simultaneous_shiftTest_cover: small covers by shifted tests.

References

• V. Lecomte, P. Ramakrishnan, Optimal Shallow Circuits for Majority

theorem Cslib.Circuits.Boolean.ShallowSymmetric.pow_self_le_three_pow_mul_factorial (k : ℕ) : k ^ k ≤ 3 ^ k * k.factorial

A convenient elementary form of the factorial estimate; no asymptotics.

theorem Cslib.Circuits.Boolean.ShallowSymmetric.exists_shiftTest_cover {G : Type u_1} {W : Type u_2} [Fintype G] [AddCommGroup G] [Fintype W] (t : G) (w : W → G → G) (n : ℕ) (hcard : Fintype.card W ≤ 2 ^ n) (hw : ∀ (x : W), ∑ i : G, w x i = t) : ∃ (tests : Fin (3 ^ Fintype.card G * (n + 1)) → G → G), ∀ (x : W), ∃ (j : Fin (3 ^ Fintype.card G * (n + 1))), ShiftTest t (w x) (tests j)

The shifted tests cover any 2^n valid weight vectors using at most 3^|G| * (n+1) tests.

theorem Cslib.Circuits.Boolean.ShallowSymmetric.exists_simultaneous_shiftTest_cover {ι : Type u_1} {W : Type u_2} [Fintype ι] [Fintype W] {G : ι → Type u_3} [(i : ι) → Fintype (G i)] [(i : ι) → AddCommGroup (G i)] (t : (i : ι) → G i) (w : W → (i : ι) → G i → G i) (n : ℕ) (hcard : Fintype.card W ≤ 2 ^ n) (hw : ∀ (x : W) (i : ι), ∑ a : G i, w x i a = t i) : ∃ (tests : Fin ((3 ^ ∑ i : ι, Fintype.card (G i)) * (n + 1)) → (i : ι) → G i → G i), ∀ (x : W), ∃ (j : Fin ((3 ^ ∑ i : ι, Fintype.card (G i)) * (n + 1))), ∀ (i : ι), ShiftTest (t i) (w x i) (tests j i)

Independent residue tests can be covered simultaneously, with an exponent equal to the sum of the group sizes.