The KKL inequality for events, and sharp thresholds

TheoremOSSS Bernoulli weight equals the configuration weight#✓fully proved

The OSSS Bernoulli weight of a configuration is StatMech.configWeight.

theorem kklw_weight_eq (p : ℝ) (ω : ConfigSpace E) :
    OSSS.weight (OSSS.bernoulliWeight p) ω = StatMech.configWeight p ω

Uses 5 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Probability of a configuration under a product weight · Bernoulli product weight of a configuration

Proof usesBernoulli weight of a single coordinate

Used byPivotal-probability influence as the OSSS influence of an indicator · Event probability as the OSSS expectation of its indicator

TheoremEvent probability as the OSSS expectation of its indicator#✓fully proved

StatMech.prob p A is the OSSS expectation of the indicator of A.

theorem kklw_prob_eq_expect (p : ℝ) (A : Set (ConfigSpace E)) :
    StatMech.prob p A
      = OSSS.expect (OSSS.bernoulliWeight p) (A.indicator (fun _ => (1 : ℝ)))

Uses 7 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Expectation under a product weight · Bernoulli weight of an event

Proof usesProbability of a configuration under a product weight · OSSS Bernoulli weight equals the configuration weight · Bernoulli product weight of a configuration

Used byVariance of an event indicator is \(P(A)(1 - P(A))\)

TheoremPivotal-probability influence as the OSSS influence of an indicator#✓fully proved

StatMech.BeffaraDC.influence is the OSSS influence of the indicator of A.

theorem kklw_influence_eq_infl (p : ℝ) (A : Set (ConfigSpace E)) (e : E) :
    StatMech.BeffaraDC.influence p A e
      = OSSS.infl (OSSS.bernoulliWeight p) (A.indicator (fun _ => (1 : ℝ))) e

Uses 11 · Used by 1

Statement usesInfluence of an edge on an event · Configuration space of a statistical-mechanics model · Bernoulli product weight · Influence of a coordinate

Proof usesPivotal coordinate for an event · Expectation under a product weight · Influence on an indicator is the pivotal probability · Probability of a configuration under a product weight · OSSS Bernoulli weight equals the configuration weight · Bernoulli product weight of a configuration · Weight of the event that a coordinate is pivotal

Used byKKL inequality with constant 2 at \(p\) implies its event form

TheoremVariance of an event indicator is \(P(A)(1 - P(A))\)#✓fully proved

The variance of the indicator of A is P(A)(1 - P(A)).

theorem kklw_var_eq (p : ℝ) (A : Set (ConfigSpace E)) :
    OSSS.var (OSSS.bernoulliWeight p) (A.indicator (fun _ => (1 : ℝ)))
      = StatMech.prob p A * (1 - StatMech.prob p A)

Uses 7 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Variance under a product weight · Bernoulli weight of an event

Proof usesCovariance under a product weight · Expectation under a product weight · Event probability as the OSSS expectation of its indicator

Used byKKL inequality with constant 2 at \(p\) implies its event form

DefinitionLogarithm of the reciprocal maximal influence of an event#✓fully proved

log (1 / maxₑ Infₑ(A)) under the Bernoulli(p) product measure.

noncomputable def kklw_logMaxInfl [Nonempty E] (p : ℝ) (A : Set (ConfigSpace E)) : ℝ :=
  Real.log (1 / maxInfl (OSSS.bernoulliWeight p) (A.indicator (fun _ => (1 : ℝ))))

Uses 3 · Used by 8

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

Used byKKL on the interior of \((1/2, q)\) implies its event form there · Kahn–Kalai–Linial inequality · 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)\) · Sharp-threshold bound under the \(p\)-biased KKL hypothesis · Sharp-threshold window under the \(p\)-biased KKL hypothesis · Sharp-threshold bound from the conditional KKL statement

TheoremKKL inequality with constant 2 at \(p\) implies its event form#✓fully proved

The KKL inequality KKLHypercontractive p 2 for an event: 2 · P_p(A)(1 - P_p(A)) · log (1 / maxₑ Infₑ(A)) ≤ ∑ₑ Infₑ(A).

theorem kklw_hkkl_of_hypercontractive {E : Type} [Fintype E] [DecidableEq E] [Nonempty E]
    {p : ℝ}
    (H : KKLHypercontractive p 2) (A : Set (ConfigSpace E)) :
    2 * (StatMech.prob p A * (1 - StatMech.prob p A)) * kklw_logMaxInfl p A
      ≤ ∑ e, StatMech.BeffaraDC.influence p A e

Uses 12 · Used by 2

Statement usesInfluence of an edge on an event · Configuration space of a statistical-mechanics model · KKL inequality with constant \(c\) for the \(p\)-biased measure · Logarithm of the reciprocal maximal influence of an event · Bernoulli weight of an event

Proof usesBernoulli product weight · Influence of a coordinate · Variance under a product weight · Maximal influence under a product weight · Total influence under a product weight · Pivotal-probability influence as the OSSS influence of an indicator · Variance of an event indicator is \(P(A)(1 - P(A))\)

Used byKKL on the interior of \((1/2, q)\) implies its event form there · Kahn–Kalai–Linial inequality

TheoremKahn–Kalai–Linial inequality#✓fully proved

Kahn–Kalai–Linial inequality for events under the uniform measure (J. Kahn, G. Kalai, N. Linial, The influence of variables on Boolean functions, FOCS 1988), with constant 2: 2 · P(A)(1 - P(A)) · log (1 / maxₑ Infₑ(A)) ≤ ∑ₑ Infₑ(A), where Infₑ(A) is the probability that e is pivotal for A.

