OSSS inequality for decision trees

DefinitionProbability of a configuration under a product weight#✓fully proved

The probability ∏ₑ ν e (ω e) of the configuration ω under the product weight ν.

noncomputable def weight (ν : E → Bool → ℝ) (ω : ConfigSpace E) : ℝ := ∏ e, ν e (ω e)

Uses 1 · Used by 49

Statement usesConfiguration space of a statistical-mechanics model

Used byDamped KKL inequality under the \(p\)-biased measure · Log-sum estimate for the fiber weights · Capped estimate with zero weights holds trivially · Capped estimate implies KKL with constant 2 on \((1/2, q)\) · Some truncation level makes the low-degree right side nonnegative · Sum of influence powers capped by the maximal influence · Bonami–Beckner applied to a discrete derivative · Capped log-sum estimate for damped influences · Log-sum inequality for influences against damped influences · Data-processing inequality for entropy under a two-point mixture · Sub-additivity (tensorization) of entropy · Maximal influence of a Boolean function is at most one · Capped estimate when the maximal influence is at least \(e^{-1}\) · Right side of the capped estimate is nonnegative · Low-range case implies the small-influence case · Capped estimate at \(p = 1/2\) for all \(u \in (0, 1)\) · Target-exponent capped estimate from a domination bound · Capped estimate at the endpoint \(u = 1\) · Squared \(p\)-biased and Walsh coefficients agree at \(p = 1/2\) · Pivotal-probability influence as the OSSS influence of an indicator · Event probability as the OSSS expectation of its indicator · OSSS Bernoulli weight equals the configuration weight · KKL inequality · KKL inequality with constant 0 holds trivially · Reflection of the KKL inequality from \(p\) to \(1 - p\) · Complement swaps the Bernoulli \(p\) and \(1 - p\) weights · Event influence is four times the canonical influence · Hypercontractive form of KKL with constant 0 holds trivially · Variance as Fourier weight off the empty set · Uniform variance agrees with the canonical Boolean variance · Root step of the OSSS induction · Subtree step of the OSSS induction · Expectation under a product weight · Bernoulli product weight computes product-measure integrals · Influence on an indicator is the pivotal probability · OSSS covariance inequality over all product weights · Poincaré inequality for Boolean functions under a product measure · Covariance form of the Poincaré inequality · Capped per-coordinate estimate under the \(p\)-biased measure · \(p\)-biased Fourier inversion · Expectations of product functions factor under product measure · \(p\)-biased hypercontractivity on \(\{0, 1\}^n\) · \(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 · Trivial KKL inequality with constant \(0\) · Tensorization step for \(p\)-biased hypercontractivity

DefinitionExpectation under a product weight#✓fully proved

The expectation ∑_ω weight ν ω * g ω of g under the product weight ν.

noncomputable def expect (ν : E → Bool → ℝ) (g : ConfigSpace E → ℝ) : ℝ :=
  ∑ ω, weight ν ω * g ω

Uses 2 · Used by 54

Statement usesConfiguration space of a statistical-mechanics model · Probability of a configuration under a product weight

Used byDamped KKL inequality under the \(p\)-biased measure · Log-sum estimate for the fiber weights · Capped estimate with zero weights holds trivially · Capped estimate implies KKL with constant 2 on \((1/2, q)\) · Some truncation level makes the low-degree right side nonnegative · Sum of influence powers capped by the maximal influence · Bonami–Beckner applied to a discrete derivative · Capped log-sum estimate for damped influences · Log-sum inequality for influences against damped influences · Data-processing inequality for entropy under a two-point mixture · Entropy of a function under a product weight · Sub-additivity (tensorization) of entropy · Maximal influence of a Boolean function is at most one · Capped estimate when the maximal influence is at least \(e^{-1}\) · Right side of the capped estimate is nonnegative · Low-range case implies the small-influence case · Capped estimate at \(p = 1/2\) for all \(u \in (0, 1)\) · Target-exponent capped estimate from a domination bound · Capped estimate at the endpoint \(u = 1\) · Squared \(p\)-biased and Walsh coefficients agree at \(p = 1/2\) · Pivotal-probability influence as the OSSS influence of an indicator · Event probability as the OSSS expectation of its indicator · Variance of an event indicator is \(P(A)(1 - P(A))\) · KKL inequality · KKL inequality with constant 0 holds trivially · Reflection of the KKL inequality from \(p\) to \(1 - p\) · Event influence is four times the canonical influence · Hypercontractive form of KKL with constant 0 holds trivially · Variance as Fourier weight off the empty set · Uniform variance agrees with the canonical Boolean variance · Root step of the OSSS induction · Subtree step of the OSSS induction · Covariance under a product weight · Bernoulli product weight computes product-measure integrals · Influence of a coordinate · Influence on an indicator is the pivotal probability · OSSS covariance inequality over all product weights · Poincaré inequality for Boolean functions under a product measure · Covariance form of the Poincaré inequality · Revealment of a variable by a decision tree · Capped per-coordinate estimate under the \(p\)-biased measure · \(p\)-biased Fourier coefficient · Expectations of product functions factor under product measure · \(p\)-biased hypercontractivity on \(\{0, 1\}^n\) · \(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\) · Orthonormality of the \(p\)-biased characters · Parseval's identity under the \(p\)-biased measure · \(p\)-biased hypercontractivity for a discrete derivative · \(q\)-th moment under the \(p\)-biased measure · Trivial KKL inequality with constant \(0\) · Tensorization step for \(p\)-biased hypercontractivity · \(p\)-biased variance as Fourier weight off the empty set

StructureProduct probability weight#✓fully proved

ν is a product probability weight: each ν e is a probability vector on Bool.

structure IsProbWeight (ν : E → Bool → ℝ) : Prop where
  nonneg : ∀ e b, 0 ≤ ν e b
  normalized : ∀ e, ν e false + ν e true = 1

Used by 35

Used byDamped KKL inequality under the \(p\)-biased measure · Log-sum estimate for the fiber weights · Capped estimate with zero weights holds trivially · Capped estimate implies KKL with constant 2 on \((1/2, q)\) · Some truncation level makes the low-degree right side nonnegative · Sum of influence powers capped by the maximal influence · Bonami–Beckner applied to a discrete derivative · Capped log-sum estimate for damped influences · Log-sum inequality for influences against damped influences · Data-processing inequality for entropy under a two-point mixture · Sub-additivity (tensorization) of entropy · Maximal influence of a Boolean function is at most one · Capped estimate when the maximal influence is at least \(e^{-1}\) · Right side of the capped estimate is nonnegative · Low-range case implies the small-influence case · Capped estimate at \(p = 1/2\) for all \(u \in (0, 1)\) · Target-exponent capped estimate from a domination bound · Capped estimate at the endpoint \(u = 1\) · KKL inequality · KKL inequality with constant 0 holds trivially · Hypercontractive form of KKL with constant 0 holds trivially · Root step of the OSSS induction · Subtree step of the OSSS induction · OSSS inequality · OSSS inequality for the Bernoulli product measure · OSSS covariance inequality over all product weights · OSSS inequality · Poincaré inequality for Boolean functions under a product measure · Poincaré inequality for the Bernoulli product measure · Covariance form of the Poincaré inequality · Capped per-coordinate estimate under the \(p\)-biased measure · Fourier form of \(p\)-biased hypercontractivity on \(\{0, 1\}^n\) · \(p\)-biased hypercontractivity for a discrete derivative · Trivial KKL inequality with constant \(0\) · Tensorization step for \(p\)-biased hypercontractivity

DefinitionPoint-mass weight on the Booleans#✓fully proved

The point mass at b, as a weight on Bool. Replacing ν e by pt b conditions on ω e = b.

def pt (b : Bool) : Bool → ℝ := fun c => if c = b then 1 else 0

Used by 3

Used byRoot step of the OSSS induction · Subtree step of the OSSS induction · OSSS covariance inequality over all product weights

DefinitionCovariance under a product weight#✓fully proved

The covariance 𝔼[f g] - 𝔼[f] 𝔼[g] under the product weight ν.

noncomputable def cov (ν : E → Bool → ℝ) (f g : ConfigSpace E → ℝ) : ℝ :=
  expect ν (fun ω => f ω * g ω) - expect ν f * expect ν g

Uses 2 · Used by 12

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

Used byVariance of an event indicator is \(P(A)(1 - P(A))\) · Reflection of the KKL inequality from \(p\) to \(1 - p\) · Variance as Fourier weight off the empty set · Uniform variance agrees with the canonical Boolean variance · Root step of the OSSS induction · Subtree step of the OSSS induction · OSSS inequality · OSSS inequality for the Bernoulli product measure · OSSS covariance inequality over all product weights · Covariance form of the Poincaré inequality · Variance under a product weight · \(p\)-biased variance as Fourier weight off the empty set

DefinitionVariance under a product weight#✓fully proved

The variance of g under the product weight ν.

noncomputable def var (ν : E → Bool → ℝ) (g : ConfigSpace E → ℝ) : ℝ := cov ν g g

Uses 2 · Used by 21

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

Used byKKL inequality with constant \(2\) at \(p = 1/2\) · Damped variance equals the variance at \(p = 1/2\) · Log-sum estimate for the fiber weights · Capped estimate implies KKL with constant 2 on \((1/2, q)\) · Variance decomposition by maximal element · KKL inequality with constant 2 at \(p\) implies its event form · Variance of an event indicator is \(P(A)(1 - P(A))\) · KKL inequality with constant 0 holds trivially · Kahn–Kalai–Linial inequality · Kahn–Kalai–Linial inequality · KKL inequality with constant \(c\) for the \(p\)-biased measure · Reflection of the KKL inequality from \(p\) to \(1 - p\) · Hypercontractive form of KKL implies the KKL inequality at \(p = 1/2\) · Variance as Fourier weight off the empty set · Uniform variance agrees with the canonical Boolean variance · OSSS inequality · Poincaré inequality for Boolean functions under a product measure · Poincaré inequality for the Bernoulli product measure · \(p\)-biased KKL inequality conditional on the capped estimate · Trivial KKL inequality with constant \(0\) · \(p\)-biased variance as Fourier weight off the empty set

DefinitionInfluence of a coordinate#✓fully proved

The influence of coordinate e on g: 𝔼 |g(ω^{e ↦ 1}) - g(ω^{e ↦ 0})|. For the indicator of an event this is the probability that e is pivotal (infl_indicator_eq_pivotal).

See also BooleanCube.boolInfluence, the uniform-measure influence 𝔼 ((f x - f x^{⊕i}) / 2)²; for 0/1-valued functions on the uniform cube the two differ by the factor 4.

noncomputable def infl (ν : E → Bool → ℝ) (g : ConfigSpace E → ℝ) (e : E) : ℝ :=
  expect ν (fun ω => |g (setOpen e ω) - g (setClosed e ω)|)

Uses 4 · Used by 49

Statement usesConfiguration space of a statistical-mechanics model · Expectation under a product weight · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Used byDamped KKL inequality under the \(p\)-biased measure · Hypercontractive bound on the damped fiber weight · Log-sum estimate for the fiber weights · Capped estimate with zero weights holds trivially · Capped estimate implies KKL with constant 2 on \((1/2, q)\) · Some truncation level makes the low-degree right side nonnegative · Sum of influence powers capped by the maximal influence · Capped per-coordinate hypercontractive estimate · Bonami–Beckner applied to a discrete derivative · Summed per-coordinate Bonami–Beckner bound · Hypercontractive 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 · Maximal influence of a Boolean function is at most one · Capped estimate when the maximal influence is at least \(e^{-1}\) · Right side of the capped estimate is nonnegative · Low-range case implies the small-influence case · Capped estimate at \(p = 1/2\) for all \(u \in (0, 1)\) · Target-exponent capped estimate from a domination bound · Capped estimate at the endpoint \(u = 1\) · KKL inequality with constant 2 at \(p\) implies its event form · Pivotal-probability influence as the OSSS influence of an indicator · KKL inequality · KKL inequality with constant 0 holds trivially · Kahn–Kalai–Linial inequality · Maximal influence under a product weight · Total influence under a product weight · Reflection of the KKL inequality from \(p\) to \(1 - p\) · Event influence is four times the canonical influence · Influence of a coordinate as Fourier weight · Hypercontractive form of KKL with constant 0 holds trivially · Total influence as Fourier weight · Root step of the OSSS induction · Influence on an indicator is the pivotal probability · OSSS inequality · OSSS inequality for the Bernoulli product measure · OSSS covariance inequality over all product weights · OSSS inequality · Poincaré inequality for Boolean functions under a product measure · Poincaré inequality for the Bernoulli product measure · Covariance form of the Poincaré inequality · Capped per-coordinate estimate under the \(p\)-biased measure · \(p\)-biased influence of a coordinate as Fourier weight · \(p\)-biased hypercontractivity for a discrete derivative · Trivial KKL inequality with constant \(0\) · Summed per-coordinate \(p\)-biased hypercontractive bound · \(p\)-biased total influence as Fourier weight

DefinitionConditional expectation given the other coordinates#✓fully proved

The conditional expectation of g given all coordinates except e.

noncomputable def condMean (ν : E → Bool → ℝ) (e : E) (g : ConfigSpace E → ℝ) :
    ConfigSpace E → ℝ :=
  fun ω => ν e true * g (setOpen e ω) + ν e false * g (setClosed e ω)

Uses 3 · Used by 4

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

Used byConditional entropy in one coordinate · Sub-additivity (tensorization) of entropy · Root step of the OSSS induction · OSSS covariance inequality over all product weights

InductiveBinary decision tree#✓fully proved

A binary decision tree on the variables E: a leaf outputs a Boolean value, and a node queries a variable and continues in the first subtree if it is true and in the second otherwise.

inductive DecisionTree (E : Type*) where
  | leaf : Bool → DecisionTree E
  | node : E → DecisionTree E → DecisionTree E → DecisionTree E

Used by 13

Used bySubtree step of the OSSS induction · Boolean function computed by a decision tree · Real-valued function computed by a decision tree · Decision tree querying a list of variables · Decision tree querying every variable · OSSS inequality · OSSS inequality for the Bernoulli product measure · OSSS covariance inequality over all product weights · OSSS inequality · Poincaré inequality for Boolean functions under a product measure · Covariance form of the Poincaré inequality · Variables queried by a decision tree on an input · Revealment of a variable by a decision tree

DefinitionBoolean function computed by a decision tree#✓fully proved

The Boolean function computed by the decision tree.

def eval : DecisionTree E → ConfigSpace E → Bool
  | leaf b, _ => b
  | node e t f, ω => if ω e then eval t ω else eval f ω

Uses 2 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Binary decision tree

Used bySubtree step of the OSSS induction · Real-valued function computed by a decision tree · OSSS covariance inequality over all product weights · Poincaré inequality for Boolean functions under a product measure · Covariance form of the Poincaré inequality

DefinitionVariables queried by a decision tree on an input#✓fully proved

The set of variables the decision tree queries on input ω.

def queried : DecisionTree E → ConfigSpace E → Finset E
  | leaf _, _ => ∅
  | node e t f, ω => insert e (if ω e then queried t ω else queried f ω)

Uses 2 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Binary decision tree

Used byOSSS covariance inequality over all product weights · Poincaré inequality for Boolean functions under a product measure · Covariance form of the Poincaré inequality · Revealment of a variable by a decision tree

DefinitionReal-valued function computed by a decision tree#✓fully proved

The function computed by the decision tree, as a 0/1-valued real function.

noncomputable def evalR (T : DecisionTree E) (ω : ConfigSpace E) : ℝ :=
  if T.eval ω then 1 else 0

Uses 3 · Used by 7

Statement usesConfiguration space of a statistical-mechanics model · Binary decision tree · Boolean function computed by a decision tree

Used bySubtree step of the OSSS induction · OSSS inequality · OSSS inequality for the Bernoulli product measure · OSSS covariance inequality over all product weights · OSSS inequality · Poincaré inequality for Boolean functions under a product measure · Covariance form of the Poincaré inequality

DefinitionRevealment of a variable by a decision tree#✓fully proved

The revealment δₑ(T): the probability that the decision tree T queries the variable e.

noncomputable def reveal (ν : E → Bool → ℝ) (T : DecisionTree E) (e : E) : ℝ :=
  expect ν (fun ω => if e ∈ T.queried ω then (1 : ℝ) else 0)

Uses 4 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model · Binary decision tree · Variables queried by a decision tree on an input · Expectation under a product weight

Used byOSSS inequality · OSSS inequality for the Bernoulli product measure · OSSS covariance inequality over all product weights · OSSS inequality · Poincaré inequality for Boolean functions under a product measure · Covariance form of the Poincaré inequality

DefinitionConfiguration with one coordinate flipped#✓fully proved

The configuration ω with coordinate e flipped.

See also BooleanCube.flipCoord, the same operation on Fin n → Bool.

def flipAt (e : E) (ω : ConfigSpace E) : ConfigSpace E := Function.update ω e (!(ω e))

Uses 1 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model

Used byRoot step of the OSSS induction · Subtree step of the OSSS induction · OSSS covariance inequality over all product weights

LemmaRoot step of the OSSS induction#✓fully proved

Root step of the OSSS induction: the covariance of a function whose discrete derivative in e is bounded by 1 with the martingale increment g - 𝔼[g | ω_{≠e}] is at most Infₑ(g).

lemma claimA {ν : E → Bool → ℝ} (hν : IsProbWeight ν) (e : E) (F g : ConfigSpace E → ℝ)
    (hF : ∀ ω, |F (setOpen e ω) - F (setClosed e ω)| ≤ 1) :
    cov ν F (fun ω => g ω - condMean ν e g ω) ≤ infl ν g e

Uses 11 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Product probability weight · Conditional expectation given the other coordinates · Covariance under a product weight · Influence of a coordinate · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Proof usesExpectation under a product weight · Configuration with one coordinate flipped · Point-mass weight on the Booleans · Probability of a configuration under a product weight

Used byOSSS covariance inequality over all product weights

LemmaSubtree step of the OSSS induction#✓fully proved

Subtree step of the OSSS induction: for G independent of the root variable e, the covariance with a tree rooted at e splits into the covariances with the two subtrees under the conditioned weights.

lemma claimB {ν : E → Bool → ℝ} (hν : IsProbWeight ν) (e : E) (t f : DecisionTree E)
    (G : ConfigSpace E → ℝ)
    (hG : ∀ ω, G (flipAt e ω) = G ω) :
    cov ν (DecisionTree.node e t f).evalR G
      = ν e true * cov (Function.update ν e (pt true)) t.evalR G
      + ν e false * cov (Function.update ν e (pt false)) f.evalR G

Uses 10 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Binary decision tree · Real-valued function computed by a decision tree · Product probability weight · Covariance under a product weight · Configuration with one coordinate flipped · Point-mass weight on the Booleans

Proof usesBoolean function computed by a decision tree · Expectation under a product weight · Probability of a configuration under a product weight

Used byOSSS covariance inequality over all product weights

TheoremOSSS covariance inequality over all product weights#✓fully proved

The OSSS covariance inequality, stated for all product weights at once so that it can be proved by induction on the decision tree. Use osss for the usual argument order.

theorem osss_cov (T : DecisionTree E) :
    ∀ ν, IsProbWeight ν → ∀ g : ConfigSpace E → ℝ,
      cov ν T.evalR g ≤ ∑ i, reveal ν T i * infl ν g i

Uses 18 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Binary decision tree · Real-valued function computed by a decision tree · Product probability weight · Covariance under a product weight · Influence of a coordinate · Revealment of a variable by a decision tree

Proof usesBoolean function computed by a decision tree · Variables queried by a decision tree on an input · Root step of the OSSS induction · Subtree step of the OSSS induction · Conditional expectation given the other coordinates · Expectation under a product weight · Configuration with one coordinate flipped · Point-mass weight on the Booleans · Probability of a configuration under a product weight · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Used byOSSS inequality · OSSS inequality for the Bernoulli product measure · OSSS inequality

TheoremOSSS inequality#✓fully proved

OSSS inequality (O'Donnell, Saks, Schramm, Servedio, Every decision tree has an influential variable, FOCS 2005): if the decision tree T computes f, then Var(f) ≤ ∑ᵢ δᵢ(T) Infᵢ(f) under every product probability measure.

theorem osss_var {ν : E → Bool → ℝ} (hν : IsProbWeight ν) (T : DecisionTree E) :
    var ν T.evalR ≤ ∑ i, reveal ν T i * infl ν T.evalR i

Uses 7 · Used by 1

Statement usesBinary decision tree · Real-valued function computed by a decision tree · Product probability weight · Influence of a coordinate · Revealment of a variable by a decision tree · Variance under a product weight

Proof usesOSSS covariance inequality over all product weights

Used byPoincaré inequality for Boolean functions under a product measure

TheoremOSSS inequality#✓fully proved

OSSS inequality, covariance form (O'Donnell, Saks, Schramm, Servedio, Every decision tree has an influential variable, FOCS 2005; in this form Duminil-Copin, Raoufi, Tassion, Ann. of Math. 2019): if the decision tree T computes the Boolean function f, then for every real function g and every product probability measure, Cov(f, g) ≤ ∑ᵢ δᵢ(T) Infᵢ(g), where Infᵢ(g) = 𝔼 |g(ω^{i ↦ 1}) - g(ω^{i ↦ 0})|.

This is osss_cov with the weight and its hypothesis as leading arguments.

theorem osss {ν : E → Bool → ℝ} (hν : IsProbWeight ν) (T : DecisionTree E) (g : ConfigSpace E → ℝ) :
    cov ν T.evalR g ≤ ∑ i, reveal ν T i * infl ν g i

Uses 8 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Binary decision tree · Real-valued function computed by a decision tree · Product probability weight · Covariance under a product weight · Influence of a coordinate · Revealment of a variable by a decision tree

Proof usesOSSS covariance inequality over all product weights

Used byCovariance form of the Poincaré inequality

DefinitionBernoulli product weight#✓fully proved

The Bernoulli(p) product weight: every coordinate is true with probability p.

noncomputable def bernoulliWeight (p : ℝ) : E → Bool → ℝ :=
  fun _ b => if b then p else 1 - p

Used by 95

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\) · Hypercontractive bound on the damped fiber weight · 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 · Some truncation level makes the low-degree right side nonnegative · Capped estimate from its low-degree part · Sum of influence powers capped by the maximal influence · Capped per-coordinate hypercontractive estimate · Bonami–Beckner applied to a discrete derivative · Fourier-form KKL at \(p = 1/2\) conditional on the capped estimate · Conditional Fourier-form KKL holds trivially with constant zero · Summed per-coordinate Bonami–Beckner bound · Fourier-form KKL inequality given the indicator Bonami–Beckner bound · Indicator-bound form of KKL with constant 0 holds trivially · Hypercontractive 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 · Conditional entropy in one coordinate · Sub-additivity (tensorization) of entropy · Maximal influence of a Boolean function is at most one · 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'\) · Right side of the capped estimate is nonnegative · 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\) · Open-interval case implies the full capped estimate on \((1/2, q)\) · Open-interval residual case of the capped estimate · Fourier-form KKL inequality given the measure–influence bound · Measure–influence form of KKL with constant 0 holds trivially · Squared \(p\)-biased and Walsh coefficients agree at \(p = 1/2\) · Total influence at \(p = 1/2\) via \(p\)-biased Fourier coefficients · KKL inequality with constant 2 at \(p\) implies its event form · Pivotal-probability influence as the OSSS influence of an indicator · Logarithm of the reciprocal maximal influence of an event · Event probability as the OSSS expectation of its indicator · Variance of an event indicator is \(P(A)(1 - P(A))\) · OSSS Bernoulli weight equals the configuration weight · Capped estimate rewritten in the variable \(u = 1 - \rho^2\) · KKL inequality · KKL inequality with constant 0 holds trivially · Kahn–Kalai–Linial inequality · Kahn–Kalai–Linial inequality · KKL inequality with constant \(c\) for the \(p\)-biased measure · Reflection of the KKL inequality from \(p\) to \(1 - p\) · Complement swaps the Bernoulli \(p\) and \(1 - p\) weights · Event influence is four times the canonical influence · Influence of a coordinate as Fourier weight · Hypercontractive form of KKL implies the KKL inequality at \(p = 1/2\) · Fourier-form KKL inequality given the hypercontractive bound · Hypercontractive form of KKL with constant 0 holds trivially · Total influence as Fourier weight · Variance as Fourier weight off the empty set · Uniform variance agrees with the canonical Boolean variance · Bernoulli product weight computes product-measure integrals · OSSS inequality for the Bernoulli product measure · Poincaré inequality for the Bernoulli product measure · Capped per-coordinate estimate under the \(p\)-biased measure · \(p\)-biased Fourier coefficient · \(p\)-biased Fourier inversion · Expectations of product functions factor under product measure · \(p\)-biased hypercontractivity on \(\{0, 1\}^n\) · \(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\) · Orthonormality of the \(p\)-biased characters · Parseval's identity under the \(p\)-biased measure · \(p\)-biased hypercontractivity for a discrete derivative · \(q\)-th moment under the \(p\)-biased measure · \(p\)-biased KKL inequality conditional on the capped estimate · Trivial KKL inequality with constant \(0\) · Summed per-coordinate \(p\)-biased hypercontractive bound · Tensorization step for \(p\)-biased hypercontractivity · \(p\)-biased total influence as Fourier weight · \(p\)-biased variance as Fourier weight off the empty set

TheoremOSSS inequality for the Bernoulli product measure#✓fully proved

The OSSS inequality for the Bernoulli(p) product measure.

theorem osss_bernoulli {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1)
    (T : DecisionTree E) (g : ConfigSpace E → ℝ) :
    cov (bernoulliWeight p) T.evalR g
      ≤ ∑ i, reveal (bernoulliWeight p) T i * infl (bernoulliWeight p) g i

Uses 9

Statement usesConfiguration space of a statistical-mechanics model · Binary decision tree · Real-valued function computed by a decision tree · Bernoulli product weight · Covariance under a product weight · Influence of a coordinate · Revealment of a variable by a decision tree

Proof usesProduct probability weight · OSSS covariance inequality over all product weights

TheoremInfluence on an indicator is the pivotal probability#✓fully proved

The influence of e on the indicator of A is the probability that e is pivotal for A.

theorem infl_indicator_eq_pivotal (ν : E → Bool → ℝ) (A : Set (ConfigSpace E)) (e : E) :
    infl ν (A.indicator (fun _ => (1 : ℝ))) e
      = expect ν ({ω | IsPivotal e A ω}.indicator (fun _ => (1 : ℝ)))

Uses 7 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Pivotal coordinate for an event · Expectation under a product weight · Influence of a coordinate

Proof usesProbability of a configuration under a product weight · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Used byPivotal-probability influence as the OSSS influence of an indicator

TheoremBernoulli product weight computes product-measure integrals#✓fully proved

The Bernoulli(p) product weight computes integrals against StatMech.bernoulliProductMeasure, the corresponding product probability measure.

theorem expect_bernoulliWeight_eq_integral (p : NNReal) (hp : p ≤ 1) (g : ConfigSpace E → ℝ) :
    expect (bernoulliWeight (p : ℝ)) g = ∫ ω, g ω ∂(bernoulliProductMeasure p hp)

Uses 7

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

Proof usesProbability of a configuration under a product weight · Bernoulli distribution on the Booleans · Mass of a configuration under a finite Bernoulli product measure, real form

DefinitionDecision tree querying a list of variables#✓fully proved

The decision tree that queries the variables of l in order and then outputs the value of φ at the configuration that agrees with the answers on l and is false elsewhere. It computes φ when φ depends only on the variables in l (eval_fullTree).

def fullTree (φ : ConfigSpace E → Bool) : List E → DecisionTree E
  | [] => .leaf (φ (fun _ => false))
  | (e :: l) =>
      .node e (fullTree (fun ω => φ (setOpen e ω)) l)
              (fullTree (fun ω => φ (setClosed e ω)) l)

Uses 4 · Used by 3

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

Used byDecision tree querying every variable · Poincaré inequality for Boolean functions under a product measure · Covariance form of the Poincaré inequality

DefinitionFunction depending only on listed coordinates#✓fully proved

φ depends only on the coordinates in the list l.

def InsensOutside (φ : ConfigSpace E → Bool) (l : List E) : Prop :=
  ∀ ω ω', (∀ e ∈ l, ω e = ω' e) → φ ω = φ ω'

Uses 1 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model

Used byPoincaré inequality for Boolean functions under a product measure · Covariance form of the Poincaré inequality

DefinitionDecision tree querying every variable#✓fully proved

The decision tree that queries every variable and then outputs the value of φ; it computes φ and has revealment 1 at every variable.

noncomputable def fullTreeUniv (φ : ConfigSpace E → Bool) : DecisionTree E :=
  fullTree φ (Finset.univ.toList)

Uses 3 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Binary decision tree · Decision tree querying a list of variables

Used byPoincaré inequality for Boolean functions under a product measure · Covariance form of the Poincaré inequality

TheoremPoincaré inequality for Boolean functions under a product measure#✓fully proved

Poincaré inequality for Boolean functions under a product measure: Var(1_A) ≤ ∑ₑ Infₑ(1_A), where Infₑ(1_A) is the probability that e is pivotal. This is the OSSS inequality for the full decision tree; it is weaker than the Efron–Stein inequality Var(f) ≤ ∑ₑ pₑ(1 - pₑ) 𝔼[(∂ₑ f)²] by the factor pₑ(1 - pₑ) ≤ 1/4.

theorem poincare {ν : E → Bool → ℝ} (hν : IsProbWeight ν) (φ : ConfigSpace E → Bool) :
    var ν (fun ω => if φ ω then (1 : ℝ) else 0)
      ≤ ∑ e, infl ν (fun ω => if φ ω then (1 : ℝ) else 0) e

Uses 17 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Product probability weight · Influence of a coordinate · Variance under a product weight

Proof usesBinary decision tree · Boolean function computed by a decision tree · Real-valued function computed by a decision tree · Variables queried by a decision tree on an input · Function depending only on listed coordinates · Decision tree querying a list of variables · Decision tree querying every variable · Expectation under a product weight · OSSS inequality · Revealment of a variable by a decision tree · Probability of a configuration under a product weight · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Used byPoincaré inequality for the Bernoulli product measure

TheoremCovariance form of the Poincaré inequality#✓fully proved

Covariance form of poincare: Cov(1_A, g) ≤ ∑ₑ Infₑ(g) for every real function g.

theorem poincare_cov {ν : E → Bool → ℝ} (hν : IsProbWeight ν) (φ : ConfigSpace E → Bool)
    (g : ConfigSpace E → ℝ) :
    cov ν (fun ω => if φ ω then (1 : ℝ) else 0) g ≤ ∑ e, infl ν g e

Uses 17

Statement usesConfiguration space of a statistical-mechanics model · Product probability weight · Covariance under a product weight · Influence of a coordinate

Proof usesBinary decision tree · Boolean function computed by a decision tree · Real-valued function computed by a decision tree · Variables queried by a decision tree on an input · Function depending only on listed coordinates · Decision tree querying a list of variables · Decision tree querying every variable · Expectation under a product weight · OSSS inequality · Revealment of a variable by a decision tree · Probability of a configuration under a product weight · Closing a coordinate of a configuration · Opening a coordinate of a configuration

TheoremPoincaré inequality for the Bernoulli product measure#✓fully proved

poincare for the Bernoulli(p) product measure.

theorem poincare_bernoulli {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (φ : ConfigSpace E → Bool) :
    var (bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)
      ≤ ∑ e, infl (bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0) e

Uses 6

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Influence of a coordinate · Variance under a product weight

Proof usesProduct probability weight · Poincaré inequality for Boolean functions under a product measure

29 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.