Documentation

Complexity.Foundations.Combinatorics.Additive.SumsetCover

Small representative sets for Boolean sumsets #

For arbitrary subsets A and B of the Boolean cube, choose A₀ ⊆ A and B₀ ⊆ B such that A + B = (A₀ + B) ∪ (A + B₀) and |A₀| + |B₀| ≤ 3 ∑_{j ≤ n/3} binom(n,j). Here addition of bit strings is coordinatewise XOR. There is no degree or circuit-size assumption on A and B.

This is the case q = 2 (the field 𝔽₂) of [Ellenberg2017Sumsets, Theorem 1, pp. 1–2]. The proof uses the general image-sparsification theorem with restricted low-degree evaluation spaces. Its input is the common slice-space containment of the polynomial pullbacks; we do not use or formalize the theorem of Meshulam used in the published proof. All choices are nonuniform.

Main results #

References #

theorem Cslib.BitString.exists_add_cover_of_degree {ι : Type u_1} [Fintype ι] (A B : Finset (ι → Bool)) (p q : ℕ) :
∃ (A₀ : Finset (ι → Bool)) (B₀ : Finset (ι → Bool)), A₀ ⊆ A ∧ B₀ ⊆ B ∧ A + B = A₀ + B ∪ (A + B₀) ∧ A₀.card + B₀.card ≤ {S : Finset ι | S.card ≤ p}.card + {S : Finset ι | S.card ≤ q}.card + (2 ^ Fintype.card ι - {S : Finset ι | S.card ≤ p + q + 1}.card)

Restricting the degree-p and degree-q evaluation spaces to the two summands yields an exact sumset cover with budget D(p) + D(q) + 2^n - D(p+q+1). Parentheses around the codimension keep the subtraction in natural numbers local to that term.

theorem Cslib.BitString.exists_add_cover {ι : Type u_1} [Fintype ι] (A B : Finset (ι → Bool)) :
∃ (A₀ : Finset (ι → Bool)) (B₀ : Finset (ι → Bool)), A₀ ⊆ A ∧ B₀ ⊆ B ∧ A + B = A₀ + B ∪ (A + B₀) ∧ A₀.card + B₀.card ≤ 3 * {S : Finset ι | S.card ≤ Fintype.card ι / 3}.card

Ellenberg's sumset cover on the Boolean cube. At most three times the number of degree-⌊n/3⌋ monomials suffice to generate the whole sumset using translates of the original summands. This includes empty summands and the zero-dimensional cube.