theorem kklw_hkkl_half {E : Type} [Fintype E] [DecidableEq E] [Nonempty E]
    (A : Set (ConfigSpace E)) :
    2 * (StatMech.prob (1 / 2) A * (1 - StatMech.prob (1 / 2) A)) * kklw_logMaxInfl (1 / 2) A
      ≤ ∑ e, StatMech.BeffaraDC.influence (1 / 2) A e

Uses 7

Statement usesInfluence of an edge on an event · Configuration space of a statistical-mechanics model · Logarithm of the reciprocal maximal influence of an event · Bernoulli weight of an event

Proof usesKKL inequality at \(p = 1/2\) from the conditional statement · KKL inequality · KKL inequality with constant 2 at \(p\) implies its event form

TheoremKKL on the interior of \((1/2, q)\) implies its event form there#✓fully proved

kklw_hkkl_of_hypercontractive at every p in the interior of [1/2, q].

theorem kklw_hkkl {E : Type} [Fintype E] [DecidableEq E] [Nonempty E]
    (A : Set (ConfigSpace E)) {q : ℝ}
    (Hbkkkl : ∀ p ∈ interior (Set.Icc (1 / 2 : ℝ) q), KKLHypercontractive p 2) :
    ∀ p ∈ interior (Set.Icc (1 / 2 : ℝ) q),
      2 * (StatMech.prob p A * (1 - StatMech.prob p A)) * kklw_logMaxInfl p A
        ≤ ∑ e, StatMech.BeffaraDC.influence p A e

Uses 6 · Used by 2

Statement usesInfluence of an edge on an event · Configuration space of a statistical-mechanics model · KKL inequality with constant \(c\) for the \(p\)-biased measure · Logarithm of the reciprocal maximal influence of an event · Bernoulli weight of an event

Proof usesKKL inequality with constant 2 at \(p\) implies its event form

Used bySharp-threshold bound assuming the KKL inequality on \((1/2, q)\) · Sharp-threshold window bound assuming the KKL inequality on \((1/2, q)\)

TheoremSharp-threshold bound assuming the KKL inequality on \((1/2, q)\)#✓fully proved

Sharp-threshold bound: for an increasing event with P_{1/2}(A) = 1/2, if the KKL inequality holds for all p ∈ (1/2, q) and there P_p(A)(1 - P_p(A)) ≥ v₀ and log (1 / maxₑ Infₑ(A)) ≥ L, then P_q(A) ≥ 1/2 + 2 v₀ L (q - 1/2).

theorem kklw_sharpThreshold {E : Type} [Fintype E] [DecidableEq E] [Nonempty E]
    (A : Set (ConfigSpace E)) (hA : IsIncreasing A)
    {q v₀ L : ℝ} (hq : (1 : ℝ) / 2 ≤ q)
    (hv0 : 0 ≤ v₀) (hL : 0 ≤ L)
    (hhalf : StatMech.prob (1 / 2) A = 1 / 2)
    (Hbkkkl : ∀ p ∈ interior (Set.Icc (1 / 2 : ℝ) q), KKLHypercontractive p 2)
    (hvar : ∀ p ∈ interior (Set.Icc (1 / 2 : ℝ) q),
      v₀ ≤ StatMech.prob p A * (1 - StatMech.prob p A))
    (hLL' : ∀ p ∈ interior (Set.Icc (1 / 2 : ℝ) q), L ≤ kklw_logMaxInfl p A) :
    1 / 2 + (2 * v₀ * L) * (q - 1 / 2) ≤ StatMech.prob q A

Uses 7 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · KKL inequality with constant \(c\) for the \(p\)-biased measure · Logarithm of the reciprocal maximal influence of an event · Bernoulli weight of an event

Proof usesKKL on the interior of \((1/2, q)\) implies its event form there · Sharp threshold from a KKL-type influence inequality

Used bySharp-threshold bound under the \(p\)-biased KKL hypothesis

TheoremSharp-threshold window bound assuming the KKL inequality on \((1/2, q)\)#✓fully proved

Window form of kklw_sharpThreshold: under the same hypotheses, if P_q(A) ≤ 1 - ε then q - 1/2 ≤ (1/2 - ε) / (2 v₀ L).

theorem kklw_sharpThreshold_window {E : Type} [Fintype E] [DecidableEq E] [Nonempty E]
    (A : Set (ConfigSpace E)) (hA : IsIncreasing A)
    {q v₀ L ε : ℝ} (hq : (1 : ℝ) / 2 ≤ q)
    (hM : 0 < 2 * v₀ * L)
    (hhalf : StatMech.prob (1 / 2) A = 1 / 2)
    (hv0 : 0 ≤ v₀) (hL : 0 ≤ L)
    (Hbkkkl : ∀ p ∈ interior (Set.Icc (1 / 2 : ℝ) q), KKLHypercontractive p 2)
    (hvar : ∀ p ∈ interior (Set.Icc (1 / 2 : ℝ) q),
      v₀ ≤ StatMech.prob p A * (1 - StatMech.prob p A))
    (hLL' : ∀ p ∈ interior (Set.Icc (1 / 2 : ℝ) q), L ≤ kklw_logMaxInfl p A)
    (hnotyet : StatMech.prob q A ≤ 1 - ε) :
    q - 1 / 2 ≤ (1 / 2 - ε) / (2 * v₀ * L)

Uses 8 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · KKL inequality with constant \(c\) for the \(p\)-biased measure · Logarithm of the reciprocal maximal influence of an event · Bernoulli weight of an event

Proof usesInfluence of an edge on an event · KKL on the interior of \((1/2, q)\) implies its event form there · Sharp threshold from influences

Used bySharp-threshold window under the \(p\)-biased KKL hypothesis

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.