The KKL inequality at p = 1/2, and the p-biased basis at p = 1/2

TheoremNormalized bit at \(p = 1/2\) is \(-(-1)^b\)#✓fully proved

At p = 1/2 the normalized bit is -(-1)^b.

theorem fsr_ptn_psi_half (b : Bool) :
    ptn_psi (1 / 2 : ℝ) b = - khc_sign b

Uses 4 · Used by 1

Statement uses\(\pm 1\) value of a bit · Normalized Bernoulli bit

Proof usesStandard deviation of a Bernoulli bit · Zero-one value of a bit

Used by\(p\)-biased character at \(p = 1/2\) is the Walsh character up to sign

Theorem\(p\)-biased character at \(p = 1/2\) is the Walsh character up to sign#✓fully proved

At p = 1/2 the p-biased character is (-1)^{|S|} times the Walsh character.

theorem fsr_ptn_pchar_half (S : Finset ι) (ω : ConfigSpace ι) :
    ptn_pchar (1 / 2 : ℝ) S ω = (-1) ^ S.card * khc_walshChar S ω

Uses 6 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Walsh character on the Boolean cube · \(p\)-biased character

Proof usesNormalized bit at \(p = 1/2\) is \(-(-1)^b\) · \(\pm 1\) value of a bit · Normalized Bernoulli bit

Used bySquared \(p\)-biased and Walsh coefficients agree at \(p = 1/2\)

TheoremSquared \(p\)-biased and Walsh coefficients agree at \(p = 1/2\)#✓fully proved

At p = 1/2 the squared p-biased and Walsh Fourier coefficients agree.

theorem fsr_ptn_coeff_half_sq (f : ConfigSpace ι → ℝ) (S : Finset ι) :
    (ptn_coeff (1 / 2 : ℝ) f S) ^ 2 = (khc_fourierCoeff f S) ^ 2

Uses 10 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Fourier–Walsh coefficient under the uniform measure · \(p\)-biased Fourier coefficient

Proof usesBernoulli product weight · Expectation under a product weight · Probability of a configuration under a product weight · Uniform expectation on the Boolean cube · \(p\)-biased character at \(p = 1/2\) is the Walsh character up to sign · Walsh character on the Boolean cube · \(p\)-biased character

Used byTotal influence at \(p = 1/2\) via \(p\)-biased Fourier coefficients

TheoremTotal influence at \(p = 1/2\) via \(p\)-biased Fourier coefficients#✓fully proved

Total influence at p = 1/2 in terms of the p-biased Fourier coefficients.

theorem fsr_totalInfl_half_eq (φ : ConfigSpace ι → Bool) :
    totalInfl (OSSS.bernoulliWeight (1 / 2 : ℝ)) (fun ω => if φ ω then (1 : ℝ) else 0)
      = ∑ S : Finset ι, 4 * (S.card : ℝ)
          * (ptn_coeff (1 / 2 : ℝ) (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2

Uses 7

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · \(p\)-biased Fourier coefficient · Total influence under a product weight

Proof usesSquared \(p\)-biased and Walsh coefficients agree at \(p = 1/2\) · Fourier–Walsh coefficient under the uniform measure · Total influence as Fourier weight

TheoremKahn–Kalai–Linial inequality#✓fully proved

Kahn–Kalai–Linial inequality for the uniform measure with constant 2 (J. Kahn, G. Kalai, N. Linial, The influence of variables on Boolean functions, FOCS 1988; proof after D. Falik, A. Samorodnitsky, 2007): for every finite nonempty E and every Boolean function φ on {0, 1}^E, 2 · Var(φ) · log (1 / maxₑ Infₑ(φ)) ≤ ∑ₑ Infₑ(φ), where Infₑ(φ) is the probability that e is pivotal. This is the p = 1/2 case of the p-biased KKL inequality.

theorem fsr_pbiased_endpoint :
    KKLHypercontractive (1 / 2 : ℝ) 2

Uses 3

Statement usesKKL inequality with constant \(c\) for the \(p\)-biased measure

Proof usesKKL inequality at \(p = 1/2\) from the conditional statement · KKL inequality

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.