Total degree and Fourier degree on the Boolean cube

Every function f on the cube ι → Bool with values in a commutative ring R is a unique R-linear combination of the monomials ∏_{i ∈ S} xᵢ, its multilinear representation. Its total degree BitString.totalDegree f is the least D such that f is a combination of monomials of at most D coordinates, that is, the least D with f ∈ BitString.lowDegree R ι D (BitString.totalDegree_le_iff_mem_lowDegree); by BitString.lowDegree_eq_map_restrictTotalDegree it is also the least total degree of a polynomial that agrees with f on the cube.

Over a field F in which 2 is invertible, the characters chi F S and the monomials of at most D coordinates span the same functions (BitString.chi_mem_lowDegree, BitString.lowDegree_le_signSpan). Over ℝ, low degree is therefore the vanishing of the Fourier coefficients on sets of more than D coordinates (BitString.mem_lowDegree_iff_fourierCoeff_eq_zero), and the total degree is the largest size of a set with a nonzero Fourier coefficient (BitString.totalDegree_le_iff_fourierCoeff_eq_zero, BitString.exists_card_eq_totalDegree_fourierCoeff_ne_zero) [NS94], [OD14].

Main definitions

• Cslib.BitString.signSpan: the span of the characters of at most H coordinates.
• Cslib.BitString.totalDegree: the total degree of a function on the cube.

Main results

• Cslib.BitString.chi_mem_lowDegree, Cslib.BitString.lowDegree_le_signSpan: characters of at most H coordinates and monomials of at most H coordinates span the same space when 2 is invertible.
• Cslib.BitString.totalDegree_le_iff_mem_lowDegree: the total degree is the least D with f ∈ lowDegree R ι D.
• Cslib.BitString.mem_lowDegree_iff_fourierCoeff_eq_zero: over ℝ, low degree is the vanishing of the Fourier coefficients on larger sets.
• Cslib.BitString.totalDegree_le_iff_fourierCoeff_eq_zero, Cslib.BitString.exists_card_eq_totalDegree_fourierCoeff_ne_zero: the total degree over ℝ is the largest size of a set with a nonzero Fourier coefficient.
• Cslib.BitString.signVal_comp_mem_lowDegree_iff, Cslib.BitString.totalDegree_signVal_comp: reading a Boolean function as 0/1 or as ±1 gives the same degree over ℝ.

References

• N. Nisan, M. Szegedy, On the degree of Boolean functions as real polynomials
• R. O'Donnell, Analysis of Boolean Functions

The span of characters

def Cslib.BitString.signSpan (F : Type u_1) [Field F] (ι : Type u_2) (H : ℕ) : Submodule F ((ι → Bool) → F)

The span of the characters of the sets of at most H coordinates.

theorem Cslib.BitString.chi_mem_lowDegree {F : Type u_1} [Field F] {ι : Type u_2} (S : Finset ι) : chi F S ∈ lowDegree F ι S.card

The character of S has degree at most |S|.

theorem Cslib.BitString.signSpan_mono {F : Type u_1} [Field F] {ι : Type u_2} {H K : ℕ} (hHK : H ≤ K) : signSpan F ι H ≤ signSpan F ι K

The span of the characters of at most H coordinates grows with H.

theorem Cslib.BitString.monomial_mem_signSpan {F : Type u_1} [Field F] {ι : Type u_2} [Invertible 2] (S : Finset ι) : monomial F S ∈ signSpan F ι S.card

Each monomial expands into characters of its subsets.

theorem Cslib.BitString.lowDegree_le_signSpan {F : Type u_1} [Field F] {ι : Type u_2} [Invertible 2] (H : ℕ) : lowDegree F ι H ≤ signSpan F ι H

When 2 is invertible in F, every function of degree at most H lies in the span of the characters of at most H coordinates.

Total degree over a commutative ring

noncomputable def Cslib.BitString.totalDegree {R : Type u_1} [CommRing R] {ι : Type u_2} (f : (ι → Bool) → R) : ℕ

The total degree of a function on the cube: the least D such that f is an R-linear combination of monomials of at most D coordinates, the degree of its multilinear representation. It is 0 when there is no such D, which can only happen over infinitely many coordinates.

