PBiased Tensorize

DefinitionZero-one value of a bit#✓fully proved

The 0/1 value of a bit.

def ptn_val (b : Bool) : ℝ := if b then 1 else 0

Used by 7

Used byNormalized bit at \(p = 1/2\) is \(-(-1)^b\) · \(p\)-biased Fourier inversion · \(p\)-biased influence of a coordinate as Fourier weight · Kernel and Fourier noise operators agree · Orthonormality of the \(p\)-biased characters · \(p\)-biased hypercontractivity for a discrete derivative · Normalized Bernoulli bit

DefinitionStandard deviation of a Bernoulli bit#✓fully proved

The standard deviation √(p(1-p)) of a Bernoulli(p) bit.

noncomputable def ptn_sigma (p : ℝ) : ℝ := Real.sqrt (p * (1 - p))

Used by 38

Used byCapped \(p\)-biased per-coordinate estimate in the variable \(u\) · Hypercontractive bound on the damped fiber weight · Log-sum estimate for the fiber weights · Capped estimate implies KKL with constant 2 on \((1/2, q)\) · Fourier total weight equals \(4p(1-p)\) times the total influence · Low-degree case implies the low-range case · Low-degree residual case of the capped estimate · Damped influence of a coordinate · 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 · Low-range case condition fails for some \(u\) · Capped estimate in the hypercontractive range with matching \(q'\) · Under the gap condition the hypercontractive bound is dominated · Gap condition holds at \(u = 1\) · Low-range residual case of the capped estimate · Gap condition holds at some \(u < 1\) in the hypercontractive range · Low-range case implies the small-influence case · Capped estimate at \(p = 1/2\) for all \(u \in (0, 1)\) · Target-exponent capped estimate under the gap condition · Target-exponent capped estimate from a domination bound · Damped total weight at \(u = 0\) is at most the total influence · Capped estimate in the hypercontractive range · Capped estimate at the endpoint \(u = 1\) · Damped total weight as a sum of per-coordinate weights · Per-coordinate damped weight · Normalized bit at \(p = 1/2\) is \(-(-1)^b\) · Capped per-coordinate estimate under the \(p\)-biased measure · \(p\)-biased Fourier inversion · \(p\)-biased influence of a coordinate as Fourier weight · Kernel and Fourier noise operators agree · Orthonormality of the \(p\)-biased characters · \(p\)-biased hypercontractivity for a discrete derivative · Normalized Bernoulli bit · \(p\)-biased KKL inequality conditional on the capped estimate · Summed per-coordinate \(p\)-biased hypercontractive bound · \(p\)-biased total influence as Fourier weight

DefinitionNormalized Bernoulli bit#✓fully proved

The normalized Bernoulli(p) bit ψ(b) = (b - p) / √(p(1-p)), which has mean 0 and variance 1.

noncomputable def ptn_psi (p : ℝ) (b : Bool) : ℝ := (ptn_val b - p) / ptn_sigma p

Uses 2 · Used by 8

Statement usesStandard deviation of a Bernoulli bit · Zero-one value of a bit

Used by\(p\)-biased character at \(p = 1/2\) is the Walsh character up to sign · Normalized bit at \(p = 1/2\) is \(-(-1)^b\) · \(p\)-biased Fourier inversion · \(p\)-biased influence of a coordinate as Fourier weight · Kernel and Fourier noise operators agree · Orthonormality of the \(p\)-biased characters · \(p\)-biased character · \(p\)-biased hypercontractivity for a discrete derivative

TheoremExpectations of product functions factor under product measure#✓fully proved

Expectations of product functions factor under the product measure.

theorem ptn_expect_prod (p : ℝ) (h : ι → Bool → ℝ) :
    OSSS.expect (OSSS.bernoulliWeight p) (fun ω => ∏ e : ι, h e (ω e))
      = ∏ e : ι, ((1 - p) * h e false + p * h e true)

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Expectation under a product weight

Proof usesProbability of a configuration under a product weight

Used byOrthonormality of the \(p\)-biased characters

Definition\(p\)-biased character#✓fully proved

The p-biased character φ_S(ω) = ∏_{i ∈ S} ψ(ω i).

noncomputable def ptn_pchar (p : ℝ) (S : Finset ι) (ω : ConfigSpace ι) : ℝ :=
  ∏ i ∈ S, ptn_psi p (ω i)

Uses 2 · Used by 13

Statement usesConfiguration space of a statistical-mechanics model · Normalized Bernoulli bit

Used bySquared \(p\)-biased and Walsh coefficients agree at \(p = 1/2\) · \(p\)-biased character at \(p = 1/2\) is the Walsh character up to sign · \(p\)-biased Fourier coefficient · \(p\)-biased Fourier inversion · \(p\)-biased influence of a coordinate as Fourier weight · Kernel and Fourier noise operators agree · Fourier form of \(p\)-biased hypercontractivity on finite index types · Fourier form of \(p\)-biased hypercontractivity on \(\{0, 1\}^n\) · \(p\)-biased noise operator on the Fourier side · Orthonormality of the \(p\)-biased characters · Parseval's identity under the \(p\)-biased measure · \(p\)-biased hypercontractivity for a discrete derivative · \(p\)-biased variance as Fourier weight off the empty set

TheoremOrthonormality of the \(p\)-biased characters#✓fully proved

The p-biased characters are orthonormal in L²(μ_p).

theorem ptn_orthonormal {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1) (S T : Finset ι) :
    OSSS.expect (OSSS.bernoulliWeight p) (fun ω => ptn_pchar p S ω * ptn_pchar p T ω)
      = if S = T then 1 else 0

Uses 8 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Expectation under a product weight · \(p\)-biased character

Proof usesExpectations of product functions factor under product measure · Normalized Bernoulli bit · Standard deviation of a Bernoulli bit · Zero-one value of a bit

Used by\(p\)-biased influence of a coordinate as Fourier weight · Fourier form of \(p\)-biased hypercontractivity on finite index types · Fourier form of \(p\)-biased hypercontractivity on \(\{0, 1\}^n\) · Parseval's identity under the \(p\)-biased measure · \(p\)-biased hypercontractivity for a discrete derivative

Definition\(p\)-biased Fourier coefficient#✓fully proved

The p-biased Fourier coefficient f̂(S) = 𝔼_p[f φ_S].

noncomputable def ptn_coeff (p : ℝ) (f : ConfigSpace ι → ℝ) (S : Finset ι) : ℝ :=
  OSSS.expect (OSSS.bernoulliWeight p) (fun ω => f ω * ptn_pchar p S ω)

Uses 4 · Used by 55

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Expectation under a product weight · \(p\)-biased character

Used byDamped KKL inequality under the \(p\)-biased measure · KKL inequality with constant \(2\) at \(p = 1/2\) · Capped \(p\)-biased per-coordinate estimate in the variable \(u\) · Damped variance equals the variance at \(p = 1/2\) · Noise-damped fiber weight · Hypercontractive bound on the damped fiber weight · Fourier weight of a maximal-element fiber · Log-sum estimate for the fiber weights · Capped estimate with zero weights holds trivially · Capped influence estimate for all \(p\) in \((1/2, q)\) · Capped estimate implies KKL with constant 2 on \((1/2, q)\) · Variance decomposition by maximal element · Fourier total weight equals \(4p(1-p)\) times the total influence · Bound on the high-degree part of the damped total weight · Low-degree case implies the low-range case · Low-degree residual case of the capped estimate · Capped estimate from its low-degree part · Damped influence of a coordinate · 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 · Convexity of the damped total weight · Capped estimate when the maximal influence is at least \(e^{-1}\) · Capped estimate on \((0, 1)\) from concavity of the right side · Small-influence case implies the open-interval case · Small-influence residual case of the capped estimate · Capped estimate in the hypercontractive range with matching \(q'\) · Low-range residual case of the capped estimate · Low-range case implies the small-influence case · Capped estimate at \(p = 1/2\) for all \(u \in (0, 1)\) · Target-exponent capped estimate under the gap condition · Target-exponent capped estimate from a domination bound · Damped total weight at \(u = 0\) is at most the total influence · Capped estimate in the hypercontractive range · Capped estimate at the endpoint \(u = 1\) · Damped total weight as a sum of per-coordinate weights · Open-interval case implies the full capped estimate on \((1/2, q)\) · Open-interval residual case of the capped estimate · Per-coordinate damped weight · Squared \(p\)-biased and Walsh coefficients agree at \(p = 1/2\) · Total influence at \(p = 1/2\) via \(p\)-biased Fourier coefficients · Capped per-coordinate estimate under the \(p\)-biased measure · \(p\)-biased Fourier inversion · \(p\)-biased influence of a coordinate as Fourier weight · Kernel and Fourier noise operators agree · Fourier form of \(p\)-biased hypercontractivity on finite index types · Fourier form of \(p\)-biased hypercontractivity on \(\{0, 1\}^n\) · \(p\)-biased noise operator on the Fourier side · Parseval's identity under the \(p\)-biased measure · \(p\)-biased hypercontractivity for a discrete derivative · \(p\)-biased KKL inequality conditional on the capped estimate · Summed per-coordinate \(p\)-biased hypercontractive bound · \(p\)-biased total influence as Fourier weight · \(p\)-biased variance as Fourier weight off the empty set

Theorem\(p\)-biased Fourier inversion#✓fully proved

Fourier inversion under μ_p: f = ∑_S f̂(S) φ_S for 0 < p < 1.

theorem ptn_expansion {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1)
    (f : ConfigSpace ι → ℝ) (x : ConfigSpace ι) :
    (∑ S : Finset ι, ptn_coeff p f S * ptn_pchar p S x) = f x

Uses 8 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · \(p\)-biased Fourier coefficient · \(p\)-biased character

Proof usesBernoulli product weight · Probability of a configuration under a product weight · Normalized Bernoulli bit · Standard deviation of a Bernoulli bit · Zero-one value of a bit

Used by\(p\)-biased influence of a coordinate as Fourier weight · Kernel and Fourier noise operators agree · Parseval's identity under the \(p\)-biased measure · \(p\)-biased hypercontractivity for a discrete derivative

TheoremParseval's identity under the \(p\)-biased measure#✓fully proved

Parseval's identity under μ_p: 𝔼_p[f g] = ∑_S f̂(S) ĝ(S).

theorem ptn_parseval {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1) (f g : ConfigSpace ι → ℝ) :
    OSSS.expect (OSSS.bernoulliWeight p) (fun ω => f ω * g ω)
      = ∑ S : Finset ι, ptn_coeff p f S * ptn_coeff p g S

Uses 8 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Expectation under a product weight · \(p\)-biased Fourier coefficient

Proof usesProbability of a configuration under a product weight · \(p\)-biased Fourier inversion · Orthonormality of the \(p\)-biased characters · \(p\)-biased character

Used by\(p\)-biased variance as Fourier weight off the empty set

Theorem\(p\)-biased variance as Fourier weight off the empty set#✓fully proved

The variance under μ_p is the Fourier weight off the empty set.

theorem ptn_var_eq_fourierWeight {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1) (f : ConfigSpace ι → ℝ) :
    OSSS.var (OSSS.bernoulliWeight p) f
      = ∑ S ∈ (univ.erase (∅ : Finset ι)), (ptn_coeff p f S) ^ 2

Uses 8 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Variance under a product weight · \(p\)-biased Fourier coefficient

Proof usesCovariance under a product weight · Expectation under a product weight · Parseval's identity under the \(p\)-biased measure · \(p\)-biased character

Used byDamped variance equals the variance at \(p = 1/2\) · Capped estimate implies KKL with constant 2 on \((1/2, q)\) · Variance decomposition by maximal element

Theorem\(p\)-biased influence of a coordinate as Fourier weight#✓fully proved

The influence of e on a Boolean function under μ_p is ∑_{S ∋ e} f̂(S)² / (p(1-p)).

theorem ptn_infl_eq_fourierWeight {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1)
    (φ : ConfigSpace ι → Bool) (e : ι) :
    OSSS.infl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0) e
      = (1 / (ptn_sigma p) ^ 2) * ∑ S ∈ univ.filter (fun S : Finset ι => e ∈ S),
          (ptn_coeff p (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2

Uses 14 · Used by 4

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

Proof usesExpectation under a product weight · Probability of a configuration under a product weight · \(p\)-biased Fourier inversion · Orthonormality of the \(p\)-biased characters · \(p\)-biased character · Normalized Bernoulli bit · Zero-one value of a bit · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Used byDamped influence at \(\rho = 1\) is the influence · Capped log-sum estimate for damped influences · Log-sum inequality for influences against damped influences · \(p\)-biased total influence as Fourier weight

Theorem\(p\)-biased total influence as Fourier weight#✓fully proved

The total influence of a Boolean function under μ_p is ∑_S |S| f̂(S)² / (p(1-p)).

theorem ptn_totalInfl_eq_fourierWeight {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1)
    (φ : ConfigSpace ι → Bool) :
    totalInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)
      = (1 / (ptn_sigma p) ^ 2) * ∑ S : Finset ι, (S.card : ℝ)
          * (ptn_coeff p (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2

Uses 7 · Used by 2

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

Proof usesInfluence of a coordinate · \(p\)-biased influence of a coordinate as Fourier weight

Used byFourier total weight equals \(4p(1-p)\) times the total influence · Damped total weight at \(u = 0\) is at most the total influence

Definition\(q\)-th moment under the \(p\)-biased measure#✓fully proved

The q-th moment 𝔼_p |f|^q.

noncomputable def ptn_qnormPow (p q : ℝ) (f : ConfigSpace ι → ℝ) : ℝ :=
  OSSS.expect (OSSS.bernoulliWeight p) (fun ω => |f ω| ^ q)

Uses 3 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Expectation under a product weight

Used by\(p\)-biased hypercontractivity on \(\{0, 1\}^n\) · Fourier form of \(p\)-biased hypercontractivity on finite index types · Fourier form of \(p\)-biased hypercontractivity on \(\{0, 1\}^n\) · \(p\)-biased hypercontractivity for a discrete derivative · \(L^q\) norm under the \(p\)-biased measure · Tensorization step for \(p\)-biased hypercontractivity

Definition\(L^q\) norm under the \(p\)-biased measure#✓fully proved

The L^q(μ_p) norm (𝔼_p |f|^q)^{1/q}.

noncomputable def ptn_qnorm (p q : ℝ) (f : ConfigSpace ι → ℝ) : ℝ :=
  (ptn_qnormPow p q f) ^ (1 / q)

Uses 2 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · \(q\)-th moment under the \(p\)-biased measure

Used by\(p\)-biased hypercontractivity on \(\{0, 1\}^n\) · Fourier form of \(p\)-biased hypercontractivity on finite index types · Fourier form of \(p\)-biased hypercontractivity on \(\{0, 1\}^n\) · \(p\)-biased hypercontractivity for a discrete derivative · Tensorization step for \(p\)-biased hypercontractivity

Definition\(p\)-biased noise operator on the Fourier side#✓fully proved

The p-biased noise operator on the Fourier side: T_ρ f = ∑_S ρ^{|S|} f̂(S) φ_S.

noncomputable def ptn_noiseOp (p ρ : ℝ) (f : ConfigSpace ι → ℝ) : ConfigSpace ι → ℝ :=
  fun ω => ∑ S : Finset ι, (ρ ^ S.card * ptn_coeff p f S) * ptn_pchar p S ω

Uses 3 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · \(p\)-biased Fourier coefficient · \(p\)-biased character

Used byKernel and Fourier noise operators agree · Fourier form of \(p\)-biased hypercontractivity on finite index types · Fourier form of \(p\)-biased hypercontractivity on \(\{0, 1\}^n\) · \(p\)-biased hypercontractivity for a discrete derivative

DefinitionOne-coordinate \(p\)-biased noise kernel#✓fully proved

The one-coordinate noise kernel: keep the bit with probability ρ, otherwise resample it from Bernoulli(p).

noncomputable def ptn_kbit (p ρ : ℝ) (x y : Bool) : ℝ :=
  ρ * (if x = y then 1 else 0) + (1 - ρ) * (if y then p else 1 - p)

Used by 6

Used by\(p\)-biased hypercontractivity on \(\{0, 1\}^n\) · Product noise kernel on the Boolean cube · Kernel and Fourier noise operators agree · Fourier form of \(p\)-biased hypercontractivity on finite index types · \(p\)-biased hypercontractivity for a discrete derivative · Tensorization step for \(p\)-biased hypercontractivity

DefinitionProduct noise kernel on the Boolean cube#✓fully proved

The product noise kernel on {0, 1}^ι.

noncomputable def ptn_kernel (p ρ : ℝ) (x y : ConfigSpace ι) : ℝ :=
  ∏ i : ι, ptn_kbit p ρ (x i) (y i)

Uses 2 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model · One-coordinate \(p\)-biased noise kernel

Used by\(p\)-biased hypercontractivity on \(\{0, 1\}^n\) · \(p\)-biased noise operator via its Markov kernel · Kernel and Fourier noise operators agree · Fourier form of \(p\)-biased hypercontractivity on finite index types · \(p\)-biased hypercontractivity for a discrete derivative · Tensorization step for \(p\)-biased hypercontractivity

Definition\(p\)-biased noise operator via its Markov kernel#✓fully proved

The p-biased noise operator T_ρ f (x) = ∑_y K_ρ(x, y) f y, defined by its Markov kernel.

noncomputable def ptn_kop (p ρ : ℝ) (f : ConfigSpace ι → ℝ) : ConfigSpace ι → ℝ :=
  fun x => ∑ y : ConfigSpace ι, ptn_kernel p ρ x y * f y

Uses 2 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model · Product noise kernel on the Boolean cube

Used by\(p\)-biased hypercontractivity on \(\{0, 1\}^n\) · Kernel and Fourier noise operators agree · Fourier form of \(p\)-biased hypercontractivity on finite index types · Fourier form of \(p\)-biased hypercontractivity on \(\{0, 1\}^n\) · \(p\)-biased hypercontractivity for a discrete derivative · Tensorization step for \(p\)-biased hypercontractivity

TheoremKernel and Fourier noise operators agree#✓fully proved

The kernel and Fourier definitions of the p-biased noise operator agree for 0 < p < 1.

theorem ptn_kop_eq_noiseOp {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1) (ρ : ℝ) (f : ConfigSpace ι → ℝ) :
    ptn_kop p ρ f = ptn_noiseOp p ρ f

Uses 11 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · \(p\)-biased noise operator via its Markov kernel · \(p\)-biased noise operator on the Fourier side

Proof uses\(p\)-biased Fourier coefficient · \(p\)-biased Fourier inversion · One-coordinate \(p\)-biased noise kernel · Product noise kernel on the Boolean cube · \(p\)-biased character · Normalized Bernoulli bit · Standard deviation of a Bernoulli bit · Zero-one value of a bit

Used byFourier form of \(p\)-biased hypercontractivity on finite index types · Fourier form of \(p\)-biased hypercontractivity on \(\{0, 1\}^n\) · \(p\)-biased hypercontractivity for a discrete derivative

TheoremTensorization step for \(p\)-biased hypercontractivity#✓fully proved

Induction step of the tensorization: hypercontractivity on {0, 1}^n implies it on {0, 1}^{n+1}.

theorem ptn_tensorStep {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)) (n : ℕ)
    (ih : ∀ g : (Fin n → Bool) → ℝ, ptn_qnorm p 2 (ptn_kop p ρ g) ≤ ptn_qnorm p q g)
    (f : (Fin (n + 1) → Bool) → ℝ) :
    ptn_qnorm p 2 (ptn_kop p ρ f) ≤ ptn_qnorm p q f

Uses 11 · Used by 1

Statement uses\(p\)-biased noise operator via its Markov kernel · \(L^q\) norm under the \(p\)-biased measure

Proof usesConfiguration space of a statistical-mechanics model · Product probability weight · Bernoulli product weight · Expectation under a product weight · Probability of a configuration under a product weight · p-biased two-point inequality · One-coordinate \(p\)-biased noise kernel · Product noise kernel on the Boolean cube · \(q\)-th moment under the \(p\)-biased measure

Used by\(p\)-biased hypercontractivity on \(\{0, 1\}^n\)

Theorem\(p\)-biased hypercontractivity on \(\{0, 1\}^n\)#✓fully proved

p-biased hypercontractivity on {0, 1}^n: ‖T_ρ f‖₂ ≤ ‖f‖_q for 0 < p < 1, 1 ≤ q ≤ 2 and ρ² = 4p(1-p)(q - 1). The noise rate is not optimal for p ≠ 1/2.

theorem ptn_hypercontractivity_fin {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))
    (n : ℕ) (f : (Fin n → Bool) → ℝ) :
    ptn_qnorm p 2 (ptn_kop p ρ f) ≤ ptn_qnorm p q f

Uses 10 · Used by 1

Statement uses\(p\)-biased noise operator via its Markov kernel · \(L^q\) norm under the \(p\)-biased measure

Proof usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Expectation under a product weight · Probability of a configuration under a product weight · One-coordinate \(p\)-biased noise kernel · Product noise kernel on the Boolean cube · \(q\)-th moment under the \(p\)-biased measure · Tensorization step for \(p\)-biased hypercontractivity

Used byFourier form of \(p\)-biased hypercontractivity on \(\{0, 1\}^n\)

TheoremFourier form of \(p\)-biased hypercontractivity on \(\{0, 1\}^n\)#✓fully proved

Fourier form of ptn_hypercontractivity_fin on {0, 1}^n.

theorem ptn_lowDegreeWeight_fin {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))
    (n : ℕ) (f : (Fin n → Bool) → ℝ) :
    (∑ S : Finset (Fin n), (ρ ^ S.card) ^ 2 * (ptn_coeff p f S) ^ 2)
      ≤ (ptn_qnorm p q f) ^ 2

Uses 14 · Used by 1

Statement uses\(p\)-biased Fourier coefficient · \(L^q\) norm under the \(p\)-biased measure

Proof usesConfiguration space of a statistical-mechanics model · Product probability weight · Bernoulli product weight · Expectation under a product weight · Probability of a configuration under a product weight · \(p\)-biased hypercontractivity on \(\{0, 1\}^n\) · \(p\)-biased noise operator via its Markov kernel · Kernel and Fourier noise operators agree · \(p\)-biased noise operator on the Fourier side · Orthonormality of the \(p\)-biased characters · \(p\)-biased character · \(q\)-th moment under the \(p\)-biased measure

Used byFourier form of \(p\)-biased hypercontractivity on finite index types

TheoremFourier form of \(p\)-biased hypercontractivity on finite index types#✓fully proved

p-biased hypercontractivity in Fourier form on any finite index type: ∑_S ρ^{2|S|} f̂(S)² ≤ ‖f‖_q² for ρ² = 4p(1-p)(q - 1).

theorem ptn_lowDegreeWeight {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))
    (f : ConfigSpace ι → ℝ) :
    (∑ S : Finset ι, (ρ ^ S.card) ^ 2 * (ptn_coeff p f S) ^ 2)
      ≤ (ptn_qnorm p q f) ^ 2

