Lautemann's covering lemma

Let S be a subset of a finite group G. If S is large, a few shifts of S cover G; if S is small, they do not. Precisely, if |G| |G \ S| ^ k < |G| ^ k, then some k elements u i satisfy ∀ g, ∃ i, g * u i ∈ S (exists_forall_exists_mul_mem_of_card_mul_card_compl_pow_lt), by the union bound over g for uniformly random shifts (exists_cover_of_scaled_card_lt). Conversely, if k |S| < |G|, then no k shifts do (exists_forall_mul_notMem_of_mul_card_lt), as the k translates have at most k |S| elements in all. Each of these statements has an additive version, with g + u i in place of g * u i.

On strings of m bits, with xor as the group operation, this is the combinatorial heart of the Sipser–Gács–Lautemann theorem BPP ⊆ Σ₂ᵖ ∩ Π₂ᵖ: if A decides L with error at most 1 / (2 m) over random strings of m bits, then x ∈ L iff some m shifts u i make A x (r + u i) true for one i at every string r (BitString.mem_iff_exists_forall_exists), and iff for all m shifts some r makes every A x (r + u i) true (BitString.mem_iff_forall_exists_forall). The bound m ≥ 2 is needed: at m = 1, an error of 1 / 2 carries no information.

Main results

• Cslib.exists_forall_exists_mul_mem_of_card_mul_card_compl_pow_lt: the union-bound form of the covering lemma; Cslib.exists_forall_exists_mul_mem_of_mul_card_compl_le is its density form.
• Cslib.exists_forall_mul_notMem_of_mul_card_lt: the converse, by counting; Cslib.exists_forall_mul_notMem_of_mul_card_le is its density form.
• Cslib.BitString.exists_forall_exists_add_mem_of_two_pow_mul_card_compl_le, Cslib.BitString.exists_forall_add_notMem_of_two_pow_mul_card_le: the two claims in Arora and Barak's proof of the Sipser–Gács theorem, for sets of strings of density 1 - 2 ^ (-n) and 2 ^ (-n).
• Cslib.BitString.mem_iff_exists_forall_exists, Cslib.BitString.mem_iff_forall_exists_forall: the ∃ ∀ ∃ and ∀ ∃ ∀ forms of a language decided with error at most 1 / (2 m).

References

• C. Lautemann, BPP and the polynomial hierarchy
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 7.5.2