theorem Cslib.BitString.totalDegree_le_of_mem_lowDegree {R : Type u_1} [CommRing R] {ι : Type u_2} {f : (ι → Bool) → R} {D : ℕ} (h : f ∈ lowDegree R ι D) : totalDegree f ≤ D

theorem Cslib.BitString.mem_lowDegree_totalDegree {R : Type u_1} [CommRing R] {ι : Type u_2} [Finite ι] (f : (ι → Bool) → R) : f ∈ lowDegree R ι (totalDegree f)

A function on finitely many coordinates is a combination of monomials of at most its total degree coordinates.

theorem Cslib.BitString.totalDegree_le_iff_mem_lowDegree {R : Type u_1} [CommRing R] {ι : Type u_2} {f : (ι → Bool) → R} {D : ℕ} [Finite ι] : totalDegree f ≤ D ↔ f ∈ lowDegree R ι D

Total degree as low degree: the total degree is at most D exactly when f is a combination of monomials of at most D coordinates.

theorem Cslib.BitString.totalDegree_le_card {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] (f : (ι → Bool) → R) : totalDegree f ≤ Fintype.card ι

The total degree is at most the number of coordinates.

theorem Cslib.BitString.totalDegree_comp_not {R : Type u_1} [CommRing R] {ι : Type u_2} (f : (ι → Bool) → R) : (totalDegree fun (x : ι → Bool) => f fun (i : ι) => !x i) = totalDegree f

Negating every input bit preserves the total degree.

Total degree and Fourier coefficients

theorem Cslib.BitString.fourierCoeff_eq_zero_of_mem_lowDegree {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → ℝ} {D : ℕ} (hf : f ∈ lowDegree ℝ ι D) {S : Finset ι} (hS : D < S.card) : fourierCoeff f S = 0

A function of total degree at most D has no Fourier weight on sets of more than D coordinates.

theorem Cslib.BitString.mem_lowDegree_iff_fourierCoeff_eq_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → ℝ} {D : ℕ} : f ∈ lowDegree ℝ ι D ↔ ∀ (S : Finset ι), D < S.card → fourierCoeff f S = 0

Low degree is Fourier degree: a real function is a combination of monomials of at most D coordinates exactly when its Fourier coefficients on sets of more than D coordinates vanish.

theorem Cslib.BitString.card_le_totalDegree_of_fourierCoeff_ne_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → ℝ} {S : Finset ι} (h : fourierCoeff f S ≠ 0) : S.card ≤ totalDegree f

A nonzero Fourier coefficient bounds the total degree below.

theorem Cslib.BitString.totalDegree_le_iff_fourierCoeff_eq_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → ℝ} {D : ℕ} : totalDegree f ≤ D ↔ ∀ (S : Finset ι), D < S.card → fourierCoeff f S = 0

The total degree of a real function is at most D exactly when its Fourier coefficients vanish on the sets of more than D coordinates.

theorem Cslib.BitString.exists_card_eq_totalDegree_fourierCoeff_ne_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → ℝ} (h : totalDegree f ≠ 0) : ∃ (S : Finset ι), S.card = totalDegree f ∧ fourierCoeff f S ≠ 0

The total degree is attained: a real function of positive total degree has a nonzero Fourier coefficient on a set of exactly its total degree coordinates.

theorem Cslib.BitString.signVal_comp_mem_lowDegree_iff {ι : Type u_1} {D : ℕ} {g : (ι → Bool) → Bool} : (fun (x : ι → Bool) => signVal (g x)) ∈ lowDegree ℝ ι D ↔ (fun (x : ι → Bool) => bitVal ℝ (g x)) ∈ lowDegree ℝ ι D

Reading the values of a Boolean function as 0 and 1 or as the signs ±1 gives the same low-degree membership: signVal b = 1 - 2 bitVal ℝ b.

theorem Cslib.BitString.totalDegree_signVal_comp {ι : Type u_1} (g : (ι → Bool) → Bool) : (totalDegree fun (x : ι → Bool) => signVal (g x)) = totalDegree fun (x : ι → Bool) => bitVal ℝ (g x)

Reading the values of a Boolean function as 0 and 1 or as the signs ±1 gives the same total degree: signVal b = 1 - 2 bitVal ℝ b.