Pulling low-degree functions back along XOR

Over a field of characteristic two, a monomial at x + y expands over partitions of its coordinates between x and y. If its degree is at most p + q + 1, every term has degree at most p in the first input or at most q in the second. Thus the pullback lies in a sum of two slice spaces. The statement uses the existing function-space definition of low degree and the general image-sparsification API; it does not restrict the degree of the Boolean predicates whose accepting sets will later be sparsified.

Main results

• Cslib.BitString.bitVal_xor_of_char_two: XOR becomes addition in characteristic two.
• Cslib.BitString.monomial_add: the squarefree expansion of a monomial at a sum.
• Cslib.BitString.hasSliceDecomposition_add: low-degree spaces satisfy the general pullback criterion for image sparsification.

References

• The degree split is the polynomial-method step in J. S. Ellenberg, Sumsets as unions of sumsets of subsets, proof of Theorem 1, pp. 2–3. Here it is expressed as containment in fixed slice spaces, rather than only as a bound on each matrix's rank.

theorem Cslib.BitString.bitVal_xor_of_char_two {K : Type u_1} [CommRing K] [CharP K 2] (a b : Bool) : bitVal K (a ^^ b) = bitVal K a + bitVal K b

Reading bits in characteristic two takes XOR to addition.

theorem Cslib.BitString.monomial_add {K : Type u_1} {ι : Type u_2} [CommRing K] [CharP K 2] [DecidableEq ι] (S : Finset ι) (x y : ι → Bool) : monomial K S (x + y) = ∑ T ∈ S.powerset, monomial K T x * monomial K (S \ T) y

Expanding a squarefree monomial at a sum partitions its coordinates between the inputs.

theorem Cslib.BitString.hasSliceDecomposition_add {K : Type u_1} {ι : Type u_2} [Field K] [CharP K 2] (p q : ℕ) : ImageSparsification.HasSliceDecomposition (fun (x y : ι → Bool) => x + y) (lowDegree K ι p) (lowDegree K ι q) (lowDegree K ι (p + q + 1))

A polynomial of degree at most p + q + 1 at x + y is a sum of slices with first-input degree at most p or second-input degree at most q.