Documentation

Complexity.Computability.QueryComplexity.Degree

The degree of a Boolean function #

The degree deg(f) of a Boolean function is the total degree of its values 0 and 1 read in ℝ (QueryComplexity.degree), that is, the least D such that f is a real combination of monomials of at most D coordinates (QueryComplexity.degree_le_iff_mem_lowDegree) [NS94], [BdW02]. Reading the values as the signs ±1 gives the same degree (QueryComplexity.degree_eq_totalDegree_signVal), and so does negating the output or the input bits (QueryComplexity.degree_not, QueryComplexity.degree_comp_not). A decision tree of depth d computes a function of total degree at most d over any commutative ring, since a node querying i computes (1 - xᵢ) f₀ + xᵢ f₁ from the functions f₀ and f₁ of its subtrees (DecisionTree.comp_eval_mem_lowDegree), so deg(f) ≤ D(f) (DecisionTree.degree_le_complexity). Parity, conjunction and disjunction of n bits have degree n.

The general theory of BitString.totalDegree and the equivalence between BitString.lowDegree ℝ ι D and Fourier degree on the cube live in Complexity.Foundations.BooleanAnalysis.Degree.

Main definitions #

Main results #

References #

source
theorem Cslib.DecisionTree.comp_eval_mem_lowDegree {R : Type u_1} [CommRing R] {ι : Type u_2} {β : Type u_3} (g : β → R) (t : DecisionTree ι β) :
(fun (x : ι → Bool) => g (t.eval x)) ∈ BitString.lowDegree R ι t.depth

Decision trees compute low-degree functions: a function of the output of a decision tree of depth d is a combination of monomials of at most d coordinates, over any commutative ring.

source
theorem Cslib.DecisionTree.totalDegree_comp_eval_le {R : Type u_1} [CommRing R] {ι : Type u_2} {β : Type u_3} (g : β → R) (t : DecisionTree ι β) :
(BitString.totalDegree fun (x : ι → Bool) => g (t.eval x)) ≤ t.depth

A function of the output of a decision tree has total degree at most the depth of the tree.

source
noncomputable def Cslib.QueryComplexity.degree {n : ℕ} (f : BooleanFunction n) :
ℕ

The degree deg(f) of a Boolean function: the degree of the unique multilinear real polynomial that agrees with f on {0,1}ⁿ, reading the values of f as 0 and 1.

Instances For
    source
    theorem Cslib.QueryComplexity.degree_le_iff_mem_lowDegree {n : ℕ} {f : BooleanFunction n} {D : ℕ} :
    degree f ≤ D ↔ (fun (x : BitString n) => BitString.bitVal ℝ (f x)) ∈ BitString.lowDegree ℝ (Fin n) D

    deg(f) ≤ D exactly when f, read with values 0 and 1, is a real combination of monomials of at most D coordinates.

    source
    theorem Cslib.QueryComplexity.degree_eq_totalDegree_signVal {n : ℕ} (f : BooleanFunction n) :
    degree f = BitString.totalDegree fun (x : Fin n → Bool) => BitString.signVal (f x)

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

    source
    theorem Cslib.QueryComplexity.degree_le_card {n : ℕ} (f : BooleanFunction n) :
    degree f ≤ n

    deg(f) ≤ n.

    source
    theorem Cslib.QueryComplexity.degree_not {n : ℕ} (f : BooleanFunction n) :
    (degree fun (x : BitString n) => !f x) = degree f

    Negating a Boolean function preserves its degree: bitVal (!b) = 1 - bitVal b.

    source
    theorem Cslib.QueryComplexity.degree_comp_not {n : ℕ} (f : BooleanFunction n) :
    (degree fun (x : BitString n) => f fun (i : Fin n) => !x i) = degree f

    Negating every input bit of a Boolean function preserves its degree.

    source
    theorem Cslib.QueryComplexity.card_le_degree_of_fourierCoeff_ne_zero {n : ℕ} {f : BooleanFunction n} {S : Finset (Fin n)} (h : BitString.fourierCoeff (fun (x : Fin n → Bool) => BitString.signVal (f x)) S ≠ 0) :
    S.card ≤ degree f

    A nonzero Fourier coefficient of f, read as signs, bounds deg(f) below.

    source
    theorem Cslib.QueryComplexity.degree_parity {n : ℕ} :
    degree (parity n) = n

    Parity of n bits has degree n: read as signs, it is the character of all coordinates.

    source
    theorem Cslib.QueryComplexity.degree_threshold_self {n : ℕ} :
    degree (threshold n n) = n

    The conjunction of n bits has degree n: read with values 0 and 1, it is the monomial of all coordinates, whose top Fourier coefficient is (-1)ⁿ / 2ⁿ.

    source
    theorem Cslib.QueryComplexity.degree_threshold_one_right {n : ℕ} :
    degree (threshold n 1) = n

    The disjunction of n bits has degree n: it is the negation of the conjunction of the negated bits.

    source
    theorem Cslib.DecisionTree.degree_le_complexity {n : ℕ} (f : BooleanFunction n) :
    QueryComplexity.degree f ≤ complexity f

    Degree is at most decision tree complexity: deg(f) ≤ D(f).