Documentation

Complexity.Foundations.BooleanAnalysis.KahnKalaiLinial

The Kahn–Kalai–Linial theorem and Talagrand's inequality #

Read a Boolean function f as the function F = (-1) ^ f with values ±1. By the Poincaré inequality the influences of F on its n coordinates average at least Var[F] / n; the Kahn–Kalai–Linial theorem says that some coordinate has influence at least c · Var[F] · log n / n, for an absolute constant c > 0 [KKL88]. We prove it with c = 1 / 12 (BitString.exists_expect_sub_expect_sq_mul_log_card_div_le_influence), through its edge-isoperimetric form in O'Donnell's exposition: if every coordinate has influence at most δ, then the total influence is at least 1 / 6 · Var[F] · log (1 / δ) (BitString.expect_sub_expect_sq_mul_log_inv_le_six_mul_totalInfluence) O'Donnell, Section 9.6. Here Var[F] is written 𝔼 x, (F x - 𝔼 y, F y) ^ 2, the Fourier weight of F on the nonempty sets.

The same argument, run separately on each coordinate, proves Talagrand's inequality Var[F] ≤ 6 ∑ᵢ Infᵢ[F] / log (1 / Infᵢ[F]), for functions whose influences are all less than one (BitString.expect_sub_expect_sq_le_six_mul_sum_influence_div_log) [Tal94]; the form Var[F] ≤ 7 ∑ᵢ Infᵢ[F] / (1 + log (1 / Infᵢ[F])) holds for every Boolean function (BitString.expect_sub_expect_sq_le_seven_mul_sum_influence_div_one_add_log).

Proof #

The derivative Dᵢ F takes the values 0 and ±1, so ‖Dᵢ F‖_{4/3} ^ 2 = Infᵢ[F] ^ (3/2) (BitString.lpNorm_derivative_signVal), and the (4/3, 2)-Hypercontractivity Theorem Stab_{1/3}[Dᵢ F] ≤ ‖Dᵢ F‖_{4/3} ^ 2 bounds the low-degree part of the Fourier weight on the sets containing i (BitString.mul_noiseStability_derivative, BitString.sum_filter_mem_one_third_pow_mul_fourierCoeff_sq_le):

∑_{S ∋ i} 3 ^ (-|S|) F̂(S) ^ 2 = 1/3 · Stab_{1/3}[Dᵢ F] ≤ 1/3 · Infᵢ[F] ^ (3/2).

The variance is ∑ᵢ ∑_{S ∋ i} F̂(S) ^ 2 / |S|. For A > 1 and every m ≥ 1, 1 / m ≤ log 3 / log A + A 3 ^ (-m), according as 3 ^ m ≥ A or not, so the weight on the sets containing i is at most log 3 / log A · Infᵢ[F] + A / 3 · Infᵢ[F] ^ (3/2). If Infᵢ[F] ≤ δ < 1, the choice A = δ ^ (-1/4) and the bound δ ^ (1/4) log (1 / δ) < 4 turn this into 6 Infᵢ[F] / log (1 / δ). Summing over i with a common δ gives the Kahn–Kalai–Linial bound, and taking δ = Infᵢ[F] gives Talagrand's inequality.

Main results #

References #

Hypercontractivity on the derivatives #

source
theorem Cslib.BitString.sum_filter_mem_one_third_pow_mul_fourierCoeff_sq_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) (i : ι) :
∑ S : Finset ι with i ∈ S, (1 / 3) ^ S.card * fourierCoeff (fun (x : ι → Bool) => signVal (f x)) S ^ 2 ≤ (influence i fun (x : ι → Bool) => signVal (f x)) * √(influence i fun (x : ι → Bool) => signVal (f x)) / 3

Hypercontractivity bounds the low-degree weight on the sets containing a coordinate: for a Boolean function read as signs, ∑_{S ∋ i} 3 ^ (-|S|) F̂(S) ^ 2 ≤ 1/3 · Infᵢ[F] ^ (3/2), by the (4/3, 2)-Hypercontractivity Theorem applied to the derivative in i O'Donnell, Section 9.6.

