The KKL inequality under p-biased measures: reflection and threshold consequences

DefinitionCoordinatewise complement of a configuration#✓fully proved

The coordinatewise complement ω ↦ ¬ω of a configuration.

def kpb_flipAll (ω : ConfigSpace E) : ConfigSpace E := fun e => !(ω e)

Uses 1 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model

Used byReflection of the KKL inequality from \(p\) to \(1 - p\) · Complement swaps the Bernoulli \(p\) and \(1 - p\) weights

LemmaComplement swaps the Bernoulli \(p\) and \(1 - p\) weights#✓fully proved

Complementing sends the Bernoulli(p) weight to the Bernoulli(1 - p) weight.

lemma kpb_weight_flip (p : ℝ) (ω : ConfigSpace E) :
    OSSS.weight (OSSS.bernoulliWeight (1 - p)) (kpb_flipAll ω)
      = OSSS.weight (OSSS.bernoulliWeight p) ω

Uses 4 · Used by 1

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

Used byReflection of the KKL inequality from \(p\) to \(1 - p\)

TheoremReflection of the KKL inequality from \(p\) to \(1 - p\)#✓fully proved

The KKL inequality with constant 2 at p implies it at 1 - p.

theorem kpb_kkl_reflect {p : ℝ} (H : KKLHypercontractive p 2) :
    KKLHypercontractive (1 - p) 2

Uses 14

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

Proof usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Covariance under a product weight · Expectation under a product weight · Influence of a coordinate · Variance under a product weight · Probability of a configuration under a product weight · Coordinatewise complement of a configuration · Complement swaps the Bernoulli \(p\) and \(1 - p\) weights · Maximal influence under a product weight · Total influence under a product weight · Closing a coordinate of a configuration · Opening a coordinate of a configuration

DefinitionKKL inequality with constant 2 on \((1/2, q)\)#✓fully proved

The KKL inequality with constant 2 for every Bernoulli parameter p ∈ (1/2, q).

def kpb_PBiasedHC (q : ℝ) : Prop :=
  ∀ p ∈ Set.Ioo (1 / 2 : ℝ) q, KKLHypercontractive p 2

Uses 1 · Used by 4

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

Used byKKL hypothesis on \((1/2, q)\) restated on the interior of \((1/2, q)\) · Sharp-threshold bound under the \(p\)-biased KKL hypothesis · Sharp-threshold window under the \(p\)-biased KKL hypothesis · Conditional KKL gives KKL with constant 2 on \((1/2, q)\) for \(q \le 1\)

TheoremKKL inequality with constant 0 holds trivially on \((1/2, q)\)#✓fully proved

The KKL inequality with constant 0 holds for every p; this is trivial.

theorem kpb_residue_c0 {q : ℝ} (hq : q ≤ 1) :
    ∀ p ∈ Set.Ioo (1 / 2 : ℝ) q, KKLHypercontractive p 0

Uses 2

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

Proof usesKKL inequality with constant 0 holds trivially

TheoremKKL hypothesis on \((1/2, q)\) restated on the interior of \((1/2, q)\)#✓fully proved

kpb_PBiasedHC q in the form used by StatMech.TwoDim.kklw_sharpThreshold.

theorem kpb_Hbkkkl {q : ℝ} (Hpb : kpb_PBiasedHC q) :
    ∀ p ∈ interior (Set.Icc (1 / 2 : ℝ) q), KKLHypercontractive p 2

Uses 2 · Used by 2

Statement usesKKL inequality with constant \(c\) for the \(p\)-biased measure · KKL inequality with constant 2 on \((1/2, q)\)

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

TheoremSharp-threshold bound under the \(p\)-biased KKL hypothesis#✓fully proved

StatMech.TwoDim.kklw_sharpThreshold under kpb_PBiasedHC q.

theorem kpb_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)
    (Hpb : kpb_PBiasedHC q)
    (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 ≤ StatMech.TwoDim.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 2 on \((1/2, q)\) · Logarithm of the reciprocal maximal influence of an event · Bernoulli weight of an event

Proof usesKKL hypothesis on \((1/2, q)\) restated on the interior of \((1/2, q)\) · Sharp-threshold bound assuming the KKL inequality on \((1/2, q)\)

Used bySharp-threshold bound from the conditional KKL statement

TheoremSharp-threshold window under the \(p\)-biased KKL hypothesis#✓fully proved

StatMech.TwoDim.kklw_sharpThreshold_window under kpb_PBiasedHC q.

theorem kpb_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)
    (Hpb : kpb_PBiasedHC q)
    (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 ≤ StatMech.TwoDim.kklw_logMaxInfl p A)
    (hnotyet : StatMech.prob q A ≤ 1 - ε) :
    q - 1 / 2 ≤ (1 / 2 - ε) / (2 * v₀ * L)

Uses 7

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · KKL inequality with constant 2 on \((1/2, q)\) · Logarithm of the reciprocal maximal influence of an event · Bernoulli weight of an event

Proof usesKKL hypothesis on \((1/2, q)\) restated on the interior of \((1/2, q)\) · Sharp-threshold window bound assuming the KKL inequality on \((1/2, q)\)

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.