Exact dimensions of low-degree functions on the Boolean cube

The squarefree monomials form a basis over any field: they span all functions, and their number equals the dimension of the function space. Restricting this basis gives the exact dimension of BitString.lowDegree. Complementing coordinate sets bounds the codimension by another low-degree dimension, which is useful when a polynomial-method argument budgets exceptional outputs by codimension.

Main results

• Cslib.BitString.linearIndependent_monomial: squarefree monomials are independent.
• Cslib.BitString.finrank_lowDegree: the exact dimension, including degrees above the dimension of the cube.
• Cslib.BitString.card_sub_finrank_lowDegree_le: a complementary-degree codimension bound.

theorem Cslib.BitString.linearIndependent_monomial {K : Type u_1} {ι : Type u_2} [Field K] [Finite ι] : LinearIndependent K (monomial K)

The squarefree monomials on a finite Boolean cube are linearly independent over any field.

theorem Cslib.BitString.finrank_lowDegree {K : Type u_1} {ι : Type u_2} [Field K] [Fintype ι] (D : ℕ) : Module.finrank K ↥(lowDegree K ι D) = {S : Finset ι | S.card ≤ D}.card

The dimension of the functions of degree at most D is exactly the number of coordinate sets of cardinality at most D.

theorem Cslib.BitString.card_sub_finrank_lowDegree_le {K : Type u_1} {ι : Type u_2} [Field K] [Fintype ι] {D E : ℕ} (h : Fintype.card ι ≤ D + E + 1) : 2 ^ Fintype.card ι - Module.finrank K ↥(lowDegree K ι D) ≤ {S : Finset ι | S.card ≤ E}.card

Complementing sets of size greater than D injects them into the sets of size at most E when n ≤ D + E + 1. Equivalently, the codimension of degree D is at most the dimension of degree E.