The KKL inequality: statement and elementary bounds

DefinitionTotal influence under a product weight#✓fully proved

The total influence ∑ₑ Infₑ(g) of g under the product weight ν.

noncomputable def totalInfl (ν : E → Bool → ℝ) (g : ConfigSpace E → ℝ) : ℝ :=
  ∑ e, OSSS.infl ν g e

Uses 2 · Used by 45

Statement usesConfiguration space of a statistical-mechanics model · Influence of a coordinate

Used byDamped KKL inequality under the \(p\)-biased measure · KKL inequality with constant \(2\) at \(p = 1/2\) · Capped \(p\)-biased per-coordinate estimate in the variable \(u\) · Log-sum estimate for the fiber weights · Capped estimate with zero weights holds trivially · Capped influence estimate for all \(p\) in \((1/2, q)\) · Capped estimate implies KKL with constant 2 on \((1/2, q)\) · Fourier total weight equals \(4p(1-p)\) times the total influence · Bound on the high-degree part of the damped total weight · Low-degree case implies the low-range case · Low-degree residual case of the capped estimate · Some truncation level makes the low-degree right side nonnegative · Capped estimate from its low-degree part · Sum of influence powers capped by the maximal influence · Capped log-sum estimate for damped influences · Capped estimate when the maximal influence is at least \(e^{-1}\) · Capped estimate on \((0, 1)\) from concavity of the right side · Small-influence case implies the open-interval case · Small-influence residual case of the capped estimate · Capped estimate in the hypercontractive range with matching \(q'\) · Right side of the capped estimate is nonnegative · Low-range residual case of the capped estimate · Low-range case implies the small-influence case · Capped estimate at \(p = 1/2\) for all \(u \in (0, 1)\) · Target-exponent capped estimate under the gap condition · Target-exponent capped estimate from a domination bound · Damped total weight at \(u = 0\) is at most the total influence · Capped estimate in the hypercontractive range · Capped estimate at the endpoint \(u = 1\) · Open-interval case implies the full capped estimate on \((1/2, q)\) · Open-interval residual case of the capped estimate · Total influence at \(p = 1/2\) via \(p\)-biased Fourier coefficients · KKL inequality with constant 2 at \(p\) implies its event form · KKL inequality with constant 0 holds trivially · Kahn–Kalai–Linial inequality · Kahn–Kalai–Linial inequality · KKL inequality with constant \(c\) for the \(p\)-biased measure · Reflection of the KKL inequality from \(p\) to \(1 - p\) · Hypercontractive form of KKL implies the KKL inequality at \(p = 1/2\) · Hypercontractive form of KKL with constant 0 holds trivially · Total influence as Fourier weight · Capped per-coordinate estimate under the \(p\)-biased measure · \(p\)-biased KKL inequality conditional on the capped estimate · Trivial KKL inequality with constant \(0\) · \(p\)-biased total influence as Fourier weight

DefinitionMaximal influence under a product weight#✓fully proved

The maximal influence maxₑ Infₑ(g) of g under the product weight ν.

noncomputable def maxInfl [Nonempty E] (ν : E → Bool → ℝ) (g : ConfigSpace E → ℝ) : ℝ :=
  Finset.univ.sup' Finset.univ_nonempty (OSSS.infl ν g)

Uses 2 · Used by 50

Statement usesConfiguration space of a statistical-mechanics model · Influence of a coordinate

Used byDamped KKL inequality under the \(p\)-biased measure · KKL inequality with constant \(2\) at \(p = 1/2\) · Capped \(p\)-biased per-coordinate estimate in the variable \(u\) · Log-sum estimate for the fiber weights · Capped estimate with zero weights holds trivially · Capped influence estimate for all \(p\) in \((1/2, q)\) · Capped estimate implies KKL with constant 2 on \((1/2, q)\) · Low-degree case implies the low-range case · Low-degree residual case of the capped estimate · Some truncation level makes the low-degree right side nonnegative · Sum of influence powers capped by the maximal influence · Capped per-coordinate hypercontractive estimate · Fourier-form KKL at \(p = 1/2\) conditional on the capped estimate · Conditional Fourier-form KKL holds trivially with constant zero · Fourier-form KKL inequality given the indicator Bonami–Beckner bound · Indicator-bound form of KKL with constant 0 holds trivially · Capped log-sum estimate for damped influences · Maximal influence of a Boolean function is at most one · Capped estimate when the maximal influence is at least \(e^{-1}\) · Capped estimate on \((0, 1)\) from concavity of the right side · Small-influence case implies the open-interval case · Small-influence residual case of the capped estimate · Capped estimate in the hypercontractive range with matching \(q'\) · Right side of the capped estimate is nonnegative · Low-range residual case of the capped estimate · Low-range case implies the small-influence case · Capped estimate at \(p = 1/2\) for all \(u \in (0, 1)\) · Target-exponent capped estimate under the gap condition · Target-exponent capped estimate from a domination bound · Capped estimate in the hypercontractive range · Capped estimate at the endpoint \(u = 1\) · Open-interval case implies the full capped estimate on \((1/2, q)\) · Open-interval residual case of the capped estimate · Fourier-form KKL inequality given the measure–influence bound · Measure–influence form of KKL with constant 0 holds trivially · KKL inequality with constant 2 at \(p\) implies its event form · Logarithm of the reciprocal maximal influence of an event · Capped estimate rewritten in the variable \(u = 1 - \rho^2\) · KKL inequality · KKL inequality with constant 0 holds trivially · Kahn–Kalai–Linial inequality · Kahn–Kalai–Linial inequality · KKL inequality with constant \(c\) for the \(p\)-biased measure · Reflection of the KKL inequality from \(p\) to \(1 - p\) · Hypercontractive form of KKL implies the KKL inequality at \(p = 1/2\) · Fourier-form KKL inequality given the hypercontractive bound · Hypercontractive form of KKL with constant 0 holds trivially · Capped per-coordinate estimate under the \(p\)-biased measure · \(p\)-biased KKL inequality conditional on the capped estimate · Trivial KKL inequality with constant \(0\)

DefinitionKKL inequality with constant \(c\) for the \(p\)-biased measure#✓fully proved

The KKL inequality with constant c for the Bernoulli(p) product measure: for every finite nonempty index type E and every Boolean function φ on {0, 1}^E, c · Var(φ) · log (1 / maxₑ Infₑ(φ)) ≤ ∑ₑ Infₑ(φ), with Infₑ(φ) the probability that e is pivotal.

Despite its name, this is the conclusion of the KKL theorem, not a hypercontractivity estimate. It holds trivially for c = 0 (kkl_hypercontractive_zero) and is proved for p = 1/2, c = 2 in fsr_pbiased_endpoint. When maxₑ Infₑ(φ) = 0, log (1 / 0) = 0 in Lean and the inequality is trivial.

def KKLHypercontractive (p c : ℝ) : Prop :=
  ∀ {E : Type} [Fintype E] [DecidableEq E] [Nonempty E] (φ : ConfigSpace E → Bool),
    c * OSSS.var (bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)
        * Real.log (1 / maxInfl (bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0))
      ≤ totalInfl (bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)

Uses 5 · Used by 18

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Variance under a product weight · Maximal influence under a product weight · Total influence under a product weight

Used byKKL inequality at \(p = 1/2\) from the conditional statement · Indicator-bound form of KKL implies the KKL inequality at \(p = 1/2\) · KKL inequality for p-biased measures · Measure–influence form of KKL implies the KKL inequality at \(p = 1/2\) · Kahn–Kalai–Linial inequality · KKL on the interior of \((1/2, q)\) implies its event form there · KKL inequality with constant 2 at \(p\) implies its event form · Sharp-threshold bound assuming the KKL inequality on \((1/2, q)\) · Sharp-threshold window bound assuming the KKL inequality on \((1/2, q)\) · KKL inequality with constant 0 holds trivially · Kahn–Kalai–Linial inequality · Kahn–Kalai–Linial inequality · KKL hypothesis on \((1/2, q)\) restated on the interior of \((1/2, q)\) · Reflection of the KKL inequality from \(p\) to \(1 - p\) · KKL inequality with constant 2 on \((1/2, q)\) · KKL inequality with constant 0 holds trivially on \((1/2, q)\) · Hypercontractive form of KKL implies the KKL inequality at \(p = 1/2\) · Conditional \(p\)-biased KKL statement yields KKL with constant \(2\)

TheoremKahn–Kalai–Linial inequality#✓fully proved

Kahn–Kalai–Linial inequality, total-influence form (J. Kahn, G. Kalai, N. Linial, The influence of variables on Boolean functions, FOCS 1988): under KKLHypercontractive p c, c · Var(φ) · log (1 / maxₑ Infₑ(φ)) ≤ ∑ₑ Infₑ(φ).

theorem kkl_inequality_total {p c : ℝ} (H : KKLHypercontractive p c)
    {E : Type} [Fintype E] [DecidableEq E] [Nonempty E] (φ : ConfigSpace E → Bool) :
    c * OSSS.var (bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)
        * Real.log (1 / maxInfl (bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0))
      ≤ totalInfl (bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)

Uses 6 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Variance under a product weight · KKL inequality with constant \(c\) for the \(p\)-biased measure · Maximal influence under a product weight · Total influence under a product weight

Used byKahn–Kalai–Linial inequality

TheoremKahn–Kalai–Linial inequality#✓fully proved

Kahn–Kalai–Linial inequality, maximal-influence form (J. Kahn, G. Kalai, N. Linial, The influence of variables on Boolean functions, FOCS 1988): under KKLHypercontractive p c, c · Var(φ) · log (1 / δ) ≤ |E| · δ with δ = maxₑ Infₑ(φ), so δ is at least of order Var(φ) · log |E| / |E|.

theorem kkl_inequality_max {p c : ℝ} (H : KKLHypercontractive p c)
    {E : Type} [Fintype E] [DecidableEq E] [Nonempty E] (φ : ConfigSpace E → Bool) :
    c * OSSS.var (bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)
        * Real.log (1 / maxInfl (bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0))
      ≤ (Fintype.card E : ℝ)
          * maxInfl (bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)

Uses 8

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Variance under a product weight · KKL inequality with constant \(c\) for the \(p\)-biased measure · Maximal influence under a product weight

Proof usesInfluence of a coordinate · Kahn–Kalai–Linial inequality · Total influence under a product weight

TheoremKKL inequality with constant 0 holds trivially#✓fully proved

KKLHypercontractive p 0 holds trivially, since total influence is nonnegative.

theorem kkl_hypercontractive_zero (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) :
    KKLHypercontractive p 0

Uses 12 · Used by 1

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

Proof usesConfiguration space of a statistical-mechanics model · Product probability weight · Bernoulli product weight · Expectation under a product weight · Influence of a coordinate · Variance under a product weight · Probability of a configuration under a product weight · Maximal influence under a product weight · Total influence under a product weight · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Used byKKL inequality with constant 0 holds trivially on \((1/2, q)\)

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.