Fourier coefficients of restrictions

Fixing the coordinates outside a set J to the bits of z turns f into the function x ↦ f (J.piecewise x z) of the coordinates in J. Its Fourier coefficient on S collects the coefficients of f on the sets U with U ∩ J = S, twisted by the characters of U \ J at z (BitString.fourierCoeff_piecewise). Averaged over a uniformly random z, the twists are orthogonal, so the expected squared coefficient on S is the weight of f on the sets meeting J in S (BitString.expect_fourierCoeff_piecewise_sq), and the expected weight of the restriction on sets of at least m coordinates is the weight of f on the sets meeting J in at least m coordinates (BitString.expect_sum_fourierCoeff_piecewise_sq) O'Donnell, Section 3.3.

Averaging over the fixed bits instead of over their squares averages the twists away: the average of f over the coordinates outside J keeps the coefficients of f on the subsets of J and kills the others (BitString.fourierCoeff_expect_piecewise), so it is the part of the Fourier expansion of f on the subsets of J (BitString.expect_piecewise_eq_sum), at mean square distance from f the weight of f outside the subsets of J (BitString.expect_sub_expect_piecewise_sq).

Main results

• Cslib.BitString.fourierCoeff_piecewise: the coefficients of a restriction.
• Cslib.BitString.expect_sum_fourierCoeff_piecewise_sq: the expected weight of a restriction above a degree.
• Cslib.BitString.fourierCoeff_expect_piecewise, Cslib.BitString.expect_piecewise_eq_sum: the average over the coordinates outside a set.
• Cslib.BitString.expect_sub_expect_piecewise_sq: the mean square distance of a function from that average is its Fourier weight outside the subsets of the set.

References

• R. O'Donnell, Analysis of Boolean Functions

theorem Cslib.BitString.chi_piecewise {ι : Type u_1} [DecidableEq ι] {R : Type u_2} [CommRing R] (U J : Finset ι) (x z : ι → Bool) : chi R U (J.piecewise x z) = chi R (U ∩ J) x * chi R (U \ J) z

A character at a point with the coordinates outside J replaced splits into the characters of the parts of U inside and outside J.

theorem Cslib.BitString.fourierCoeff_piecewise {ι : Type u_1} [DecidableEq ι] [Fintype ι] (f : (ι → Bool) → ℝ) (J : Finset ι) (z : ι → Bool) (S : Finset ι) : fourierCoeff (fun (x : ι → Bool) => f (J.piecewise x z)) S = ∑ U : Finset ι with U ∩ J = S, fourierCoeff f U * chi ℝ (U \ J) z

The Fourier coefficients of a restriction: the coefficient on S sums the coefficients of f on the sets meeting J in S, each multiplied by the character of its part outside J at z.

theorem Cslib.BitString.expect_fourierCoeff_piecewise_sq {ι : Type u_1} [DecidableEq ι] [Fintype ι] (f : (ι → Bool) → ℝ) (J S : Finset ι) : (Finset.univ.expect fun (z : ι → Bool) => fourierCoeff (fun (x : ι → Bool) => f (J.piecewise x z)) S ^ 2) = ∑ U : Finset ι with U ∩ J = S, fourierCoeff f U ^ 2

Averaged over the fixed bits, the squared coefficient of a restriction on S is the weight of f on the sets meeting J in S.

theorem Cslib.BitString.expect_sum_fourierCoeff_piecewise_sq {ι : Type u_1} [DecidableEq ι] [Fintype ι] (f : (ι → Bool) → ℝ) (J : Finset ι) (m : ℕ) : (Finset.univ.expect fun (z : ι → Bool) => ∑ S : Finset ι with m ≤ S.card, fourierCoeff (fun (x : ι → Bool) => f (J.piecewise x z)) S ^ 2) = ∑ U : Finset ι with m ≤ (U ∩ J).card, fourierCoeff f U ^ 2

The expected weight of a restriction above a degree: averaged over the fixed bits, the Fourier weight of the restriction on sets of at least m coordinates is the weight of f on the sets meeting J in at least m coordinates.

Averaging out the coordinates outside a set

theorem Cslib.BitString.fourierCoeff_expect_piecewise {ι : Type u_1} [DecidableEq ι] [Fintype ι] (f : (ι → Bool) → ℝ) (J S : Finset ι) : fourierCoeff (fun (x : ι → Bool) => Finset.univ.expect fun (z : ι → Bool) => f (J.piecewise x z)) S = if S ⊆ J then fourierCoeff f S else 0

The Fourier coefficients of the average over the coordinates outside J: averaging keeps the coefficients on the subsets of J and kills the others.

theorem Cslib.BitString.expect_piecewise_eq_sum {ι : Type u_1} [DecidableEq ι] [Fintype ι] (f : (ι → Bool) → ℝ) (J : Finset ι) (x : ι → Bool) : (Finset.univ.expect fun (z : ι → Bool) => f (J.piecewise x z)) = ∑ S : Finset ι with S ⊆ J, fourierCoeff f S * chi ℝ S x

The average over the coordinates outside J is the part of the Fourier expansion on the subsets of J.

theorem Cslib.BitString.expect_sub_expect_piecewise_sq {ι : Type u_1} [DecidableEq ι] [Fintype ι] (f : (ι → Bool) → ℝ) (J : Finset ι) : (Finset.univ.expect fun (x : ι → Bool) => (f x - Finset.univ.expect fun (z : ι → Bool) => f (J.piecewise x z)) ^ 2) = ∑ S : Finset ι with ¬S ⊆ J, fourierCoeff f S ^ 2

The mean square distance from f to its average over the coordinates outside J is the Fourier weight of f outside the subsets of J.