Uses 17 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · \(p\)-biased Fourier coefficient · \(L^q\) norm under the \(p\)-biased measure

Proof usesBernoulli product weight · Expectation under a product weight · Probability of a configuration under a product weight · Cube bijection induced by an index bijection · Reindexing a cube function along an index bijection · One-coordinate \(p\)-biased noise kernel · Product noise kernel on the Boolean cube · \(p\)-biased noise operator via its Markov kernel · Kernel and Fourier noise operators agree · Fourier form of \(p\)-biased hypercontractivity on \(\{0, 1\}^n\) · \(p\)-biased noise operator on the Fourier side · Orthonormality of the \(p\)-biased characters · \(p\)-biased character · \(q\)-th moment under the \(p\)-biased measure

Used by\(p\)-biased hypercontractivity for a discrete derivative

Theorem\(p\)-biased hypercontractivity for a discrete derivative#✓fully proved

p-biased hypercontractivity applied to the discrete derivative ∂ₑ 1_A.

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

Uses 24 · Used by 3

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

Proof usesProduct probability weight · Expectation under a product weight · Probability of a configuration under a product weight · Discrete derivative in a coordinate · \(p\)-biased Fourier inversion · One-coordinate \(p\)-biased noise kernel · Product noise kernel on the Boolean cube · \(p\)-biased noise operator via its Markov kernel · Kernel and Fourier noise operators agree · Fourier form of \(p\)-biased hypercontractivity on finite index types · \(p\)-biased noise operator on the Fourier side · Orthonormality of the \(p\)-biased characters · \(p\)-biased character · Normalized Bernoulli bit · \(L^q\) norm under the \(p\)-biased measure · \(q\)-th moment under the \(p\)-biased measure · Zero-one value of a bit · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Used byHypercontractive bound on the damped fiber weight · Hypercontractive bound on the damped influence · Summed per-coordinate \(p\)-biased hypercontractive bound

