Low-degree functions on the Boolean cube

Reading the bits of x : ι → Bool as 0 and 1 in a commutative ring R (BitString.bitVal), the monomial of a set S of coordinates is the function x ↦ ∏_{i ∈ S} x i (BitString.monomial), and the functions of degree at most D are the R-linear combinations of monomials of at most D coordinates (BitString.lowDegree). This is the degree of the multilinear polynomial representing a function on the cube, without formal polynomials: on bits every monomial is idempotent, so products of monomials are monomials (BitString.monomial_mul) and degrees add under multiplication (BitString.mul_mem_lowDegree). Evaluated at the bits read in R, Mathlib's polynomials of total degree at most D give exactly the functions of degree at most D (BitString.lowDegree_eq_map_restrictTotalDegree). Every function has degree at most the number of coordinates (BitString.mem_lowDegree_self), and the functions of degree at most D span a space of dimension at most the number of sets of at most D coordinates (BitString.finrank_lowDegree_le), which is at most (n + 1) ^ D for n coordinates (BitString.card_filter_card_le_le_pow).

These are the polynomials of Razborov's and Smolensky's approximation method [Raz87], [Smo87].

Main definitions

• Cslib.BitString.monomial, Cslib.BitString.lowDegree.

Main results

• Cslib.BitString.mul_mem_lowDegree: degrees add under multiplication.
• Cslib.BitString.lowDegree_eq_map_restrictTotalDegree: the functions of degree at most D are the evaluations at bits of the polynomials of total degree at most D.
• Cslib.BitString.mem_lowDegree_self: every function has degree at most the number of coordinates.
• Cslib.BitString.finrank_lowDegree_le: the dimension of the functions of degree at most D.
• Cslib.BitString.card_filter_card_le_le_pow: there are at most (n + 1) ^ D sets of at most D of n coordinates.

References

• A. A. Razborov, Lower bounds on the size of bounded depth circuits over a complete basis with logical addition
• R. Smolensky, Algebraic methods in the theory of lower bounds for Boolean circuit complexity

def Cslib.BitString.monomial (R : Type u_1) [CommRing R] {ι : Type u_2} (S : Finset ι) (x : ι → Bool) : R

The monomial of a set S of coordinates: the product of the selected bits, read in R. The empty monomial is the constant 1.

def Cslib.BitString.lowDegree (R : Type u_1) [CommRing R] (ι : Type u_2) (D : ℕ) : Submodule R ((ι → Bool) → R)

The functions on the cube of degree at most D: the R-linear span of the monomials of at most D coordinates.

theorem Cslib.BitString.monomial_apply {R : Type u_1} [CommRing R] {ι : Type u_2} (S : Finset ι) (x : ι → Bool) : monomial R S x = if ∀ i ∈ S, x i = true then 1 else 0

A monomial is 1 where all its coordinates are true and 0 elsewhere.

theorem Cslib.BitString.monomial_mul {R : Type u_1} [CommRing R] {ι : Type u_2} [DecidableEq ι] (S T : Finset ι) : monomial R S * monomial R T = monomial R (S ∪ T)

The product of two monomials is the monomial of the union.

@[simp]

theorem Cslib.BitString.monomial_empty {R : Type u_1} [CommRing R] {ι : Type u_2} : monomial R ∅ = 1

The monomial of the empty set is the constant 1.

theorem Cslib.BitString.monomial_singleton {R : Type u_1} [CommRing R] {ι : Type u_2} (i : ι) : monomial R {i} = fun (x : ι → Bool) => bitVal R (x i)

The monomial of a single coordinate i is the bit at i, read in R.

theorem Cslib.BitString.monomial_mem_lowDegree {R : Type u_1} [CommRing R] {ι : Type u_2} {S : Finset ι} {D : ℕ} (hS : S.card ≤ D) : monomial R S ∈ lowDegree R ι D

The monomial of a set of at most D coordinates has degree at most D.

theorem Cslib.BitString.lowDegree_mono {R : Type u_1} [CommRing R] {ι : Type u_2} {D E : ℕ} (hDE : D ≤ E) : lowDegree R ι D ≤ lowDegree R ι E

The functions of degree at most D have degree at most E when D ≤ E.

theorem Cslib.BitString.one_mem_lowDegree {R : Type u_1} [CommRing R] {ι : Type u_2} (D : ℕ) : 1 ∈ lowDegree R ι D

The constant function 1 has degree at most D, for every D.

theorem Cslib.BitString.const_mem_lowDegree {R : Type u_1} [CommRing R] {ι : Type u_2} (D : ℕ) (c : R) : (fun (x : ι → Bool) => c) ∈ lowDegree R ι D

A constant function has degree at most D, for every D.

