Hypercontractivity applied to discrete derivatives

DefinitionDiscrete derivative in a coordinate#✓fully proved

The discrete derivative ∂ₑ f (ω) = f(ω^{e ↦ 1}) - f(ω^{e ↦ 0}).

noncomputable def bph_deriv (f : ConfigSpace ι → ℝ) (e : ι) : ConfigSpace ι → ℝ :=
  fun ω => f (StatMech.setOpen e ω) - f (StatMech.setClosed e ω)

Uses 3 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Used byBonami–Beckner applied to a discrete derivative · \(p\)-biased hypercontractivity for a discrete derivative

TheoremBonami–Beckner applied to a discrete derivative#✓fully proved

Bonami–Beckner applied to ∂ₑ 1_A: ∑_{S ∋ e} ρ^{2|S \ {e}|} · 4 f̂(S)² ≤ Infₑ(1_A)^{2/(1+ρ²)}.

theorem bph_perCoord_hc {ρ : ℝ} (h0 : 0 ≤ ρ) (h1 : ρ ≤ 1)
    (φ : ConfigSpace ι → Bool) (e : ι) :
    (∑ S ∈ univ.filter (fun S : Finset ι => e ∈ S),
        (ρ ^ (S.erase e).card) ^ 2
          * (4 * (khc_fourierCoeff (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2))
      ≤ (OSSS.infl (OSSS.bernoulliWeight (1 / 2 : ℝ))
          (fun ω => if φ ω then (1 : ℝ) else 0) e) ^ (2 / (1 + ρ ^ 2))

Uses 30 · Used by 1

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

Proof usesBoolean cube · Noise operator on the Boolean cube · Characters are eigenfunctions of the noise operator · Fourier character on the Boolean cube · Sum of a Boolean cube character · Product probability weight · Expectation under a product weight · Probability of a configuration under a product weight · Noise kernel on the Boolean cube · Noise operator on the Boolean cube · Agreement of the two noise operators on the Boolean cube · \(L^q\) norm under the uniform measure on the cube · q-th moment under the uniform measure on the cube · Uniform expectation on the Boolean cube · Discrete derivative in a coordinate · Cube bijection induced by an index bijection · Fourier inversion on the Boolean cube · Bonami–Beckner hypercontractive inequality · Reindexing a cube function along an index bijection · Reindexing preserves values at corresponding cube points · \(\pm 1\) value of a bit · Walsh character on the Boolean cube · Walsh character agrees with the canonical cube character up to sign · Reindexing a Walsh character reindexes its coordinate set · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Used bySummed per-coordinate Bonami–Beckner bound

TheoremSummed per-coordinate Bonami–Beckner bound#✓fully proved

bph_perCoord_hc summed over all coordinates.

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

Uses 5 · Used by 1

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

Proof usesBonami–Beckner applied to a discrete derivative

Used byCapped per-coordinate hypercontractive estimate

TheoremTermwise cap \(x^\theta \le \delta^{\theta-1} x\)#✓fully proved

x^θ ≤ δ^{θ-1} x for 0 ≤ x ≤ δ and θ ≥ 1.

theorem bph_cap_term (x δ θ : ℝ) (hx : 0 ≤ x) (hcap : x ≤ δ) (hθ : 1 ≤ θ) :
    x ^ θ ≤ δ ^ (θ - 1) * x

Used by 4

Used byLog-sum estimate for the fiber weights · Sum of influence powers capped by the maximal influence · Capped log-sum estimate for damped influences · Capped per-coordinate estimate under the \(p\)-biased measure

TheoremSum of influence powers capped by the maximal influence#✓fully proved

∑ₑ Infₑ^{θ} ≤ (maxₑ Infₑ)^{θ-1} ∑ₑ Infₑ with θ = 2/(1+ρ²).

theorem bph_cap_sum [Nonempty ι] {ρ : ℝ} (h0 : 0 ≤ ρ) (h1 : ρ ≤ 1) (φ : ConfigSpace ι → Bool) :
    (∑ e : ι, (OSSS.infl (OSSS.bernoulliWeight (1 / 2 : ℝ))
        (fun ω => if φ ω then (1 : ℝ) else 0) e) ^ (2 / (1 + ρ ^ 2)))
      ≤ (maxInfl (OSSS.bernoulliWeight (1 / 2 : ℝ)) (fun ω => if φ ω then (1 : ℝ) else 0))
          ^ (2 / (1 + ρ ^ 2) - 1)
        * (∑ S : Finset ι, 4 * (S.card : ℝ)
            * (khc_fourierCoeff (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2)

Uses 13 · Used by 1

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

Proof usesProduct probability weight · Expectation under a product weight · Probability of a configuration under a product weight · Termwise cap \(x^\theta \le \delta^{\theta-1} x\) · Total influence as Fourier weight · Total influence under a product weight · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Used byCapped per-coordinate hypercontractive estimate

TheoremCapped per-coordinate hypercontractive estimate#✓fully proved

The capped per-coordinate hypercontractive estimate: ∑_S 4 |S| ρ^{2(|S|-1)} f̂(S)² ≤ δ^{2/(1+ρ²) - 1} ∑_S 4 |S| f̂(S)², with δ = maxₑ Infₑ(1_A).

theorem bph_capped_hc [Nonempty ι] {ρ : ℝ} (h0 : 0 ≤ ρ) (h1 : ρ ≤ 1) (φ : ConfigSpace ι → Bool) :
    (∑ S : Finset ι, 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 ι, 4 * (S.card : ℝ)
            * (khc_fourierCoeff (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2)

Uses 7 · 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

Proof usesInfluence of a coordinate · Sum of influence powers capped by the maximal influence · Summed per-coordinate Bonami–Beckner bound

Used byCapped-estimate form of KKL implies the indicator-bound form

DefinitionFourier-form KKL at \(p = 1/2\) conditional on the capped estimate#✓fully proved

The KKL inequality at p = 1/2 in Fourier form, with the capped estimate bph_capped_hc (for all ρ ∈ [0, 1]) as a hypothesis. It holds with c = 2 (cro2_rhoOptimise).

StatMech.Probability.bph_RhoOptimise · 15 lines

def bph_RhoOptimise (c : ℝ) : Prop :=
  ∀ {E : Type} [Fintype E] [DecidableEq E] [Nonempty E] (φ : ConfigSpace E → Bool),
    (∀ ρ : ℝ, 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)) →
      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 4 · Used by 4

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 at \(p = 1/2\) from the conditional statement · Capped-estimate form of KKL implies the indicator-bound form · Conditional Fourier-form KKL holds trivially with constant zero · KKL inequality

TheoremConditional Fourier-form KKL holds trivially with constant zero#✓fully proved

bph_RhoOptimise 0 holds trivially.

theorem bph_rhoOptimise_zero : bph_RhoOptimise 0

Uses 5

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

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

TheoremCapped-estimate form of KKL implies the indicator-bound form#✓fully proved

bph_RhoOptimise c implies kls_LogOptimisation c.

theorem bph_logOptimisation_of_rho {c : ℝ} (H : bph_RhoOptimise c) :
    kls_LogOptimisation c

Uses 6 · Used by 1

Statement usesFourier-form KKL at \(p = 1/2\) conditional on the capped estimate · Fourier-form KKL inequality given the indicator Bonami–Beckner bound

Proof usesConfiguration space of a statistical-mechanics model · Uniform expectation on the Boolean cube · Capped per-coordinate hypercontractive estimate · Fourier–Walsh coefficient under the uniform measure

Used byKKL inequality at \(p = 1/2\) from the conditional statement

TheoremKKL inequality at \(p = 1/2\) from the conditional statement#✓fully proved

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

theorem bph_KKL {c : ℝ} (H : bph_RhoOptimise c) :
    KKLHypercontractive (1 / 2 : ℝ) c

Uses 4 · Used by 2

Statement usesKKL inequality with constant \(c\) for the \(p\)-biased measure · Fourier-form KKL at \(p = 1/2\) conditional on the capped estimate

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

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

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.