TheoremSummed per-coordinate \(p\)-biased hypercontractive bound#✓fully proved

ptn_perCoord_hc summed over all coordinates.

theorem ptn_summed_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) :
    (1 / (ptn_sigma p) ^ 2) * ∑ S : Finset ι, (S.card : ℝ) * ((ρ ^ (S.card - 1)) ^ 2
        * (ptn_coeff p (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2)
      ≤ ∑ e : ι, (OSSS.infl (OSSS.bernoulliWeight p)
          (fun ω => if φ ω then (1 : ℝ) else 0) e) ^ (2 / q)

Uses 6 · Used by 1

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

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

Used byCapped per-coordinate estimate under the \(p\)-biased measure

TheoremCapped per-coordinate estimate under the \(p\)-biased measure#✓fully proved

The capped per-coordinate estimate under μ_p: (1/(p(1-p))) ∑_S |S| ρ^{2(|S|-1)} f̂(S)² ≤ δ^{2/q - 1} ∑ₑ Infₑ, with δ = maxₑ Infₑ.

theorem ptn_capped_hc [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) :
    (1 / (ptn_sigma p) ^ 2) * ∑ S : Finset ι, (S.card : ℝ) * ((ρ ^ (S.card - 1)) ^ 2
        * (ptn_coeff p (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2)
      ≤ (maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)) ^ (2 / q - 1)
        * totalInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)

Uses 14 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Maximal influence under a product weight · \(p\)-biased Fourier coefficient · Standard deviation of a Bernoulli bit · 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 · Termwise cap \(x^\theta \le \delta^{\theta-1} x\) · Summed per-coordinate \(p\)-biased hypercontractive bound · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Used byCapped \(p\)-biased per-coordinate estimate in the variable \(u\) · Capped estimate in the hypercontractive range · Conditional \(p\)-biased KKL statement yields KKL with constant \(2\)

Definition\(p\)-biased KKL inequality conditional on the capped estimate#✓fully proved

The KKL inequality with constant 2 for every p ∈ (1/2, q) with p < 1, with the capped estimate ptn_capped_hc as a hypothesis.

def ptn_RhoOptimise (q : ℝ) : Prop :=
  ∀ p ∈ Set.Ioo (1 / 2 : ℝ) q, p < 1 → ∀ {E : Type} [Fintype E] [DecidableEq E] [Nonempty E]
    (φ : ConfigSpace E → Bool),
    (∀ ρ : ℝ, 0 ≤ ρ → ρ ≤ 1 → ∀ q' : ℝ, 1 ≤ q' → q' ≤ 2 → ρ ^ 2 = (q' - 1) * 4 * p * (1 - p) →
        (1 / (ptn_sigma p) ^ 2) * ∑ S : Finset E, (S.card : ℝ) * ((ρ ^ (S.card - 1)) ^ 2
            * (ptn_coeff p (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2)
          ≤ (maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)) ^ (2 / q' - 1)
            * totalInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)) →
      2 * OSSS.var (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)
          * Real.log (1 / maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0))
        ≤ totalInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)

