Friedgut's junta theorem

A Boolean function of small total influence is close to a function of few coordinates: if I[F] ≤ K for a Boolean function f read as signs F, then for every ε > 0, f agrees with a function of at most 4 K ^ 3 / (9 ε ^ 2) · 81 ^ (K / ε) coordinates outside a fraction ε of the inputs (BitString.exists_dependsOn_hammingDist_div_le_of_totalInfluence_le), so, for ε ≤ 1, with a function of at most 3 · 2 ^ (8 K / ε) coordinates (BitString.exists_card_le_three_mul_two_rpow_dependsOn_hammingDist_div_le) [Fri98] O'Donnell, Section 9.6. A function of the coordinates in J is a J-junta, written with Mathlib's DependsOn.

Proof

Averaging out the coordinates outside a set J keeps the Fourier coefficients on the subsets of J and kills the others (BitString.fourierCoeff_expect_piecewise), so f is within mean square distance ∑_{S ⊄ J} F̂(S) ^ 2 of a function of the coordinates in J, and rounding it to a sign gives a Boolean J-junta at relative Hamming distance at most that weight (BitString.exists_dependsOn_hammingDist_div_le_sum_not_subset_fourierCoeff_sq). For the set J of the coordinates of influence more than τ, the weight outside the subsets of J is at most log 3 / log A · I[F] + A / 3 · √τ · I[F] for every A > 1 (BitString.sum_filter_not_subset_fourierCoeff_sq_le): the sets of size m with 3 ^ m ≥ A carry weight at most log 3 / log A · I[F], and the hypercontractive bound of the Kahn–Kalai–Linial theorem, ∑_{S ∋ i} 3 ^ (-|S|) F̂(S) ^ 2 ≤ Infᵢ[F] ^ (3/2) / 3, summed over the coordinates i ∉ J, bounds the others. Taking A = 9 ^ (K / ε) and √τ = 3 ε / (2 K A) makes both terms at most ε / 2, and J has at most K / τ elements.

Main results

• Cslib.BitString.exists_dependsOn_hammingDist_div_le_sum_not_subset_fourierCoeff_sq: a Boolean function is close to a J-junta when its Fourier weight is concentrated on the subsets of J.
• Cslib.BitString.sum_filter_not_subset_fourierCoeff_sq_le: the Fourier weight outside the subsets of the set of influential coordinates.
• Cslib.BitString.exists_dependsOn_hammingDist_div_le_of_totalInfluence_le, Cslib.BitString.exists_card_le_three_mul_two_rpow_dependsOn_hammingDist_div_le: Friedgut's junta theorem.

References

• E. Friedgut, Boolean functions with low average sensitivity depend on few coordinates
• R. O'Donnell, Analysis of Boolean Functions

Juntas from spectral concentration

theorem Cslib.BitString.exists_dependsOn_hammingDist_div_le_sum_not_subset_fourierCoeff_sq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) (J : Finset ι) : ∃ (g : (ι → Bool) → Bool), DependsOn g ↑J ∧ ↑(hammingDist f g) / 2 ^ Fintype.card ι ≤ ∑ S : Finset ι with ¬S ⊆ J, fourierCoeff (fun (x : ι → Bool) => signVal (f x)) S ^ 2

Spectral concentration gives a junta: a Boolean function is at relative Hamming distance at most ∑_{S ⊄ J} F̂(S) ^ 2 from a Boolean function of the coordinates in J, the sign of its average over the other coordinates O'Donnell, Proposition 3.31.

The weight outside the influential coordinates

theorem Cslib.BitString.sum_filter_not_subset_fourierCoeff_sq_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) {J : Finset ι} {τ : ℝ} (hJ : ∀ i ∉ J, (influence i fun (x : ι → Bool) => signVal (f x)) ≤ τ) {A : ℝ} (hA : 1 < A) : ∑ S : Finset ι with ¬S ⊆ J, fourierCoeff (fun (x : ι → Bool) => signVal (f x)) S ^ 2 ≤ (Real.log 3 / Real.log A * totalInfluence fun (x : ι → Bool) => signVal (f x)) + A / 3 * √τ * totalInfluence fun (x : ι → Bool) => signVal (f x)

The Fourier weight outside the influential coordinates: if every coordinate outside J has influence at most τ on a Boolean function read as signs F, then for every A > 1, ∑_{S ⊄ J} F̂(S) ^ 2 ≤ log 3 / log A · I[F] + A / 3 · √τ · I[F] O'Donnell, Theorem 9.28.

Friedgut's junta theorem

theorem Cslib.BitString.exists_dependsOn_hammingDist_div_le_of_totalInfluence_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) {K ε : ℝ} (hε : 0 < ε) (hK : (totalInfluence fun (x : ι → Bool) => signVal (f x)) ≤ K) : ∃ (J : Finset ι) (g : (ι → Bool) → Bool), ↑J.card ≤ 4 * K ^ 3 / (9 * ε ^ 2) * 81 ^ (K / ε) ∧ DependsOn g ↑J ∧ ↑(hammingDist f g) / 2 ^ Fintype.card ι ≤ ε

Friedgut's junta theorem: if a Boolean function read as signs F has total influence at most K, then for every ε > 0 it is at relative Hamming distance at most ε from a Boolean function of at most 4 K ^ 3 / (9 ε ^ 2) · 81 ^ (K / ε) coordinates [Fri98] O'Donnell, Section 9.6.

theorem Cslib.BitString.exists_card_le_three_mul_two_rpow_dependsOn_hammingDist_div_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) {K ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hK : (totalInfluence fun (x : ι → Bool) => signVal (f x)) ≤ K) : ∃ (J : Finset ι) (g : (ι → Bool) → Bool), ↑J.card ≤ 3 * 2 ^ (8 * K / ε) ∧ DependsOn g ↑J ∧ ↑(hammingDist f g) / 2 ^ Fintype.card ι ≤ ε

Friedgut's junta theorem, exponential form: if a Boolean function read as signs F has total influence at most K, then for every 0 < ε ≤ 1 it is at relative Hamming distance at most ε from a Boolean function of at most 3 · 2 ^ (8 K / ε) coordinates [Fri98] O'Donnell, Section 9.6.