Decision-tree lower bounds from query-complexity measures

CSLib supplies sensitivity, block sensitivity and certificate complexity, including s(f) ≤ bs(f) ≤ C(f). The variables a tree queries at an input form a certificate, so C(f) ≤ D(f) [Nis91], Jukna, Section 14.3.

The numerical measures use CSLib's BooleanFunction n. The coordinate-witness lower bound card_le_complexity_of_forall_update_ne also applies to arbitrary finite coordinate types and arbitrary outputs, without introducing a second family of measures.

Main results

• Cslib.DecisionTree.subset_queries_of_forall_update_ne: a tree must query every coordinate whose flip changes its output.
• Cslib.DecisionTree.card_le_complexity_of_forall_update_ne: sensitive coordinates give a lower bound for arbitrary output types.
• Cslib.DecisionTree.certificateComplexity_le_complexity: C(f) ≤ D(f).
• Cslib.DecisionTree.sensitivityAt_le_complexity: sensitivity at any input bounds D(f) below.

References

• N. Nisan, CREW PRAMs and decision trees
• S. Jukna, Boolean Function Complexity: Advances and Frontiers

theorem Cslib.DecisionTree.subset_queries_of_forall_update_ne {ι : Type u_1} {β : Type u_2} [DecidableEq ι] {f : (ι → Bool) → β} {t : DecisionTree ι β} (ht : t.Computes f) {x : ι → Bool} {S : Finset ι} (hS : ∀ i ∈ S, f (Function.update x i !x i) ≠ f x) : S ⊆ t.queries x

A tree must query every coordinate whose flip changes the function's value at x. The coordinates and outputs need not be finite.

theorem Cslib.DecisionTree.card_le_complexity_of_forall_update_ne {ι : Type u_1} {β : Type u_2} [DecidableEq ι] [Finite ι] {f : (ι → Bool) → β} {x : ι → Bool} {S : Finset ι} (hS : ∀ i ∈ S, f (Function.update x i !x i) ≠ f x) : S.card ≤ complexity f

Exhibiting sensitive coordinates bounds decision tree complexity below, for any output type.

theorem Cslib.DecisionTree.complexity_eq_card_of_forall_update_ne {ι : Type u_1} {β : Type u_2} [DecidableEq ι] [Fintype ι] {f : (ι → Bool) → β} {x : ι → Bool} (h : ∀ (i : ι), f (Function.update x i !x i) ≠ f x) : complexity f = Fintype.card ι

Sensitivity to every coordinate forces a tree to query all of them in the worst case.

theorem Cslib.DecisionTree.isCertificate_queries {n : ℕ} {f : BooleanFunction n} {t : DecisionTree (Fin n) Bool} (ht : t.Computes f) (x : BitString n) : QueryComplexity.IsCertificate f x (t.queries x)

The coordinates queried at an input certify the output of the tree.

theorem Cslib.DecisionTree.certificateComplexityAt_le_depth {n : ℕ} {f : BooleanFunction n} {t : DecisionTree (Fin n) Bool} (ht : t.Computes f) (x : BitString n) : QueryComplexity.certificateComplexityAt f x ≤ t.depth

Certificate complexity at an input is at most the depth of any tree computing the function.

theorem Cslib.DecisionTree.certificateComplexity_le_complexity {n : ℕ} (f : BooleanFunction n) : QueryComplexity.certificateComplexity f ≤ complexity f

Certificate complexity is at most decision tree complexity.

theorem Cslib.DecisionTree.sensitivityAt_le_complexity {n : ℕ} (f : BooleanFunction n) (x : BitString n) : BitString.sensitivityAt f x ≤ complexity f

A lower bound on sensitivity at one input is a lower bound on decision tree complexity.

theorem Cslib.DecisionTree.complexity_eq_card_of_sensitivityAt_eq_card {n : ℕ} {f : BooleanFunction n} {x : BitString n} (h : BitString.sensitivityAt f x = n) : complexity f = n

A function sensitive to every variable at some input needs to query all of them.