Uses 7 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Variance under a product weight · Maximal influence under a product weight · \(p\)-biased Fourier coefficient · Standard deviation of a Bernoulli bit · Total influence under a product weight

Used byCapped estimate implies KKL with constant 2 on \((1/2, q)\) · Conditional \(p\)-biased KKL statement yields KKL with constant \(2\) · Conditional KKL gives KKL with constant 2 on \((1/2, q)\) for \(q \le 1\) · Sharp-threshold bound from the conditional KKL statement

TheoremConditional \(p\)-biased KKL statement yields KKL with constant \(2\)#✓fully proved

ptn_RhoOptimise q gives the KKL inequality with constant 2 at every p ∈ (1/2, q).

theorem ptn_kklHC_of_rhoOptimise {q : ℝ} (H : ptn_RhoOptimise q)
    {p : ℝ} (hp : p ∈ Set.Ioo (1 / 2 : ℝ) q) (hp1 : p < 1) :
    KKLHypercontractive p 2

Uses 4 · Used by 1

Statement usesKKL inequality with constant \(c\) for the \(p\)-biased measure · \(p\)-biased KKL inequality conditional on the capped estimate

Proof usesConfiguration space of a statistical-mechanics model · Capped per-coordinate estimate under the \(p\)-biased measure

Used byConditional KKL gives KKL with constant 2 on \((1/2, q)\) for \(q \le 1\)

