Log-sum estimates for damped influences under p-biased measures

DefinitionDamped influence of a coordinate#✓fully proved

The damped influence Dₑ(ρ) = ∑_{S ∋ e} ρ^{2|S \ {e}|} (f̂(S) / √(p(1-p)))² of coordinate e on the Boolean function φ under μ_p.

noncomputable def fsm2_dampWeight (p ρ : ℝ) (φ : ConfigSpace ι → Bool) (e : ι) : ℝ :=
  ∑ S ∈ univ.filter (fun S : Finset ι => e ∈ S),
    (ρ ^ (S.erase e).card) ^ 2 * (ptn_coeff p (fun ω => if φ ω then (1 : ℝ) else 0) S
      / ptn_sigma p) ^ 2

Uses 3 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · \(p\)-biased Fourier coefficient · Standard deviation of a Bernoulli bit

Used byHypercontractive bound on the damped influence · Damped influence is at most the influence · Damped influence at \(\rho = 1\) is the influence · Capped log-sum estimate for damped influences · Log-sum inequality for influences against damped influences

TheoremDamped influence at \(\rho = 1\) is the influence#✓fully proved

At ρ = 1 the damped influence is the influence.

theorem fsm2_dampWeight_one {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1)
    (φ : ConfigSpace ι → Bool) (e : ι) :
    fsm2_dampWeight p 1 φ e
      = OSSS.infl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0) e

Uses 7 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Influence of a coordinate · Damped influence of a coordinate

Proof uses\(p\)-biased Fourier coefficient · \(p\)-biased influence of a coordinate as Fourier weight · Standard deviation of a Bernoulli bit

Used byDamped influence is at most the influence

TheoremHypercontractive bound on the damped influence#✓fully proved

Hypercontractive bound on the damped influence: Dₑ(ρ) ≤ Infₑ^{2/q} when ρ² = 4p(1-p)(q-1) and 1 ≤ q ≤ 2.

theorem fsm2_dampWeight_le_hc {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 : ι) :
    fsm2_dampWeight p ρ φ e
      ≤ (OSSS.infl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0) e) ^ (2 / q)

Uses 5 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Influence of a coordinate · Damped influence of a coordinate

Proof uses\(p\)-biased hypercontractivity for a discrete derivative

Used byCapped log-sum estimate for damped influences

TheoremDamped influence is at most the influence#✓fully proved

The damped influence is at most the influence.

theorem fsm2_dampWeight_le_infl {p ρ : ℝ} (hp0 : 0 < p) (hp1 : p < 1) (h0 : 0 ≤ ρ) (h1 : ρ ≤ 1)
    (φ : ConfigSpace ι → Bool) (e : ι) :
    fsm2_dampWeight p ρ φ e
      ≤ OSSS.infl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0) e

Uses 7

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Influence of a coordinate · Damped influence of a coordinate

Proof usesDamped influence at \(\rho = 1\) is the influence · \(p\)-biased Fourier coefficient · Standard deviation of a Bernoulli bit

TheoremLog-sum inequality for influences against damped influences#✓fully proved

The log-sum inequality for the influences against the damped influences, over the coordinates of positive influence.

StatMech.Probability.fsm2_logSum_gain · 20 lines

theorem fsm2_logSum_gain {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)
    (_hpos : 0 < ∑ e ∈ univ.filter (fun e : ι =>
        0 < OSSS.infl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0) e),
      OSSS.infl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0) e) :
    (∑ e ∈ univ.filter (fun e : ι =>
        0 < OSSS.infl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0) e),
      OSSS.infl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0) e)
        * Real.log ((∑ e ∈ univ.filter (fun e : ι =>
            0 < OSSS.infl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0) e),
          OSSS.infl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0) e)
          / (∑ e ∈ univ.filter (fun e : ι =>
              0 < OSSS.infl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0) e),
            fsm2_dampWeight p ρ φ e))
      ≤ ∑ e ∈ univ.filter (fun e : ι =>
          0 < OSSS.infl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0) e),
        OSSS.infl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0) e
          * Real.log (OSSS.infl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0) e
              / fsm2_dampWeight p ρ φ e)

Uses 13 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Influence of a coordinate · Damped influence of a coordinate

Proof usesLog-sum inequality · Product probability weight · Expectation under a product weight · Probability of a configuration under a product weight · \(p\)-biased Fourier coefficient · \(p\)-biased influence of a coordinate as Fourier weight · Standard deviation of a Bernoulli bit · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Used byCapped log-sum estimate for damped influences

TheoremCapped log-sum estimate for damped influences#✓fully proved

The capped log-sum estimate: (∑ₑ Infₑ) · (2/q - 1) · log (1 / δ) ≤ ∑ₑ Infₑ · log (Infₑ / Dₑ(ρ)) (over coordinates of positive influence), with δ = maxₑ Infₑ ∈ (0, 1).

theorem fsm2_logGain_capped [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)
    (hTpos : 0 < totalInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0))
    (hδ0 : 0 < maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0))
    (_hδ1 : maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0) < 1) :
    totalInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)
        * (2 / q - 1)
        * Real.log (1 / maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0))
      ≤ ∑ e ∈ univ.filter (fun e : ι =>
          0 < OSSS.infl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0) e),
        OSSS.infl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0) e
          * Real.log (OSSS.infl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0) e
              / fsm2_dampWeight p ρ φ e)

Uses 17

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Influence of a coordinate · Damped influence of a coordinate · Maximal influence under a product weight · Total 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\) · Hypercontractive bound on the damped influence · Log-sum inequality for influences against damped influences · \(p\)-biased Fourier coefficient · \(p\)-biased influence of a coordinate as Fourier weight · Standard deviation of a Bernoulli bit · Closing a coordinate of a configuration · Opening a coordinate of a configuration

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.