Decomposition of the variance by maximal element

DefinitionMaximal element of a finite set#✓fully proved

The maximal element of S, or an arbitrary element if S is empty.

noncomputable def mxd_maxE [Nonempty ι] (S : Finset ι) : ι :=
  if h : S.Nonempty then S.max' h else Classical.arbitrary ι

Used by 3

Used byHypercontractive bound on the damped fiber weight · Nonempty subsets with a given maximal element · Variance decomposition by maximal element

DefinitionNonempty subsets with a given maximal element#✓fully proved

The nonempty subsets of ι whose maximal element is e.

noncomputable def mxd_fiber [Nonempty ι] (e : ι) : Finset (Finset ι) :=
  (univ.erase (∅ : Finset ι)).filter (fun S => mxd_maxE S = e)

Uses 1 · Used by 5

Statement usesMaximal element of a finite set

Used byNoise-damped fiber weight · Hypercontractive bound on the damped fiber weight · Fourier weight of a maximal-element fiber · Log-sum estimate for the fiber weights · Variance decomposition by maximal element

DefinitionFourier weight of a maximal-element fiber#✓fully proved

The p-biased Fourier weight Wₑ = ∑_{S : max S = e} f̂(S)² of the fiber of e.

noncomputable def mxd_fiberWeight [Nonempty ι] (p : ℝ) (φ : ConfigSpace ι → Bool) (e : ι) : ℝ :=
  ∑ S ∈ mxd_fiber e, (ptn_coeff p (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2

Uses 3 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Nonempty subsets with a given maximal element · \(p\)-biased Fourier coefficient

Used byLog-sum estimate for the fiber weights · Variance decomposition by maximal element

TheoremVariance decomposition by maximal element#✓fully proved

The variance of a Boolean function is the sum of the fiber weights.

theorem mxd_var_decomp [Nonempty ι] {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1)
    (φ : ConfigSpace ι → Bool) :
    OSSS.var (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)
      = ∑ e : ι, mxd_fiberWeight p φ e

Uses 8 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Variance under a product weight · Fourier weight of a maximal-element fiber

Proof usesNonempty subsets with a given maximal element · Maximal element of a finite set · \(p\)-biased Fourier coefficient · \(p\)-biased variance as Fourier weight off the empty set

Used byLog-sum estimate for the fiber weights

DefinitionNoise-damped fiber weight#✓fully proved

The noise-damped fiber weight ∑_{S : max S = e} ρ^{2|S|} f̂(S)².

noncomputable def mxd_dampFiber [Nonempty ι] (p ρ : ℝ) (φ : ConfigSpace ι → Bool) (e : ι) : ℝ :=
  ∑ S ∈ mxd_fiber e, (ρ ^ S.card) ^ 2
    * (ptn_coeff p (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2

Uses 3 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Nonempty subsets with a given maximal element · \(p\)-biased Fourier coefficient

Used byHypercontractive bound on the damped fiber weight · Log-sum estimate for the fiber weights

TheoremHypercontractive bound on the damped fiber weight#✓fully proved

Hypercontractive bound on the damped fiber weight.

theorem mxd_dampFiber_le_perCoord [Nonempty ι] {p ρ q : ℝ} (hp0 : 0 < p) (hp1 : p < 1)
    (h0 : 0 ≤ ρ) (h1 : ρ ≤ 1) (hq1 : 1 ≤ q) (hq2 : q ≤ 2)
    (hρsq : ρ ^ 2 = (q - 1) * 4 * p * (1 - p)) (φ : ConfigSpace ι → Bool) (e : ι) :
    mxd_dampFiber p ρ φ e
      ≤ ρ ^ 2 * (ptn_sigma p) ^ 2
        * (OSSS.infl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0) e) ^
            (2 / q)

Uses 9 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Influence of a coordinate · Noise-damped fiber weight · Standard deviation of a Bernoulli bit

Proof usesNonempty subsets with a given maximal element · Maximal element of a finite set · \(p\)-biased Fourier coefficient · \(p\)-biased hypercontractivity for a discrete derivative

Used byLog-sum estimate for the fiber weights

TheoremLog-sum estimate for the fiber weights#✓fully proved

The variance log-sum estimate for the fiber weights against their damped versions.

theorem mxd_logSum_gain [Nonempty ι] {p ρ q : ℝ} (hp0 : 0 < p) (hp1 : p < 1)
    (hρ : 0 < ρ) (h1 : ρ ≤ 1) (hq1 : 1 ≤ q) (hq2 : q ≤ 2)
    (hρsq : ρ ^ 2 = (q - 1) * 4 * p * (1 - p)) (φ : ConfigSpace ι → Bool)
    (hVpos : 0 < OSSS.var (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0))
    (hδ0 : 0 < maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0))
    (hTpos : 0 < totalInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)) :
    OSSS.var (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)
        * Real.log (OSSS.var (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)
          / (ρ ^ 2 * (ptn_sigma p) ^ 2
            * ((maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)) ^
                (2 / q - 1)
              * totalInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0))))
      ≤ ∑ e ∈ univ.filter (fun e : ι => 0 < mxd_fiberWeight p φ e),
        mxd_fiberWeight p φ e * Real.log (mxd_fiberWeight p φ e / mxd_dampFiber p ρ φ e)

