Granularity of the Fourier coefficients of decision trees

An integer-valued function of the output of a decision tree of depth d has Fourier coefficients that are integer multiples of 2 ^ (-d) (DecisionTree.exists_fourierCoeff_eq_intCast_div_two_pow_depth): a leaf has integer coefficients, and each node averages coefficients of its subtrees, halving the denominator. A bit read as a sign is signVal b = 1 - 2 [b], one minus twice an integer, so a Boolean function computed by a decision tree of depth d ≥ 1, read as signs, has coefficients in 2 ^ (1 - d) ℤ, and one computed by a tree of depth 0 has integer coefficients (DecisionTree.exists_fourierCoeff_signVal_eq_intCast_div_two_pow_depth_sub_one) O'Donnell, Section 3.2. The depth is structural, so unreachable paths only weaken the bound.

Main results

• Cslib.DecisionTree.exists_fourierCoeff_eq_intCast_div_two_pow_depth: granularity for integer-valued functions of decision trees.
• Cslib.DecisionTree.exists_fourierCoeff_signVal_eq_intCast_div_two_pow_depth_sub_one: granularity for Boolean functions of decision trees.

References

• R. O'Donnell, Analysis of Boolean Functions

theorem Cslib.DecisionTree.exists_fourierCoeff_eq_intCast_div_two_pow_depth {ι : Type u_1} {β : Type u_2} [Fintype ι] [DecidableEq ι] (g : β → ℤ) (t : DecisionTree ι β) (S : Finset ι) : ∃ (m : ℤ), BitString.fourierCoeff (fun (x : ι → Bool) => ↑(g (t.eval x))) S = ↑m / 2 ^ t.depth

Granularity of decision trees: the Fourier coefficients of an integer-valued function of the output of a decision tree of depth d are integer multiples of 2 ^ (-d).

theorem Cslib.DecisionTree.exists_fourierCoeff_signVal_eq_intCast_div_two_pow_depth_sub_one {ι : Type u_1} {β : Type u_2} [Fintype ι] [DecidableEq ι] (g : β → Bool) (t : DecisionTree ι β) (S : Finset ι) : ∃ (m : ℤ), BitString.fourierCoeff (fun (x : ι → Bool) => BitString.signVal (g (t.eval x))) S = ↑m / 2 ^ (t.depth - 1)

Granularity of decision trees for Boolean functions: a Boolean function of the output of a decision tree of depth d, read as signs, has Fourier coefficients in 2 ^ (1 - d) ℤ when d ≥ 1, and integer coefficients when d = 0 O'Donnell, Section 3.2.