Hypercontractivity bounds for indicator functions

TheoremBonami–Beckner bound for indicator functions#✓fully proved

Bonami–Beckner for an indicator of uniform measure m: ∑_{S ≠ ∅} ρ^{2|S|} f̂(S)² ≤ m^{2/(1+ρ²)} - m² for 0 ≤ ρ ≤ 1.

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

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 uses\(L^q\) norm under the uniform measure on the cube · q-th moment under the uniform measure on the cube · Hypercontractivity in Fourier form · Walsh character on the Boolean cube

Used byIndicator-bound form of KKL implies the hypercontractive form · Bound on \(m - m^{2/(1+\rho^2)}\) by total influence

TheoremPoincaré inequality in Fourier form#✓fully proved

Poincaré inequality in Fourier form: ∑_{S ≠ ∅} f̂(S)² ≤ ∑_S 4 |S| f̂(S)².

theorem kls_var_le_W (φ : ConfigSpace ι → Bool) :
    (∑ S ∈ (univ.erase (∅ : Finset ι)),
        (khc_fourierCoeff (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2)
      ≤ ∑ S : Finset ι, 4 * (S.card : ℝ)
          * (khc_fourierCoeff (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2

Uses 2

Statement usesConfiguration space of a statistical-mechanics model · Fourier–Walsh coefficient under the uniform measure

DefinitionFourier-form KKL inequality given the indicator Bonami–Beckner bound#✓fully proved

The KKL inequality at p = 1/2 in Fourier form, with the indicator hypercontractive bound ∑_{S ≠ ∅} ρ^{2|S|} f̂(S)² ≤ m^{2/(1+ρ²)} - m² (for all ρ ∈ [0, 1]) as a hypothesis, where f = 1_φ and m = 𝔼 f. The hypothesis always holds (kls_fluctWeight_le_pow).

def kls_LogOptimisation (c : ℝ) : Prop :=
  ∀ {E : Type} [Fintype E] [DecidableEq E] [Nonempty E] (φ : ConfigSpace E → Bool),
    (∀ ρ : ℝ, 0 ≤ ρ → ρ ≤ 1 →
        (∑ S ∈ (univ.erase (∅ : Finset E)), (ρ ^ S.card) ^ 2
            * (khc_fourierCoeff (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2)
          ≤ (bnt_uexp (fun ω => if φ ω then (1 : ℝ) else 0)) ^ (2 / (1 + ρ ^ 2))
            - (bnt_uexp (fun ω => if φ ω then (1 : ℝ) else 0)) ^ 2) →
      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 5

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 byCapped-estimate form of KKL implies the indicator-bound form · Indicator-bound form of KKL implies the hypercontractive form · Indicator-bound form of KKL with constant 0 holds trivially · Indicator-bound form of KKL implies the KKL inequality at \(p = 1/2\) · Measure–influence form of KKL implies the indicator-bound form

TheoremIndicator-bound form of KKL with constant 0 holds trivially#✓fully proved

kls_LogOptimisation 0 holds trivially.

theorem kls_logOptimisation_zero : kls_LogOptimisation 0

Uses 6

Statement usesFourier-form KKL inequality given the indicator Bonami–Beckner 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

TheoremIndicator-bound form of KKL implies the hypercontractive form#✓fully proved

kls_LogOptimisation c implies khc_LogSobolevStep c.

theorem kls_logOptimisation_implies_step {c : ℝ} (H : kls_LogOptimisation c) :
    khc_LogSobolevStep c

Uses 6 · Used by 1

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

Proof usesConfiguration space of a statistical-mechanics model · \(L^q\) norm under the uniform measure on the cube · Fourier–Walsh coefficient under the uniform measure · Bonami–Beckner bound for indicator functions

Used byIndicator-bound form of KKL implies the KKL inequality at \(p = 1/2\)

TheoremIndicator-bound form of KKL implies the KKL inequality at \(p = 1/2\)#✓fully proved

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

theorem kls_logSobolevStep {c : ℝ} (H : kls_LogOptimisation c) :
    KKLHypercontractive (1 / 2 : ℝ) c

Uses 4 · Used by 2

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

Proof usesHypercontractive form of KKL implies the KKL inequality at \(p = 1/2\) · Indicator-bound form of KKL implies the hypercontractive form

Used byKKL inequality at \(p = 1/2\) from the conditional statement · Measure–influence form of KKL implies the KKL inequality at \(p = 1/2\)

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.