The spectral norm of decision trees

The spectral norm of a function on the cube is the sum ∑ S, |f̂ S| of the absolute values of its Fourier coefficients. A function of the output of a decision tree with values in [-1, 1] has spectral norm at most the number of leaves of the tree (DecisionTree.sum_abs_fourierCoeff_le_leafCount) [KM93] O'Donnell, Section 3.2: each node averages the coefficients of its subtrees on S and on {i} ∆ S, and S ↦ {i} ∆ S permutes the sets. Since a tree of depth d has at most 2 ^ d leaves (DecisionTree.leafCount_le_two_pow_depth), the spectral norm is also at most 2 ^ d. Together with granularity, each nonzero coefficient of a Boolean function of a tree of depth d ≥ 1 has absolute value at least 2 ^ (1 - d), so such a function has at most leafCount * 2 ^ (d - 1) nonzero coefficients (DecisionTree.card_filter_fourierCoeff_signVal_ne_zero_le) O'Donnell, Section 3.2. The leaf count and the depth are structural, so unreachable leaves and paths only weaken the bounds.

Main results

• Cslib.DecisionTree.sum_abs_fourierCoeff_le_leafCount: the spectral norm of a [-1, 1]-valued function of a decision tree is at most its number of leaves.
• Cslib.DecisionTree.sum_abs_fourierCoeff_signVal_le_leafCount, Cslib.DecisionTree.sum_abs_fourierCoeff_signVal_le_two_pow_depth: the same for Boolean functions, and the bound by 2 ^ depth.
• Cslib.DecisionTree.card_filter_fourierCoeff_signVal_ne_zero_le: the Fourier sparsity of a Boolean function of a decision tree is at most leafCount * 2 ^ (depth - 1).

References

• E. Kushilevitz and Y. Mansour, Learning decision trees using the Fourier spectrum
• R. O'Donnell, Analysis of Boolean Functions

theorem Cslib.DecisionTree.sum_abs_fourierCoeff_le_leafCount {ι : Type u_1} {β : Type u_2} [Fintype ι] [DecidableEq ι] (g : β → ℝ) (hg : ∀ (b : β), |g b| ≤ 1) (t : DecisionTree ι β) : ∑ S : Finset ι, |BitString.fourierCoeff (fun (x : ι → Bool) => g (t.eval x)) S| ≤ ↑t.leafCount

The spectral norm of a decision tree is at most its number of leaves: a function of the output of a decision tree with values in [-1, 1] has Fourier coefficients whose absolute values sum to at most the number of leaves [KM93].

theorem Cslib.DecisionTree.sum_abs_fourierCoeff_signVal_le_leafCount {ι : Type u_1} {β : Type u_2} [Fintype ι] [DecidableEq ι] (g : β → Bool) (t : DecisionTree ι β) : ∑ S : Finset ι, |BitString.fourierCoeff (fun (x : ι → Bool) => BitString.signVal (g (t.eval x))) S| ≤ ↑t.leafCount

The spectral norm of a Boolean decision tree is at most its number of leaves: a Boolean function of the output of a decision tree, read as signs, has Fourier coefficients whose absolute values sum to at most the number of leaves O'Donnell, Section 3.2.

theorem Cslib.DecisionTree.sum_abs_fourierCoeff_signVal_le_two_pow_depth {ι : Type u_1} {β : Type u_2} [Fintype ι] [DecidableEq ι] (g : β → Bool) (t : DecisionTree ι β) : ∑ S : Finset ι, |BitString.fourierCoeff (fun (x : ι → Bool) => BitString.signVal (g (t.eval x))) S| ≤ 2 ^ t.depth

A Boolean function of the output of a decision tree of depth d, read as signs, has spectral norm at most 2 ^ d.

theorem Cslib.DecisionTree.card_filter_fourierCoeff_signVal_ne_zero_le {ι : Type u_1} {β : Type u_2} [Fintype ι] [DecidableEq ι] (g : β → Bool) (t : DecisionTree ι β) : {S : Finset ι | BitString.fourierCoeff (fun (x : ι → Bool) => BitString.signVal (g (t.eval x))) S ≠ 0}.card ≤ t.leafCount * 2 ^ (t.depth - 1)

Fourier sparsity of decision trees: a Boolean function of the output of a decision tree of depth d, read as signs, has at most leafCount * 2 ^ (d - 1) nonzero Fourier coefficients, since each of them has absolute value at least 2 ^ (1 - d) (at least 1 when d = 0) O'Donnell, Section 3.2.