Maximal Fourier supports on faces of the Boolean cube

If S has a nonzero Fourier coefficient and every strict superset has coefficient zero, then every face obtained by fixing the coordinates outside S contains a nonzero value. If S is nonempty, the function is nonconstant on each such face. Differentiating in a coordinate of S reduces both claims to a smaller support.

The nonconstant-face statement is the Fourier form of the maximal-monomial observation in [Mid04], Lemma 3. A support of maximum cardinality is also maximal under inclusion, so this supplies the sensitive block used in the decision tree bound D(f) ≤ deg(f) bs(f).

Main results

• Cslib.BitString.exists_ne_zero_on_face_of_fourierCoeff_maximal: every face parallel to a maximal Fourier support contains a nonzero value.
• Cslib.BitString.exists_ne_on_face_of_fourierCoeff_maximal: a nonempty maximal Fourier support makes every parallel face nonconstant.

References

• G. Midrijanis, Exact quantum query complexity for total Boolean functions

theorem Cslib.BitString.exists_ne_zero_on_face_of_fourierCoeff_maximal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : Finset ι) (f : (ι → Bool) → ℝ) : fourierCoeff f S ≠ 0 → (∀ (T : Finset ι), S ⊂ T → fourierCoeff f T = 0) → ∀ (x : ι → Bool), ∃ (y : ι → Bool), (∀ i ∉ S, y i = x i) ∧ f y ≠ 0

A maximal nonzero Fourier coefficient forces a nonzero value on every face obtained by fixing the coordinates outside its support.

theorem Cslib.BitString.exists_ne_on_face_of_fourierCoeff_maximal {ι : Type u_1} [Fintype ι] [DecidableEq ι] {S : Finset ι} (hS : S.Nonempty) {f : (ι → Bool) → ℝ} (hf : fourierCoeff f S ≠ 0) (hmax : ∀ (T : Finset ι), S ⊂ T → fourierCoeff f T = 0) (x : ι → Bool) : ∃ (y : ι → Bool), (∀ i ∉ S, y i = x i) ∧ f y ≠ f x

A nonempty maximal Fourier support makes every parallel face nonconstant. This is the Fourier form of [Mid04], Lemma 3.