Fourier coefficients of Boolean functions read as bits

A Boolean function F can be read as a real function with values 0 and 1 (fun x => bitVal ℝ (F x)) or with values ±1 (fun x => signVal (F x)). Since signVal b = 1 - 2 bitVal b, the two readings differ by an affine change, so away from the empty set their Fourier coefficients differ by the factor -1 / 2 (Cslib.BitString.fourierCoeff_bitVal_of_nonempty). In particular the Fourier weight above any level of the 0/1 reading is a quarter of that of the ±1 reading (Cslib.BitString.sum_fourierCoeff_bitVal_sq). Fourier tail bounds such as the Linial, Mansour and Nisan bound are usually stated for the ±1 reading, while their applications, such as Braverman, approximate the 0/1 reading.

Cutting the Fourier expansion of a function at level t gives a function of degree at most t whose squared L² distance to the original is the Fourier weight above t (Cslib.BitString.exists_mem_lowDegree_expect_sq_sub_eq, from Parseval's identity in the form Cslib.BitString.expect_sq_sub_sum_mul_chi), so a Fourier tail bound on a Boolean function yields a low-degree L² approximation of its 0/1 reading (Cslib.BitString.exists_mem_lowDegree_expect_sq_bitVal_sub_eq).

Main results

• Cslib.BitString.fourierCoeff_bitVal_of_nonempty: the coefficients of the 0/1 reading at a nonempty set are -1 / 2 times those of the ±1 reading.
• Cslib.BitString.sum_fourierCoeff_bitVal_sq: the Fourier weight of the 0/1 reading above a level is a quarter of that of the ±1 reading.
• Cslib.BitString.exists_mem_lowDegree_expect_sq_sub_eq, Cslib.BitString.exists_mem_lowDegree_expect_sq_bitVal_sub_eq: Fourier truncation.

References

• N. Linial, Y. Mansour, N. Nisan, Constant depth circuits, Fourier transform, and learnability
• M. Braverman, Polylogarithmic independence fools AC⁰ circuits

theorem Cslib.BitString.fourierCoeff_bitVal_of_nonempty {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : (ι → Bool) → Bool) {S : Finset ι} (hS : S.Nonempty) : fourierCoeff (fun (x : ι → Bool) => bitVal ℝ (F x)) S = -fourierCoeff (fun (x : ι → Bool) => signVal (F x)) S / 2

At a nonempty set, the Fourier coefficient of a Boolean function read as 0 or 1 is -1 / 2 times its coefficient when read as a sign.

theorem Cslib.BitString.sum_fourierCoeff_bitVal_sq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : (ι → Bool) → Bool) (t : ℕ) : ∑ S : Finset ι with t < S.card, fourierCoeff (fun (x : ι → Bool) => bitVal ℝ (F x)) S ^ 2 = (∑ S : Finset ι with t < S.card, fourierCoeff (fun (x : ι → Bool) => signVal (F x)) S ^ 2) / 4

Normalizing Fourier tails: above any level t, the Fourier weight of a Boolean function read as 0 or 1 is a quarter of its weight when read as a sign.

theorem Cslib.BitString.exists_mem_lowDegree_expect_sq_sub_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) (t : ℕ) : ∃ g ∈ lowDegree ℝ ι t, (Finset.univ.expect fun (x : ι → Bool) => (f x - g x) ^ 2) = ∑ S : Finset ι with t < S.card, fourierCoeff f S ^ 2

Fourier truncation: cutting the Fourier expansion of f at level t gives a function of degree at most t whose squared L² distance to f is the Fourier weight of f above t.

theorem Cslib.BitString.exists_mem_lowDegree_expect_sq_bitVal_sub_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : (ι → Bool) → Bool) (t : ℕ) : ∃ g ∈ lowDegree ℝ ι t, (Finset.univ.expect fun (x : ι → Bool) => (bitVal ℝ (F x) - g x) ^ 2) = (∑ S : Finset ι with t < S.card, fourierCoeff (fun (x : ι → Bool) => signVal (F x)) S ^ 2) / 4

Fourier truncation of a Boolean function: the 0/1 reading of F is approximated by a function of degree at most t with squared L² error a quarter of the Fourier weight of the ±1 reading of F above t.