Small covers by shifted distinctness tests

Explicit finite bounds for the covering argument in Lecomte and Ramakrishnan, Optimal Shallow Circuits for Majority, 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. The finite union bound is reused from Algebraic.Combinatorics.FiniteCover. 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!.

theorem Complexity.Shallow.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 Complexity.Shallow.exists_cover {S : Type u_1} {W : Type u_2} [Fintype S] [Nonempty S] [Fintype W] (hit : S → W → Prop) [DecidableRel hit] (q n : ℕ) (hq : 0 < q) (hw : Fintype.card W ≤ 2 ^ n) (density : ∀ (w : W), Fintype.card S ≤ q * Fintype.card { s : S // hit s w }) : ∃ (tests : Fin (q * (n + 1)) → S), ∀ (w : W), ∃ (i : Fin (q * (n + 1))), hit (tests i) w

A success density of at least 1/q covers 2^n obligations with q * (n + 1) tests. Repetition of tests is permitted.

theorem Complexity.Shallow.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 Complexity.Shallow.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.