The weight on the sets containing a coordinate #

source
theorem Cslib.BitString.one_le_mul_log_three_div_log_or_one_lt_mul_one_third_pow {A : ℝ} (hA : 1 < A) (m : ℕ) :
1 ≤ ↑m * (Real.log 3 / Real.log A) ∨ 1 < A * (1 / 3) ^ m

The degree threshold: for A > 1, every m satisfies 1 ≤ m log 3 / log A or 1 < A 3 ^ (-m), according as 3 ^ m ≥ A or not.

The Kahn–Kalai–Linial theorem #

source
theorem Cslib.BitString.expect_sub_expect_sq_mul_log_inv_le_six_mul_totalInfluence {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) {δ : ℝ} (hδ : ∀ (i : ι), (influence i fun (x : ι → Bool) => signVal (f x)) ≤ δ) :
(Finset.univ.expect fun (x : ι → Bool) => (signVal (f x) - Finset.univ.expect fun (y : ι → Bool) => signVal (f y)) ^ 2) * Real.log δ⁻¹ ≤ 6 * totalInfluence fun (x : ι → Bool) => signVal (f x)

The Kahn–Kalai–Linial theorem, edge-isoperimetric form: if every coordinate has influence at most δ on a Boolean function read as signs F, then Var[F] · log (1 / δ) ≤ 6 I[F], that is, the total influence is at least 1/6 · Var[F] · log (1 / δ) [KKL88] [Tal94] O'Donnell, Section 9.6. For δ ≥ 1 the left side is at most zero.

source
theorem Cslib.BitString.exists_expect_sub_expect_sq_mul_log_card_div_le_influence {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (f : (ι → Bool) → Bool) :
∃ (i : ι), (Finset.univ.expect fun (x : ι → Bool) => (signVal (f x) - Finset.univ.expect fun (y : ι → Bool) => signVal (f y)) ^ 2) * Real.log ↑(Fintype.card ι) / (12 * ↑(Fintype.card ι)) ≤ influence i fun (x : ι → Bool) => signVal (f x)

The Kahn–Kalai–Linial theorem: some coordinate has influence at least Var[F] · log n / (12 n) on a Boolean function read as signs F of n ≥ 1 coordinates [KKL88] O'Donnell, Section 9.6.

Talagrand's inequality #

source
theorem Cslib.BitString.expect_sub_expect_sq_le_six_mul_sum_influence_div_log {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) (hf : ∀ (i : ι), (influence i fun (x : ι → Bool) => signVal (f x)) < 1) :
(Finset.univ.expect fun (x : ι → Bool) => (signVal (f x) - Finset.univ.expect fun (y : ι → Bool) => signVal (f y)) ^ 2) ≤ 6 * ∑ i : ι, (influence i fun (x : ι → Bool) => signVal (f x)) / Real.log (influence i fun (x : ι → Bool) => signVal (f x))⁻¹

Talagrand's inequality: for a Boolean function read as signs F whose influences are all less than one, Var[F] ≤ 6 ∑ᵢ Infᵢ[F] / log (1 / Infᵢ[F]) [Tal94]. A coordinate of influence one contributes +∞ in the usual reading of the inequality; for an unconditional form see expect_sub_expect_sq_le_seven_mul_sum_influence_div_one_add_log.

source
theorem Cslib.BitString.expect_sub_expect_sq_le_seven_mul_sum_influence_div_one_add_log {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) :
(Finset.univ.expect fun (x : ι → Bool) => (signVal (f x) - Finset.univ.expect fun (y : ι → Bool) => signVal (f y)) ^ 2) ≤ 7 * ∑ i : ι, (influence i fun (x : ι → Bool) => signVal (f x)) / (1 + Real.log (influence i fun (x : ι → Bool) => signVal (f x))⁻¹)

Talagrand's inequality, unconditional form: for every Boolean function read as signs F, Var[F] ≤ 7 ∑ᵢ Infᵢ[F] / (1 + log (1 / Infᵢ[F])) [Tal94].