A damped KKL inequality under p-biased measures

TheoremIntegrating damped total-influence weights over the noise parameter#✓fully proved

Integrating the damped total-influence weights over the noise parameter, with the p-biased scaling A = 4p(1-p).

theorem fpe_integral_lhs (A : ℝ) (cf : Finset ι → ℝ) :
    (∫ u in (0 : ℝ)..1,
        ∑ S : Finset ι, 4 * (S.card : ℝ) * (A ^ (S.card - 1) / A) * (1 - u) ^ (S.card - 1) * cf S)
      = 4 * ∑ S ∈ (univ.erase (∅ : Finset ι)), (A ^ (S.card - 1) / A) * cf S

Uses 1 · Used by 1

Proof usesIntegral of \((1 - u)^n\) over \((0, 1)\)

Used byDamped KKL inequality under the \(p\)-biased measure

TheoremCapped \(p\)-biased per-coordinate estimate in the variable \(u\)#✓fully proved

The capped per-coordinate estimate under μ_p in the variable u, with ρ² = A (1 - u) and A = 4p(1-p).

theorem fpe_master_sub [Nonempty ι] {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1)
    (φ : ConfigSpace ι → Bool) (u : ℝ) (hu0 : 0 ≤ u) (hu1 : u ≤ 1) :
    (∑ S : Finset ι, 4 * (S.card : ℝ)
        * ((4 * p * (1 - p)) ^ (S.card - 1) / (4 * p * (1 - p)))
        * (1 - u) ^ (S.card - 1)
        * (ptn_coeff p (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2)
      ≤ (maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0))
          ^ (u / (2 - u))
        * totalInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)

Uses 7 · Used by 1

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

Proof usesCapped per-coordinate estimate under the \(p\)-biased measure · Standard deviation of a Bernoulli bit

Used byDamped KKL inequality under the \(p\)-biased measure

TheoremDamped KKL inequality under the \(p\)-biased measure#✓fully proved

Damped KKL inequality under the Bernoulli(p) measure, 0 < p < 1: with A = 4p(1-p), 2 · (∑_{S ≠ ∅} (A^{|S|-1} / A) f̂(S)²) · log (1 / maxₑ Infₑ) ≤ ∑ₑ Infₑ.

theorem fpe_dampedVarLogGain [Nonempty ι] {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1)
    (φ : ConfigSpace ι → Bool) :
    2 * (∑ S ∈ (univ.erase (∅ : Finset ι)),
          ((4 * p * (1 - p)) ^ (S.card - 1) / (4 * p * (1 - p)))
            * (ptn_coeff p (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2)
        * Real.log (1 / maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0))
      ≤ totalInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)

Uses 14 · Used by 1

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

Proof usesProduct probability weight · Expectation under a product weight · Influence of a coordinate · Probability of a configuration under a product weight · Bound on the integral of \(\delta^{u/(2-u)}\) over \((0, 1)\) · Integrating damped total-influence weights over the noise parameter · Capped \(p\)-biased per-coordinate estimate in the variable \(u\) · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Used byKKL inequality with constant \(2\) at \(p = 1/2\)

TheoremDamped variance equals the variance at \(p = 1/2\)#✓fully proved

At p = 1/2 the damped variance is the variance.

theorem fpe_Q_eq_var_at_half (φ : ConfigSpace ι → Bool) :
    (∑ S ∈ (univ.erase (∅ : Finset ι)),
        ((4 * (1/2 : ℝ) * (1 - 1/2)) ^ (S.card - 1) / (4 * (1/2 : ℝ) * (1 - 1/2)))
          * (ptn_coeff (1/2 : ℝ) (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2)
      = OSSS.var (OSSS.bernoulliWeight (1/2 : ℝ)) (fun ω => if φ ω then (1 : ℝ) else 0)

Uses 5 · Used by 1

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

Proof uses\(p\)-biased variance as Fourier weight off the empty set

Used byKKL inequality with constant \(2\) at \(p = 1/2\)

TheoremKKL inequality with constant \(2\) at \(p = 1/2\)#✓fully proved

The KKL inequality with constant 2 at p = 1/2, obtained from fpe_dampedVarLogGain. The same statement is kkl_inequality_total fsr_pbiased_endpoint, proved there by the uniform-cube argument.

theorem fpe_kklGain_at_half [Nonempty ι] (φ : ConfigSpace ι → Bool) :
    2 * OSSS.var (OSSS.bernoulliWeight (1/2 : ℝ)) (fun ω => if φ ω then (1 : ℝ) else 0)
        * Real.log (1 / maxInfl (OSSS.bernoulliWeight (1/2 : ℝ))
            (fun ω => if φ ω then (1 : ℝ) else 0))
      ≤ totalInfl (OSSS.bernoulliWeight (1/2 : ℝ)) (fun ω => if φ ω then (1 : ℝ) else 0)

Uses 8

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

Proof usesDamped variance equals the variance at \(p = 1/2\) · Damped KKL inequality under the \(p\)-biased measure · \(p\)-biased Fourier coefficient

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.