theorem Cslib.BitString.bitVal_mem_lowDegree {R : Type u_1} [CommRing R] {ι : Type u_2} (i : ι) : (fun (x : ι → Bool) => bitVal R (x i)) ∈ lowDegree R ι 1

The bit at a coordinate i, read in R, has degree at most 1.

theorem Cslib.BitString.lowDegree_mul_le {R : Type u_1} [CommRing R] {ι : Type u_2} (a b : ℕ) : lowDegree R ι a * lowDegree R ι b ≤ lowDegree R ι (a + b)

Degrees add under multiplication.

theorem Cslib.BitString.mul_mem_lowDegree {R : Type u_1} [CommRing R] {ι : Type u_2} {a b : ℕ} {f g : (ι → Bool) → R} (hf : f ∈ lowDegree R ι a) (hg : g ∈ lowDegree R ι b) : f * g ∈ lowDegree R ι (a + b)

The product of functions of degrees at most a and b has degree at most a + b.

theorem Cslib.BitString.pow_mem_lowDegree {R : Type u_1} [CommRing R] {ι : Type u_2} {a : ℕ} {f : (ι → Bool) → R} (hf : f ∈ lowDegree R ι a) (k : ℕ) : f ^ k ∈ lowDegree R ι (k * a)

The k-th power of a function of degree at most a has degree at most k * a.

theorem Cslib.BitString.prod_mem_lowDegree {R : Type u_1} [CommRing R] {ι : Type u_2} {α : Type u_3} (s : Finset α) {a : ℕ} {f : α → (ι → Bool) → R} (hf : ∀ i ∈ s, f i ∈ lowDegree R ι a) : ∏ i ∈ s, f i ∈ lowDegree R ι (s.card * a)

A product over s of functions of degree at most a has degree at most #s * a.

theorem Cslib.BitString.sum_mem_lowDegree {R : Type u_1} [CommRing R] {ι : Type u_2} {α : Type u_3} (s : Finset α) {a : ℕ} {f : α → (ι → Bool) → R} (hf : ∀ i ∈ s, f i ∈ lowDegree R ι a) : ∑ i ∈ s, f i ∈ lowDegree R ι a

A sum of functions of degree at most a has degree at most a.

theorem Cslib.BitString.one_sub_mem_lowDegree {R : Type u_1} [CommRing R] {ι : Type u_2} {a : ℕ} {f : (ι → Bool) → R} (hf : f ∈ lowDegree R ι a) : 1 - f ∈ lowDegree R ι a

If f has degree at most a, so does 1 - f.

theorem Cslib.BitString.comp_not_mem_lowDegree {R : Type u_1} [CommRing R] {ι : Type u_2} {D : ℕ} {f : (ι → Bool) → R} (hf : f ∈ lowDegree R ι D) : (fun (x : ι → Bool) => f fun (i : ι) => !x i) ∈ lowDegree R ι D

Negating all the bits of the input preserves the degree.

theorem Cslib.BitString.lowDegree_eq_map_restrictTotalDegree {R : Type u_1} [CommRing R] {ι : Type u_2} (D : ℕ) : lowDegree R ι D = Submodule.map (MvPolynomial.aeval fun (i : ι) (x : ι → Bool) => bitVal R (x i)).toLinearMap (MvPolynomial.restrictTotalDegree ι R D)

Low degree as total degree. The functions of degree at most D are the evaluations at the bits, read in R, of the multivariate polynomials of total degree at most D: a monomial x^d evaluates to the monomial of the support of d, every bit being idempotent.

theorem Cslib.BitString.mem_lowDegree_self {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] (f : (ι → Bool) → R) : f ∈ lowDegree R ι (Fintype.card ι)

Every function on the cube has degree at most the number of coordinates: it is the sum, over the points a, of its value at a times the indicator of a, a product of one function of degree one per coordinate.

theorem Cslib.BitString.finrank_lowDegree_le {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [StrongRankCondition R] (D : ℕ) : Module.finrank R ↥(lowDegree R ι D) ≤ {S : Finset ι | S.card ≤ D}.card

The dimension of the functions of degree at most D is at most the number of sets of at most D coordinates.

theorem Cslib.BitString.card_filter_card_le_le_pow {ι : Type u_2} [Fintype ι] (D : ℕ) : {S : Finset ι | S.card ≤ D}.card ≤ (Fintype.card ι + 1) ^ D

There are at most (n + 1) ^ D sets of at most D of the n coordinates.

theorem Cslib.BitString.card_filter_card_le_pos {ι : Type u_2} [Fintype ι] (D : ℕ) : 0 < {S : Finset ι | S.card ≤ D}.card

The empty set has at most D coordinates, so there is at least one such set.