theorem Cslib.exists_forall_exists_mul_mem_of_card_mul_card_compl_pow_lt {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (S : Finset G) {k : ℕ} (h : Fintype.card G * Sᶜ.card ^ k < Fintype.card G ^ k) : ∃ (u : Fin k → G), ∀ (g : G), ∃ (i : Fin k), g * u i ∈ S

Lautemann's covering lemma, union-bound form: if S is a subset of a finite group G with |G| |G \ S| ^ k < |G| ^ k, then some k shifts u i carry every g : G into S by right multiplication, g * u i ∈ S.

theorem Cslib.exists_forall_exists_add_mem_of_card_mul_card_compl_pow_lt {G : Type u_1} [AddGroup G] [Fintype G] [DecidableEq G] (S : Finset G) {k : ℕ} (h : Fintype.card G * Sᶜ.card ^ k < Fintype.card G ^ k) : ∃ (u : Fin k → G), ∀ (g : G), ∃ (i : Fin k), g + u i ∈ S

Lautemann's covering lemma, union-bound form: if S is a subset of a finite additive group G with |G| |G \ S| ^ k < |G| ^ k, then some k shifts u i carry every g : G into S by addition, g + u i ∈ S.

theorem Cslib.exists_forall_exists_mul_mem_of_mul_card_compl_le {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (S : Finset G) {q k : ℕ} (hS : q * Sᶜ.card ≤ Fintype.card G) (hk : Fintype.card G < q ^ k) : ∃ (u : Fin k → G), ∀ (g : G), ∃ (i : Fin k), g * u i ∈ S

Lautemann's covering lemma, density form: if S misses at most a 1 / q fraction of the finite group G, that is q |G \ S| ≤ |G|, and |G| < q ^ k, then some k shifts u i carry every g : G into S by right multiplication, g * u i ∈ S.

theorem Cslib.exists_forall_exists_add_mem_of_mul_card_compl_le {G : Type u_1} [AddGroup G] [Fintype G] [DecidableEq G] (S : Finset G) {q k : ℕ} (hS : q * Sᶜ.card ≤ Fintype.card G) (hk : Fintype.card G < q ^ k) : ∃ (u : Fin k → G), ∀ (g : G), ∃ (i : Fin k), g + u i ∈ S

Lautemann's covering lemma, density form: if S misses at most a 1 / q fraction of the finite additive group G, that is q |G \ S| ≤ |G|, and |G| < q ^ k, then some k shifts u i carry every g : G into S by addition, g + u i ∈ S.

theorem Cslib.exists_forall_mul_notMem_of_mul_card_lt {G : Type u_1} [Group G] [Fintype G] (S : Finset G) {k : ℕ} (h : k * S.card < Fintype.card G) (u : Fin k → G) : ∃ (g : G), ∀ (i : Fin k), g * u i ∉ S

The converse of Lautemann's covering lemma: if k |S| < |G|, then for any k shifts u i of the finite group G, some g : G has g * u i ∉ S for every i.

theorem Cslib.exists_forall_add_notMem_of_mul_card_lt {G : Type u_1} [AddGroup G] [Fintype G] (S : Finset G) {k : ℕ} (h : k * S.card < Fintype.card G) (u : Fin k → G) : ∃ (g : G), ∀ (i : Fin k), g + u i ∉ S

The converse of Lautemann's covering lemma: if k |S| < |G|, then for any k shifts u i of the finite additive group G, some g : G has g + u i ∉ S for every i.

theorem Cslib.exists_forall_mul_notMem_of_mul_card_le {G : Type u_1} [Group G] [Fintype G] (S : Finset G) {q k : ℕ} (hS : q * S.card ≤ Fintype.card G) (hk : k < q) (u : Fin k → G) : ∃ (g : G), ∀ (i : Fin k), g * u i ∉ S

The converse of Lautemann's covering lemma, density form: if S is at most a 1 / q fraction of the finite group G, that is q |S| ≤ |G|, and k < q, then for any k shifts u i, some g : G has g * u i ∉ S for every i.

theorem Cslib.exists_forall_add_notMem_of_mul_card_le {G : Type u_1} [AddGroup G] [Fintype G] (S : Finset G) {q k : ℕ} (hS : q * S.card ≤ Fintype.card G) (hk : k < q) (u : Fin k → G) : ∃ (g : G), ∀ (i : Fin k), g + u i ∉ S

The converse of Lautemann's covering lemma, density form: if S is at most a 1 / q fraction of the finite additive group G, that is q |S| ≤ |G|, and k < q, then for any k shifts u i, some g : G has g + u i ∉ S for every i.

theorem Cslib.BitString.exists_forall_exists_add_mem_of_two_pow_mul_card_compl_le {m n k : ℕ} (S : Finset (BitString m)) (hS : 2 ^ n * Sᶜ.card ≤ 2 ^ m) (hk : m < n * k) : ∃ (u : Fin k → BitString m), ∀ (r : BitString m), ∃ (i : Fin k), r + u i ∈ S

Lautemann's covering lemma for bit strings, with xor as the group operation Arora and Barak, Section 7.5.2: if a set S of strings of m bits misses at most a 2 ^ (-n) fraction of them, that is 2 ^ n |Sᶜ| ≤ 2 ^ m, and m < n k, then some k shifts u i carry every string r into S, r + u i ∈ S.

theorem Cslib.BitString.exists_forall_add_notMem_of_two_pow_mul_card_le {m n k : ℕ} (S : Finset (BitString m)) (hS : 2 ^ n * S.card ≤ 2 ^ m) (hk : k < 2 ^ n) (u : Fin k → BitString m) : ∃ (r : BitString m), ∀ (i : Fin k), r + u i ∉ S

The converse of Lautemann's covering lemma for bit strings, with xor as the group operation Arora and Barak, Section 7.5.2: if a set S of strings of m bits is at most a 2 ^ (-n) fraction of them, that is 2 ^ n |S| ≤ 2 ^ m, and k < 2 ^ n, then for any k shifts u i, some string r has r + u i ∉ S for every i.

theorem Cslib.BitString.mem_iff_exists_forall_exists {m : ℕ} {α : Type u_1} {L : Set α} {A : α → BitString m → Bool} (hm : 2 ≤ m) (hmem : ∀ x ∈ L, 2 * m * {r : BitString m | A x r = false}.card ≤ 2 ^ m) (hnotMem : ∀ x ∉ L, 2 * m * {r : BitString m | A x r = true}.card ≤ 2 ^ m) (x : α) : x ∈ L ↔ ∃ (u : Fin m → BitString m), ∀ (r : BitString m), ∃ (i : Fin m), A x (r + u i) = true

The finite core of the Sipser–Gács–Lautemann theorem, ∃ ∀ ∃ form (Lautemann, Arora and Barak, Theorem 7.15): let A x r decide x ∈ L with error at most 1 / (2 m) over the strings r of m ≥ 2 bits, that is, for each x, it is wrong for at most 2 ^ m / (2 m) strings r. Then x ∈ L iff there are m shifts u i such that, for every string r, A x (r + u i) holds for some i, where + is xor.

theorem Cslib.BitString.mem_iff_forall_exists_forall {m : ℕ} {α : Type u_1} {L : Set α} {A : α → BitString m → Bool} (hm : 2 ≤ m) (hmem : ∀ x ∈ L, 2 * m * {r : BitString m | A x r = false}.card ≤ 2 ^ m) (hnotMem : ∀ x ∉ L, 2 * m * {r : BitString m | A x r = true}.card ≤ 2 ^ m) (x : α) : x ∈ L ↔ ∀ (u : Fin m → BitString m), ∃ (r : BitString m), ∀ (i : Fin m), A x (r + u i) = true

The finite core of the Sipser–Gács–Lautemann theorem, ∀ ∃ ∀ form (Lautemann, Arora and Barak, Theorem 7.15): let A x r decide x ∈ L with error at most 1 / (2 m) over the strings r of m ≥ 2 bits, that is, for each x, it is wrong for at most 2 ^ m / (2 m) strings r. Then x ∈ L iff for all m shifts u i there is a string r such that A x (r + u i) holds for every i, where + is xor.