Decision trees have low Fourier degree

A function computed by a decision tree of depth d has no Fourier weight above degree d (DecisionTree.fourierCoeff_eq_zero_of_depth_lt) O'Donnell, Chapter 3. This follows from DecisionTree.comp_eval_mem_lowDegree and BitString.fourierCoeff_eq_zero_of_mem_lowDegree. At each node querying i, the computed function is (f₀ + f₁) / 2 + χ_{i} (f₀ - f₁) / 2 in terms of the functions f₀ and f₁ of its subtrees, so its coefficient on S is given by the coefficients of f₀ and f₁ on S and on {i} ∆ S (DecisionTree.fourierCoeff_eval_node).

Main results

• Cslib.DecisionTree.fourierCoeff_eval_node: the Fourier coefficients at a node in terms of those of the subtrees.
• Cslib.DecisionTree.fourierCoeff_eq_zero_of_depth_lt: decision trees of depth d have Fourier degree at most d.

References

• R. O'Donnell, Analysis of Boolean Functions

theorem Cslib.DecisionTree.fourierCoeff_eval_node {ι : Type u_1} {β : Type u_2} [Fintype ι] [DecidableEq ι] (g : β → ℝ) (i : ι) (t₀ t₁ : DecisionTree ι β) (S : Finset ι) : BitString.fourierCoeff (fun (x : ι → Bool) => g ((node i t₀ t₁).eval x)) S = (BitString.fourierCoeff (fun (x : ι → Bool) => g (t₀.eval x)) S + BitString.fourierCoeff (fun (x : ι → Bool) => g (t₁.eval x)) S) / 2 + (BitString.fourierCoeff (fun (x : ι → Bool) => g (t₀.eval x)) (symmDiff {i} S) - BitString.fourierCoeff (fun (x : ι → Bool) => g (t₁.eval x)) (symmDiff {i} S)) / 2

The Fourier coefficients at a node: the coefficient on S of a function of the output of a node querying i is the average of the coefficients of the functions of its subtrees on S, plus half the difference of their coefficients on {i} ∆ S.

theorem Cslib.DecisionTree.fourierCoeff_eq_zero_of_depth_lt {ι : Type u_1} {β : Type u_2} [Fintype ι] [DecidableEq ι] (g : β → ℝ) (t : DecisionTree ι β) {S : Finset ι} (hS : t.depth < S.card) : BitString.fourierCoeff (fun (x : ι → Bool) => g (t.eval x)) S = 0

Decision trees have low Fourier degree: a function of the output of a decision tree of depth d has no Fourier weight on sets of more than d coordinates.