TheoremConditional KKL gives KKL with constant 2 on \((1/2, q)\) for \(q \le 1\)#✓fully proved

ptn_RhoOptimise q implies kpb_PBiasedHC q.

theorem ptn_PBiasedHC_of_rhoOptimise {q : ℝ} (hq : q ≤ 1) (H : ptn_RhoOptimise q) :
    kpb_PBiasedHC q

Uses 3 · Used by 1

Statement usesKKL inequality with constant 2 on \((1/2, q)\) · \(p\)-biased KKL inequality conditional on the capped estimate

Proof usesConditional \(p\)-biased KKL statement yields KKL with constant \(2\)

Used bySharp-threshold bound from the conditional KKL statement

TheoremTrivial KKL inequality with constant \(0\)#✓fully proved

The KKL inequality with constant 0 holds trivially.

theorem ptn_rhoOptimise_c0 {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1)
    {E : Type} [Fintype E] [DecidableEq E] [Nonempty E] (φ : ConfigSpace E → Bool) :
    (0 : ℝ) * OSSS.var (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)
        * Real.log (1 / maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0))
      ≤ totalInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)

Uses 11

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Variance under a product weight · Maximal influence under a product weight · 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

TheoremSharp-threshold bound from the conditional KKL statement#✓fully proved

