The Bonami Lemma

A real function f on the cube has degree at most k when f ∈ BitString.lowDegree ℝ ι k, equivalently when its Fourier coefficients on the sets of more than k coordinates vanish (BitString.mem_lowDegree_iff_fourierCoeff_eq_zero). The Bonami Lemma says that low-degree functions of uniformly random bits are reasonable: if f has degree at most k, then 𝔼 f ^ 4 ≤ 9 ^ k (𝔼 f ^ 2) ^ 2, that is, ‖f‖_4 ≤ √3 ^ k ‖f‖_2 (BitString.expect_pow_four_le) [Bon70] O'Donnell, Section 9.1. More generally ‖f‖_q ≤ √(q - 1) ^ k ‖f‖_2 for every q ≥ 2 (BitString.lpNorm_le_sqrt_pow_mul_lpNorm_two) O'Donnell, Theorem 9.21.

The proof follows O'Donnell's derivation of Theorem 9.21 from the (2, q)-Hypercontractivity Theorem, rather than his induction on the number of coordinates for the case q = 4. With c = √(q - 1), the function g with coefficients c ^ |S| f̂(S) satisfies T_{1/c} g = f, so ‖f‖_q ≤ ‖g‖_2 (BitString.lpNorm_noiseOp_le_lpNorm_two), and ‖g‖_2 ^ 2 is ∑_S c ^ (2 |S|) f̂(S) ^ 2 ≤ c ^ (2 k) ‖f‖_2 ^ 2 by Parseval's identity.

Main results

• Cslib.BitString.lpNorm_le_sqrt_pow_mul_lpNorm_two, Cslib.BitString.lpNorm_le_sqrt_pow_mul_lpNorm_two_of_fourierCoeff_eq_zero: ‖f‖_q ≤ √(q - 1) ^ k ‖f‖_2 for f of degree at most k.
• Cslib.BitString.expect_pow_four_le, Cslib.BitString.expect_pow_four_le_of_fourierCoeff_eq_zero: the Bonami Lemma.

References

• A. Bonami, Étude des coefficients de Fourier des fonctions de L^p(G)
• R. O'Donnell, Analysis of Boolean Functions

theorem Cslib.BitString.lpNorm_le_sqrt_pow_mul_lpNorm_two_of_fourierCoeff_eq_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] {q : ℝ} (hq : 2 ≤ q) {k : ℕ} {f : (ι → Bool) → ℝ} (hf : ∀ (S : Finset ι), k < S.card → fourierCoeff f S = 0) : lpNorm q f ≤ √(q - 1) ^ k * lpNorm 2 f

Low-degree functions are hypercontractive, Fourier-coefficient form: if the Fourier coefficients of f vanish above degree k, then ‖f‖_q ≤ √(q - 1) ^ k ‖f‖_2 for every q ≥ 2 O'Donnell, Theorem 9.21.

theorem Cslib.BitString.lpNorm_le_sqrt_pow_mul_lpNorm_two {ι : Type u_1} [Fintype ι] [DecidableEq ι] {q : ℝ} (hq : 2 ≤ q) {k : ℕ} {f : (ι → Bool) → ℝ} (hf : f ∈ lowDegree ℝ ι k) : lpNorm q f ≤ √(q - 1) ^ k * lpNorm 2 f

Low-degree functions are hypercontractive: if f has degree at most k, then ‖f‖_q ≤ √(q - 1) ^ k ‖f‖_2 for every q ≥ 2 O'Donnell, Theorem 9.21.

theorem Cslib.BitString.expect_pow_four_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {k : ℕ} {f : (ι → Bool) → ℝ} (hf : f ∈ lowDegree ℝ ι k) : (Finset.univ.expect fun (x : ι → Bool) => f x ^ 4) ≤ 9 ^ k * (Finset.univ.expect fun (x : ι → Bool) => f x ^ 2) ^ 2

The Bonami Lemma: if f has degree at most k, then 𝔼 f ^ 4 ≤ 9 ^ k (𝔼 f ^ 2) ^ 2, that is, ‖f‖_4 ≤ √3 ^ k ‖f‖_2 [Bon70] O'Donnell, Section 9.1.

theorem Cslib.BitString.expect_pow_four_le_of_fourierCoeff_eq_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] {k : ℕ} {f : (ι → Bool) → ℝ} (hf : ∀ (S : Finset ι), k < S.card → fourierCoeff f S = 0) : (Finset.univ.expect fun (x : ι → Bool) => f x ^ 4) ≤ 9 ^ k * (Finset.univ.expect fun (x : ι → Bool) => f x ^ 2) ^ 2

The Bonami Lemma, Fourier-coefficient form: if the Fourier coefficients of f vanish above degree k, then 𝔼 f ^ 4 ≤ 9 ^ k (𝔼 f ^ 2) ^ 2 [Bon70] O'Donnell, Section 9.1.