Midrijanis's degree bound for deterministic query complexity

For every total Boolean function, D(f) ≤ deg(f) bs(f) [Mid04], proof of Theorem 4. Choose a nonzero Fourier support S with |S| = deg(f) and query all its coordinates. Every face parallel to S is nonconstant, so every input has a sensitive block contained in S (QueryComplexity.exists_card_eq_degree_forall_exists_isSensitiveBlock_subset). After fixing the answers, this block is disjoint from the sensitive blocks on the remaining coordinates. Block sensitivity therefore drops by at least one. Restriction cannot increase the degree, and induction on block sensitivity bounds the total number of queries by deg(f) bs(f).

The Nisan–Szegedy inequality bs(f) ≤ 2 deg(f)² then gives D(f) ≤ 2 deg(f)³, the conclusion of [Mid04], Theorem 4. All measures are those of total Boolean functions on Fin n → Bool; decision tree complexity counts the maximum number of queried coordinates along a branch.

Main results

• Cslib.QueryComplexity.exists_card_eq_degree_forall_exists_isSensitiveBlock_subset: a nonconstant function has a set of deg(f) coordinates containing a sensitive block at every input, the maximal-monomial property of [Mid04], Lemma 3.
• Cslib.DecisionTree.complexity_le_degree_mul_blockSensitivity: D(f) ≤ deg(f) bs(f).
• Cslib.DecisionTree.complexity_le_two_mul_degree_pow_three: D(f) ≤ 2 deg(f)³.

References

• G. Midrijanis, Exact quantum query complexity for total Boolean functions, Lemma 3 and Theorem 4, arXiv version 2, pp. 3–4.
• N. Nisan, M. Szegedy, On the degree of Boolean functions as real polynomials

theorem Cslib.QueryComplexity.exists_card_eq_degree_forall_exists_isSensitiveBlock_subset {n : ℕ} (f : BooleanFunction n) (hf : degree f ≠ 0) : ∃ (S : Finset (Fin n)), S.card = degree f ∧ ∀ (x : BitString n), ∃ B ⊆ S, IsSensitiveBlock f x B

A nonconstant Boolean function has a set of deg(f) coordinates containing a sensitive block at every input. This is the maximal-monomial property of [Mid04], Lemma 3, expressed using the equivalent Fourier degree.

theorem Cslib.DecisionTree.complexity_le_degree_mul_blockSensitivity {n : ℕ} (f : BooleanFunction n) : complexity f ≤ QueryComplexity.degree f * QueryComplexity.blockSensitivity f

Midrijanis's bound: D(f) ≤ deg(f) bs(f) for every total Boolean function [Mid04], proof of Theorem 4. Querying a maximum-degree monomial lowers block sensitivity by at least one at every input.

theorem Cslib.DecisionTree.complexity_le_two_mul_degree_pow_three {n : ℕ} (f : BooleanFunction n) : complexity f ≤ 2 * QueryComplexity.degree f ^ 3

The cubic degree bound: D(f) ≤ 2 deg(f)³ for every total Boolean function [Mid04], Theorem 4.