The KKL inequality on the uniform cube with constant 2

TheoremIntegral of \(e^{cx}\) over an interval#✓fully proved

∫_a^b exp (c x) dx = (exp (c b) - exp (c a)) / c for c ≠ 0.

theorem cro2_integral_exp_mul (c : ℝ) (hc : c ≠ 0) (a b : ℝ) :
    ∫ x in a..b, Real.exp (c * x) = (Real.exp (c * b) - Real.exp (c * a)) / c

Used by 1

Used byBound on the integral of \(e^{-tu/2}\) over \((0, 1)\)

TheoremBound on the integral of \(e^{-tu/2}\) over \((0, 1)\)#✓fully proved

∫₀¹ exp (-(t/2) u) du ≤ 2 / t for t > 0.

theorem cro2_integral_exp_le (t : ℝ) (ht : 0 < t) :
    (∫ u in (0 : ℝ)..1, Real.exp (-(t / 2) * u)) ≤ 2 / t

Uses 1 · Used by 1

Proof usesIntegral of \(e^{cx}\) over an interval

Used byBound on the integral of \(\delta^{u/(2-u)}\) over \((0, 1)\)

TheoremIntegral of \((1 - u)^n\) over \((0, 1)\)#✓fully proved

∫₀¹ (1 - u)^n du = 1 / (n + 1).

theorem cro2_integral_one_sub_pow (n : ℕ) :
    ∫ u in (0 : ℝ)..1, (1 - u) ^ n = 1 / (n + 1)

Used by 2

Used byIntegrating damped total-influence weights over the noise parameter · Integral of damped total-influence weights over the noise parameter

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

Integrating the damped total-influence weights over the noise parameter: ∫₀¹ ∑_S 4 |S| (1-u)^{|S|-1} c_S du = 4 ∑_{S ≠ ∅} c_S.

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

Uses 1 · Used by 2

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

Used byCapped estimate implies KKL with constant 2 on \((1/2, q)\) · KKL inequality

TheoremBound on the integral of \(\delta^{u/(2-u)}\) over \((0, 1)\)#✓fully proved

∫₀¹ δ^{u/(2-u)} du ≤ 2 / log (1/δ) for 0 < δ < 1.

theorem cro2_integral_rhs_le (δ : ℝ) (hδ0 : 0 < δ) (hδ1 : δ < 1) :
    (∫ u in (0 : ℝ)..1, δ ^ (u / (2 - u))) ≤ 2 / (-(Real.log δ))

Uses 1 · Used by 3

Proof usesBound on the integral of \(e^{-tu/2}\) over \((0, 1)\)

Used byDamped KKL inequality under the \(p\)-biased measure · Capped estimate implies KKL with constant 2 on \((1/2, q)\) · KKL inequality

TheoremCapped estimate rewritten in the variable \(u = 1 - \rho^2\)#✓fully proved

The capped estimate in the variable u = 1 - ρ²: ∑_S 4 |S| (1-u)^{|S|-1} f̂(S)² ≤ δ^{u/(2-u)} ∑_S 4 |S| f̂(S)².

StatMech.Probability.cro2_master_sub · 16 lines

theorem cro2_master_sub {E : Type} [Fintype E] [DecidableEq E] [Nonempty E]
    (φ : ConfigSpace E → Bool)
    (Hcap : ∀ ρ : ℝ, 0 ≤ ρ → ρ ≤ 1 →
        (∑ S : Finset E, 4 * (S.card : ℝ) * (ρ ^ (S.card - 1)) ^ 2
            * (khc_fourierCoeff (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2)
          ≤ (maxInfl (OSSS.bernoulliWeight (1 / 2 : ℝ)) (fun ω => if φ ω then (1 : ℝ) else 0))
              ^ (2 / (1 + ρ ^ 2) - 1)
            * (∑ S : Finset E, 4 * (S.card : ℝ)
                * (khc_fourierCoeff (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2))
    (u : ℝ) (hu0 : 0 ≤ u) (hu1 : u ≤ 1) :
    (∑ S : Finset E, 4 * (S.card : ℝ) * (1 - u) ^ (S.card - 1)
        * (khc_fourierCoeff (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2)
      ≤ (maxInfl (OSSS.bernoulliWeight (1 / 2 : ℝ)) (fun ω => if φ ω then (1 : ℝ) else 0))
          ^ (u / (2 - u))
        * (∑ S : Finset E, 4 * (S.card : ℝ)
            * (khc_fourierCoeff (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2)

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Fourier–Walsh coefficient under the uniform measure · Maximal influence under a product weight

Used byKKL inequality

TheoremKKL inequality#✓fully proved

KKL inequality for the uniform measure, Fourier form with constant 2 (after J. Kahn, G. Kalai, N. Linial, The influence of variables on Boolean functions, FOCS 1988; this proof follows D. Falik, A. Samorodnitsky, Edge-isoperimetric inequalities and influences, 2007): 2 · ∑_{S ≠ ∅} f̂(S)² · log (1 / maxₑ Infₑ) ≤ ∑_S 4 |S| f̂(S)² for every Boolean function.

theorem cro2_rhoOptimise : bph_RhoOptimise 2

Uses 14 · Used by 2

Statement usesFourier-form KKL at \(p = 1/2\) conditional on the capped estimate

Proof usesConfiguration space of a statistical-mechanics model · Product probability weight · Bernoulli product weight · Expectation under a product weight · Influence of a coordinate · Probability of a configuration under a product weight · Integral of damped total-influence weights over the noise parameter · Bound on the integral of \(\delta^{u/(2-u)}\) over \((0, 1)\) · Capped estimate rewritten in the variable \(u = 1 - \rho^2\) · Fourier–Walsh coefficient under the uniform measure · Maximal influence under a product weight · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Used byKahn–Kalai–Linial inequality · Kahn–Kalai–Linial inequality

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.