The sharp-threshold bound kpb_sharpThreshold under ptn_RhoOptimise q.

theorem ptn_sharpThreshold_of_rhoOptimise {q : ℝ} (hq1 : q ≤ 1) (H : ptn_RhoOptimise q)
    {E : Type} [Fintype E] [DecidableEq E] [Nonempty E]
    (A : Set (ConfigSpace E)) (hA : IsIncreasing A)
    {v₀ L : ℝ} (hq : (1 : ℝ) / 2 ≤ q) (hv0 : 0 ≤ v₀) (hL : 0 ≤ L)
    (hhalf : StatMech.prob (1 / 2) A = 1 / 2)
    (hvar : ∀ p ∈ interior (Set.Icc (1 / 2 : ℝ) q),
      v₀ ≤ StatMech.prob p A * (1 - StatMech.prob p A))
    (hLL' : ∀ p ∈ interior (Set.Icc (1 / 2 : ℝ) q),
      L ≤ StatMech.TwoDim.kklw_logMaxInfl p A) :
    1 / 2 + (2 * v₀ * L) * (q - 1 / 2) ≤ StatMech.prob q A

Uses 7

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · \(p\)-biased KKL inequality conditional on the capped estimate · Logarithm of the reciprocal maximal influence of an event · Bernoulli weight of an event

Proof usesSharp-threshold bound under the \(p\)-biased KKL hypothesis · Conditional KKL gives KKL with constant 2 on \((1/2, q)\) for \(q \le 1\)

31 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.