Sharp thresholds from influences

DefinitionEvent that an edge is open#✓fully proved

The event {ω_e = 1} that the edge e is open.

def openEdge (e : E) : Set (ConfigSpace E) := {ω | ω e = true}

Uses 1 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model

Used byRusso's formula

TheoremRusso's formula#✓fully proved

Russo's formula, covariance form: for increasing A and p ∉ {0, 1}, d/dp ℙ_p(A) = (p(1 - p))⁻¹ ∑_e (ℙ_p(A ∩ {ω_e = 1}) - ℙ_p(ω_e = 1) ℙ_p(A)).

theorem russoFormula (p : ℝ) (A : Set (ConfigSpace E)) (hA : IsIncreasing A)
    (hp0 : p ≠ 0) (hp1 : p ≠ 1) :
    deriv (fun p => prob p A) p
      = (1 / (p * (1 - p)))
          * ∑ e, (prob p (A ∩ openEdge e) - prob p (openEdge e) * prob p A)

Uses 11

Statement usesEvent that an edge is open · Configuration space of a statistical-mechanics model · Increasing event · Bernoulli weight of an event

Proof usesBernoulli product weight of a configuration · Configuration weight splits at one coordinate · Russo's formula · Bernoulli weight of a single coordinate · Weight of the event that a coordinate is pivotal · Contribution of one coordinate to Russo's formula · Product of coordinate weights off one coordinate

DefinitionInfluence of an edge on an event#✓fully proved

The influence I_e^p(A) = ℙ_p(e is pivotal for A) of the coordinate e on the event A under the p-biased product measure.

See also MathlibExt.Analysis.Fourier.BooleanCubeInfluence.boolInfluence, the influence of a real function on the uniform Boolean cube (the case p = 1/2, in Fourier normalization).

noncomputable def influence (p : ℝ) (A : Set (ConfigSpace E)) (e : E) : ℝ :=
  pivotalProb p A e

Uses 2 · Used by 7

Statement usesConfiguration space of a statistical-mechanics model · Weight of the event that a coordinate is pivotal

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 · Pivotal-probability influence as the OSSS influence of an indicator · Sharp-threshold window bound assuming the KKL inequality on \((1/2, q)\) · Sharp threshold from a KKL-type influence inequality · Sharp threshold from influences

TheoremSharp threshold from influences#✓fully proved

If A is increasing, ℙ_{1/2}(A) = 1/2, and the total influence ∑_e I_e^p(A) is at least M for all p ∈ (1/2, q), then ℙ_q(A) ≥ 1/2 + M (q - 1/2).

theorem sth_sharpThreshold (A : Set (ConfigSpace E)) (hA : IsIncreasing A) {q M : ℝ}
    (hq : (1 : ℝ) / 2 ≤ q)
    (hhalf : prob (1 / 2) A = 1 / 2)
    (hinfl : ∀ p ∈ interior (Set.Icc (1 / 2 : ℝ) q), M ≤ ∑ e, influence p A e) :
    1 / 2 + M * (q - 1 / 2) ≤ prob q A

Uses 8 · Used by 2

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

Proof usesRusso's formula · Derivative of the event weight before grouping · Weight of the event that a coordinate is pivotal · Product of coordinate weights off one coordinate

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

TheoremSharp threshold from a KKL-type influence inequality#✓fully proved

Sharp threshold from a KKL-type inequality: if ℙ_{1/2}(A) = 1/2 and for all p ∈ (1/2, q) ∑_e I_e^p(A) ≥ C · ℙ_p(A)(1 - ℙ_p(A)) · L'(p), ℙ_p(A)(1 - ℙ_p(A)) ≥ v₀ and L'(p) ≥ L, then ℙ_q(A) ≥ 1/2 + C v₀ L (q - 1/2). The KKL-type inequality is a hypothesis.

theorem ktr_sharpThreshold_via_kkl (A : Set (ConfigSpace E)) (hA : IsIncreasing A)
    {q C v₀ L : ℝ} (hq : (1 : ℝ) / 2 ≤ q)
    (hC : 0 < C) (hv0 : 0 ≤ v₀) (hL : 0 ≤ L)
    (hhalf : prob (1 / 2) A = 1 / 2)
    (L' : ℝ → ℝ)
    (hkkl : ∀ p ∈ interior (Set.Icc (1 / 2 : ℝ) q),
      C * (prob p A * (1 - prob p A)) * L' p ≤ ∑ e, influence p A e)
    (hvar : ∀ p ∈ interior (Set.Icc (1 / 2 : ℝ) q), v₀ ≤ prob p A * (1 - prob p A))
    (hLL' : ∀ p ∈ interior (Set.Icc (1 / 2 : ℝ) q), L ≤ L' p) :
    1 / 2 + (C * v₀ * L) * (q - 1 / 2) ≤ prob q A

Uses 5 · Used by 1

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

Proof usesSharp threshold from influences

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

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.