Uses 20

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Variance under a product weight · Maximal influence under a product weight · Noise-damped fiber weight · Fourier weight of a maximal-element fiber · Standard deviation of a Bernoulli bit · Total influence under a product weight

Proof usesLog-sum inequality · Product probability weight · Expectation under a product weight · Influence of a coordinate · Probability of a configuration under a product weight · Termwise cap \(x^\theta \le \delta^{\theta-1} x\) · Hypercontractive bound on the damped fiber weight · Nonempty subsets with a given maximal element · Variance decomposition by maximal element · \(p\)-biased Fourier coefficient · Closing a coordinate of a configuration · Opening a coordinate of a configuration

DefinitionCapped influence estimate for all \(p\) in \((1/2, q)\)#✓fully proved

The capped estimate ∑_S 4 |S| (1-u)^{|S|-1} f̂(S)² ≤ δ^{u/(2-u)} ∑ₑ Infₑ for all p ∈ (1/2, q) with p < 1 and all u ∈ [0, 1].

def mxd_martingaleHC_statement (q : ℝ) : Prop :=
  ∀ p ∈ Set.Ioo (1 / 2 : ℝ) q, p < 1 → ∀ {E : Type} [Fintype E] [DecidableEq E] [Nonempty E]
    (φ : ConfigSpace E → Bool), ∀ u : ℝ, 0 ≤ u → u ≤ 1 →
      (∑ S : Finset E, 4 * (S.card : ℝ) * (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 5 · Used by 5

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

Used byCapped estimate implies KKL with constant 2 on \((1/2, q)\) · Low-degree case implies the full capped estimate on \((1/2, q)\) · Small-influence case implies the full capped estimate on \((1/2, q)\) · Low-range case implies the full capped estimate on \((1/2, q)\) · Open-interval case implies the full capped estimate on \((1/2, q)\)

TheoremCapped estimate implies KKL with constant 2 on \((1/2, q)\)#✓fully proved

mxd_martingaleHC_statement q implies ptn_RhoOptimise q, hence the KKL inequality with constant 2 on (1/2, q).

theorem mxd_rhoOptimise_of_martingaleHC {q : ℝ} (H : mxd_martingaleHC_statement q) :
    ptn_RhoOptimise q

Uses 18

Statement usesCapped influence estimate for all \(p\) in \((1/2, q)\) · \(p\)-biased KKL inequality 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 · Variance under a product weight · 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)\) · Maximal influence under a product weight · \(p\)-biased Fourier coefficient · Standard deviation of a Bernoulli bit · \(p\)-biased variance as Fourier weight off the empty set · Total influence under a product weight · Closing a coordinate of a configuration · Opening a coordinate of a configuration

TheoremCapped estimate with zero weights holds trivially#✓fully proved

The capped estimate with all weights multiplied by 0 holds trivially.

theorem mxd_martingaleHC_c0 {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1)
    {E : Type} [Fintype E] [DecidableEq E] [Nonempty E] (φ : ConfigSpace E → Bool)
    (u : ℝ) :
    (∑ S : Finset E, (0 : ℝ) * (S.card : ℝ) * (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 11

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 · Closing a coordinate of a configuration · Opening a coordinate of a configuration

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.