Decomposing a function along one coordinate

The function on the cube that reads f₁ where bit i is true and f₀ where it is false is (f₀ + f₁) / 2 + χ_{i} (f₀ - f₁) / 2 (BitString.cond_eq_add_chi_mul), so its Fourier coefficient on S mixes the coefficients of f₀ and f₁ on S and on {i} ∆ S (BitString.fourierCoeff_cond). This is the step behind inductions on decision trees in Fourier analysis O'Donnell, Section 3.2. Taking for f₀ and f₁ the function f with bit i set to false and to true gives the decomposition f = Eᵢ f + χ_{i} Dᵢ f of f into its average over bit i and its derivative in i (BitString.eq_add_chi_mul_derivative) O'Donnell, Section 2.2.

Averaging over the cube the values of a function at bit i equal to false and to true is averaging the function (BitString.expect_update_false_add_update_true). The coefficient of f on {i} is the average of its derivative in i (BitString.fourierCoeff_singleton_eq_expect_derivative).

Main results

• Cslib.BitString.cond_eq_add_chi_mul, Cslib.BitString.fourierCoeff_cond: the decomposition of a branch on bit i, and its Fourier coefficients.
• Cslib.BitString.eq_add_chi_mul_derivative: the decomposition f = Eᵢ f + χ_{i} Dᵢ f.
• Cslib.BitString.expect_update_false_add_update_true: averaging over one bit.
• Cslib.BitString.fourierCoeff_singleton_eq_expect_derivative: the coefficient on {i} is the average derivative in i.

References

• R. O'Donnell, Analysis of Boolean Functions

theorem Cslib.BitString.cond_eq_add_chi_mul {ι : Type u_1} (i : ι) (f₀ f₁ : (ι → Bool) → ℝ) (x : ι → Bool) : (bif x i then f₁ x else f₀ x) = (f₀ x + f₁ x) / 2 + chi ℝ {i} x * ((f₀ x - f₁ x) / 2)

Decomposition along a bit: reading f₁ where bit i is true and f₀ where it is false is the average of f₀ and f₁ plus χ_{i} times half their difference.

theorem Cslib.BitString.eq_add_chi_mul_derivative {ι : Type u_1} [DecidableEq ι] (i : ι) (f : (ι → Bool) → ℝ) (x : ι → Bool) : f x = (f (Function.update x i false) + f (Function.update x i true)) / 2 + chi ℝ {i} x * derivative i f x

The decomposition f = Eᵢ f + χ_{i} Dᵢ f: a function is its average over bit i plus χ_{i} times its derivative in i O'Donnell, Section 2.2.

theorem Cslib.BitString.fourierCoeff_cond {ι : Type u_1} [DecidableEq ι] [Fintype ι] (i : ι) (f₀ f₁ : (ι → Bool) → ℝ) (S : Finset ι) : fourierCoeff (fun (x : ι → Bool) => bif x i then f₁ x else f₀ x) S = (fourierCoeff f₀ S + fourierCoeff f₁ S) / 2 + (fourierCoeff f₀ (symmDiff {i} S) - fourierCoeff f₁ (symmDiff {i} S)) / 2

The Fourier coefficients of a branch on bit i: the coefficient on S of the function reading f₁ where bit i is true and f₀ where it is false is the average of the coefficients of f₀ and f₁ on S, plus half the difference of their coefficients on {i} ∆ S.

theorem Cslib.BitString.expect_update_false_add_update_true {ι : Type u_1} [DecidableEq ι] [Fintype ι] (φ : (ι → Bool) → ℝ) (i : ι) : (Finset.univ.expect fun (x : ι → Bool) => φ (Function.update x i false) + φ (Function.update x i true)) = 2 * Finset.univ.expect fun (x : ι → Bool) => φ x

Averaging over one bit: averaging over the cube the sum of the values of φ at bit i equal to false and to true gives twice the average of φ.

theorem Cslib.BitString.fourierCoeff_singleton_eq_expect_derivative {ι : Type u_1} [DecidableEq ι] [Fintype ι] (i : ι) (f : (ι → Bool) → ℝ) : fourierCoeff f {i} = Finset.univ.expect fun (x : ι → Bool) => derivative i f x

The Fourier coefficient of f on {i} is the average of the derivative of f in i.