Convolution on the Boolean cube

Bit strings add coordinatewise modulo two, (x + y) i = (x i ^^ y i), through Mathlib's Boolean ring structure on Bool. Adding a fixed string permutes the cube, so the uniform expectation is translation invariant (Fintype.expect_add_left), and the characters turn sums into products (BitString.chi_add). The convolution of two real functions on the cube averages f y * g (x + y) over y (BitString.convolution); it is commutative (BitString.convolution_comm), and its Fourier coefficients are the products of the coefficients of the factors (BitString.fourierCoeff_convolution) O'Donnell, Section 1.5.

Main definitions

• Cslib.BitString.convolution: the convolution of two real functions on the cube.

Main results

• Cslib.BitString.convolution_comm: convolution is commutative.
• Cslib.BitString.fourierCoeff_convolution: the convolution theorem.

References

• R. O'Donnell, Analysis of Boolean Functions

noncomputable def Cslib.BitString.convolution {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f g : (ι → Bool) → ℝ) (x : ι → Bool) : ℝ

The convolution of two real functions on the cube: (f ∗ g) x = 𝔼_y f y * g (x + y) O'Donnell, Definition 1.24.

theorem Cslib.BitString.convolution_comm {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f g : (ι → Bool) → ℝ) : convolution f g = convolution g f

Convolution is commutative.

theorem Cslib.BitString.fourierCoeff_convolution {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f g : (ι → Bool) → ℝ) (S : Finset ι) : fourierCoeff (convolution f g) S = fourierCoeff f S * fourierCoeff g S

The convolution theorem: the Fourier coefficients of a convolution are the products of the Fourier coefficients of the factors O'Donnell, Theorem 1.27.