Parity is far from low-degree functions

Over a field F in which 2 is invertible, a function of degree at most D agrees with the parity of all |ι| coordinates on at most as many inputs as there are sets of at most |ι| / 2 + D coordinates (BitString.card_agree_parityOn_univ_le) [Smo87]. The proof works with the characters chi F S, the products of the signs (-1) ^ xᵢ = 1 - 2 xᵢ over the sets S, with values in F: the parity of all coordinates, read as a sign, is the character of univ (BitString.chi_eq_neg_one_pow_parityOn), and characters square to 1. So on the inputs where a function P of degree D agrees with parity, a character of more than |ι| / 2 coordinates equals 1 - 2 P times the character of the other coordinates, of degree at most |ι| / 2 + D. Every function on these inputs therefore agrees with one of degree at most |ι| / 2 + D (BitString.exists_agree_of_parity), and comparing dimensions bounds the number of inputs (BitString.card_le_of_forall_exists_agree).

Main results

• Cslib.BitString.exists_agree_of_parity, Cslib.BitString.card_le_of_forall_exists_agree: if Q of degree D agrees with the full character on G, every function on G agrees with one of degree at most |ι| / 2 + D, bounding #G.
• Cslib.BitString.card_agree_parityOn_univ_le, Cslib.BitString.card_agree_parity_le: parity is far from low-degree functions.

References

• R. Smolensky, Algebraic methods in the theory of lower bounds for Boolean circuit complexity

theorem Cslib.BitString.exists_agree_of_parity {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] [Invertible 2] {D : ℕ} {Q : (ι → Bool) → F} (hQ : Q ∈ lowDegree F ι D) (G : Finset (ι → Bool)) (hG : ∀ x ∈ G, Q x = chi F Finset.univ x) (f : (ι → Bool) → F) : ∃ p ∈ lowDegree F ι (Fintype.card ι / 2 + D), ∀ x ∈ G, p x = f x

If Q has degree at most D and agrees with the character of all coordinates on G, every function agrees on G with a function of degree at most |ι| / 2 + D.

theorem Cslib.BitString.card_le_of_forall_exists_agree {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] {H : ℕ} (G : Finset (ι → Bool)) (hG : ∀ (f : (ι → Bool) → F), ∃ p ∈ lowDegree F ι H, ∀ x ∈ G, p x = f x) : G.card ≤ {S : Finset ι | S.card ≤ H}.card

If every function agrees on G with a function of degree at most H, then G has at most as many points as there are sets of at most H coordinates.

theorem Cslib.BitString.card_agree_parityOn_univ_le {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] [DecidableEq ι] [DecidableEq F] [Invertible 2] {D : ℕ} {P : (ι → Bool) → F} (hP : P ∈ lowDegree F ι D) : {x : ι → Bool | P x = bitVal F (parityOn Finset.univ x)}.card ≤ {S : Finset ι | S.card ≤ Fintype.card ι / 2 + D}.card

Parity is far from low-degree functions. A function of degree at most D agrees with the parity of all coordinates on at most as many inputs as there are sets of at most |ι| / 2 + D coordinates.

theorem Cslib.BitString.card_agree_parity_le {F : Type u_1} [Field F] [DecidableEq F] [Invertible 2] {n D : ℕ} {P : BitString n → F} (hP : P ∈ lowDegree F (Fin n) D) : {x : BitString n | P x = bitVal F (parity n x)}.card ≤ {S : Finset (Fin n) | S.card ≤ n / 2 + D}.card

Parity is far from low-degree functions. A function of degree at most D agrees with parity on at most as many inputs as there are sets of at most n / 2 + D coordinates.