The edge-isoperimetric inequality and the logarithmic KKL reduction

TheoremBernoulli's inequality \(1 - x^k \le k(1 - x)\)#✓fully proved

Bernoulli's inequality in the form 1 - x^k ≤ k (1 - x) for 0 ≤ x (the hypothesis x ≤ 1 is not needed). See also one_add_mul_le_pow.

theorem klo_one_sub_pow_le (x : ℝ) (h0 : 0 ≤ x) (_h1 : x ≤ 1) (k : ℕ) :
    1 - x ^ k ≤ (1 - x) * k

Used by 1

Used byBound on \(m - m^{2/(1+\rho^2)}\) by total influence

TheoremBound on \(m - m^{2/(1+\rho^2)}\) by total influence#✓fully proved

For an event of uniform measure m and total influence I = ∑_S 4 |S| f̂(S)², m - m^{2/(1+ρ²)} ≤ (1 - ρ²) I / 4 for 0 ≤ ρ ≤ 1.

theorem klo_master_le (φ : ConfigSpace ι → Bool) (ρ : ℝ) (h0 : 0 ≤ ρ) (h1 : ρ ≤ 1) :
    bnt_uexp (fun ω => if φ ω then (1 : ℝ) else 0)
        - (bnt_uexp (fun ω => if φ ω then (1 : ℝ) else 0)) ^ (2 / (1 + ρ ^ 2))
      ≤ (1 - ρ ^ 2) * (∑ S : Finset ι, 4 * (S.card : ℝ)
          * (khc_fourierCoeff (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2) / 4

Uses 7 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Uniform expectation on the Boolean cube · Fourier–Walsh coefficient under the uniform measure

Proof usesParseval's identity on the Boolean cube · Walsh character on the Boolean cube · Bernoulli's inequality \(1 - x^k \le k(1 - x)\) · Bonami–Beckner bound for indicator functions

Used byEdge-isoperimetric inequality · Measure–influence form of KKL implies the indicator-bound form

TheoremEdge-isoperimetric inequality#✓fully proved

Edge-isoperimetric inequality on the discrete cube (S. Hart, A note on the edges of the n-cube, Discrete Math. 1976): an event of uniform measure m > 0 has total influence at least 2 m log (1 / m). Here log is the natural logarithm, so this is weaker by the factor log 2 than the sharp bound 2 m log₂ (1 / m).

theorem klo_edge_isoperimetric (φ : ConfigSpace ι → Bool)
    (hm0 : 0 < bnt_uexp (fun ω => if φ ω then (1 : ℝ) else 0)) :
    2 * bnt_uexp (fun ω => if φ ω then (1 : ℝ) else 0)
        * Real.log (1 / bnt_uexp (fun ω => if φ ω then (1 : ℝ) else 0))
      ≤ ∑ S : Finset ι, 4 * (S.card : ℝ)
          * (khc_fourierCoeff (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2

Uses 4

Statement usesConfiguration space of a statistical-mechanics model · Uniform expectation on the Boolean cube · Fourier–Walsh coefficient under the uniform measure

Proof usesBound on \(m - m^{2/(1+\rho^2)}\) by total influence

DefinitionFourier-form KKL inequality given the measure–influence bound#✓fully proved

The KKL inequality at p = 1/2 in Fourier form, with the bound m - m^{2/(1+ρ²)} ≤ (1 - ρ²) I / 4 (for all ρ ∈ [0, 1]) as a hypothesis, where m is the measure and I the total influence of φ. The hypothesis always holds (klo_master_le).

def klo_DeltaUpgrade (c : ℝ) : Prop :=
  ∀ {E : Type} [Fintype E] [DecidableEq E] [Nonempty E] (φ : ConfigSpace E → Bool),
    (∀ ρ : ℝ, 0 ≤ ρ → ρ ≤ 1 →
        bnt_uexp (fun ω => if φ ω then (1 : ℝ) else 0)
            - (bnt_uexp (fun ω => if φ ω then (1 : ℝ) else 0)) ^ (2 / (1 + ρ ^ 2))
          ≤ (1 - ρ ^ 2) * (∑ S : Finset E, 4 * (S.card : ℝ)
              * (khc_fourierCoeff (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2) / 4) →
      c * (∑ S ∈ (univ.erase (∅ : Finset E)),
            (khc_fourierCoeff (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2)
          * Real.log (1 / maxInfl (OSSS.bernoulliWeight (1 / 2 : ℝ))
              (fun ω => if φ ω then (1 : ℝ) else 0))
        ≤ ∑ S : Finset E, 4 * (S.card : ℝ)
            * (khc_fourierCoeff (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2

Uses 5 · Used by 3

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

Used byMeasure–influence form of KKL with constant 0 holds trivially · Measure–influence form of KKL implies the KKL inequality at \(p = 1/2\) · Measure–influence form of KKL implies the indicator-bound form

TheoremMeasure–influence form of KKL with constant 0 holds trivially#✓fully proved

klo_DeltaUpgrade 0 holds trivially.

theorem klo_deltaUpgrade_zero : klo_DeltaUpgrade 0

Uses 6

Statement usesFourier-form KKL inequality given the measure–influence bound

Proof usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Uniform expectation on the Boolean cube · Fourier–Walsh coefficient under the uniform measure · Maximal influence under a product weight

TheoremMeasure–influence form of KKL implies the indicator-bound form#✓fully proved

klo_DeltaUpgrade c implies kls_LogOptimisation c.

theorem klo_logOptimisation_of_deltaUpgrade {c : ℝ} (H : klo_DeltaUpgrade c) :
    kls_LogOptimisation c

Uses 6 · Used by 1

Statement usesFourier-form KKL inequality given the measure–influence bound · Fourier-form KKL inequality given the indicator Bonami–Beckner bound

Proof usesConfiguration space of a statistical-mechanics model · Uniform expectation on the Boolean cube · Fourier–Walsh coefficient under the uniform measure · Bound on \(m - m^{2/(1+\rho^2)}\) by total influence

Used byMeasure–influence form of KKL implies the KKL inequality at \(p = 1/2\)

TheoremMeasure–influence form of KKL implies the KKL inequality at \(p = 1/2\)#✓fully proved

klo_DeltaUpgrade c implies the KKL inequality KKLHypercontractive (1/2) c.

theorem klo_logOptimisation {c : ℝ} (H : klo_DeltaUpgrade c) :
    KKLHypercontractive (1 / 2 : ℝ) c

Uses 4

Statement usesKKL inequality with constant \(c\) for the \(p\)-biased measure · Fourier-form KKL inequality given the measure–influence bound

Proof usesMeasure–influence form of KKL implies the indicator-bound form · Indicator-bound form of KKL implies the KKL inequality at \(p = 1/2\)

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.