Russo's formula and pivotal coordinates

DefinitionOpening a coordinate of a configuration#✓fully proved

setOpen e ω is ω with coordinate e set to true (open).

def setOpen (e : E) (ω : ConfigSpace E) : ConfigSpace E := Function.update ω e true

Uses 1 · Used by 61

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 · Discrete derivative in a coordinate · Bonami–Beckner applied to a discrete derivative · 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}\) · 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 · 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 · Root step of the OSSS induction · Conditional expectation given the other coordinates · Decision tree querying a list of variables · 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 · 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\) · Pivotal coordinate for an event · Symmetric form of pivotality · Pivotality depends only on the other coordinates · Pivotal coordinates of an increasing event · Closing a coordinate preserves its pivotality · Opening a coordinate preserves its pivotality · Contribution of one coordinate to Russo's formula · Russo's formula on a single fiber · Closed configuration lies below the opened one · Opening a coordinate depends only on the other coordinates · Opening a coordinate of a split configuration · Aizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Duminil-Copin–Tassion differential inequality · Mean-field differential inequality for inhomogeneous percolation · Edge density lies between \(p/(p+q(1-p))\) and \(p\) for \(q \ge 1\) · Cluster count plus open-edge count is monotone · Per-box uniqueness of the random-cluster measures off a countable set · Toggle-invariant coordinates are open with probability one half · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Conditional probability that an edge is open given the rest · Finite-energy property · Opening an edge lowers the cluster count by at most one · Opening an edge does not increase the cluster count · Toggling a non-edge leaves the open subgraph unchanged

DefinitionClosing a coordinate of a configuration#✓fully proved

setClosed e ω is ω with coordinate e set to false (closed).

def setClosed (e : E) (ω : ConfigSpace E) : ConfigSpace E := Function.update ω e false

Uses 1 · Used by 61

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 · Discrete derivative in a coordinate · Bonami–Beckner applied to a discrete derivative · 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}\) · 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 · 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 · Root step of the OSSS induction · Conditional expectation given the other coordinates · Decision tree querying a list of variables · 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 · 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\) · Pivotal coordinate for an event · Symmetric form of pivotality · Pivotality depends only on the other coordinates · Pivotal coordinates of an increasing event · Closing a coordinate preserves its pivotality · Opening a coordinate preserves its pivotality · Contribution of one coordinate to Russo's formula · Russo's formula on a single fiber · Closing a coordinate depends only on the other coordinates · Closed configuration lies below the opened one · Closing a coordinate of a split configuration · Aizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Duminil-Copin–Tassion differential inequality · Mean-field differential inequality for inhomogeneous percolation · Edge density lies between \(p/(p+q(1-p))\) and \(p\) for \(q \ge 1\) · Cluster count plus open-edge count is monotone · Per-box uniqueness of the random-cluster measures off a countable set · Toggle-invariant coordinates are open with probability one half · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Conditional probability that an edge is open given the rest · Finite-energy property · Opening an edge lowers the cluster count by at most one · Opening an edge does not increase the cluster count · Toggling a non-edge leaves the open subgraph unchanged

LemmaClosed configuration lies below the opened one#✓fully proved

Closing a coordinate gives a smaller configuration than opening it.

lemma setClosed_le_setOpen (e : E) (ω : ConfigSpace E) :
    setClosed e ω ≤ setOpen e ω

Uses 3 · Used by 6

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

Used byPivotal coordinates of an increasing event · Russo's formula on a single fiber · Aizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Opening an edge lowers the cluster count by at most one · Opening an edge does not increase the cluster count

LemmaOpening a coordinate depends only on the other coordinates#✓fully proved

setOpen e ω depends only on the values of ω off e.

lemma setOpen_congr {e : E} {ω ω' : ConfigSpace E}
    (h : ∀ e', e' ≠ e → ω e' = ω' e') : setOpen e ω = setOpen e ω'

Uses 2 · Used by 1

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

Used byPivotality depends only on the other coordinates

LemmaClosing a coordinate depends only on the other coordinates#✓fully proved

setClosed e ω depends only on the values of ω off e.

lemma setClosed_congr {e : E} {ω ω' : ConfigSpace E}
    (h : ∀ e', e' ≠ e → ω e' = ω' e') : setClosed e ω = setClosed e ω'

Uses 2 · Used by 1

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

Used byPivotality depends only on the other coordinates

DefinitionPivotal coordinate for an event#✓fully proved

The coordinate e is pivotal for the event A at ω if exactly one of setOpen e ω and setClosed e ω lies in A. The condition does not depend on ω e.

def IsPivotal (e : E) (A : Set (ConfigSpace E)) (ω : ConfigSpace E) : Prop :=
  (setOpen e ω ∈ A) ≠ (setClosed e ω ∈ A)

Uses 3 · Used by 19

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

Used byPivotal-probability influence as the OSSS influence of an indicator · Influence on an indicator is the pivotal probability · Symmetric form of pivotality · Pivotality depends only on the other coordinates · Pivotal coordinates of an increasing event · Closing a coordinate preserves its pivotality · Opening a coordinate preserves its pivotality · Weight of the event that a coordinate is pivotal · Nonnegativity of the pivotal weight · Contribution of one coordinate to Russo's formula · Russo's formula on a single fiber · Aizenman–Barsky inequality on a finite graph · Configurations with an edge closed and pivotal · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Pivotal probability of an edge · Duminil-Copin–Tassion differential inequality · Mean-field differential inequality for inhomogeneous percolation · Event that an edge is closed and pivotal · Pivotal edge event

LemmaSymmetric form of pivotality#✓fully proved

Pivotality with the two sides swapped.

lemma isPivotal_comm (e : E) (A : Set (ConfigSpace E)) (ω : ConfigSpace E) :
    IsPivotal e A ω ↔ (setClosed e ω ∈ A) ≠ (setOpen e ω ∈ A)

Uses 4

Statement usesConfiguration space of a statistical-mechanics model · Pivotal coordinate for an event · Closing a coordinate of a configuration · Opening a coordinate of a configuration

LemmaPivotality depends only on the other coordinates#✓fully proved

Pivotality of e depends only on the values of ω off e.

lemma isPivotal_congr {e : E} {A : Set (ConfigSpace E)} {ω ω' : ConfigSpace E}
    (h : ∀ e', e' ≠ e → ω e' = ω' e') : IsPivotal e A ω ↔ IsPivotal e A ω'

Uses 6 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Pivotal coordinate for an event

Proof usesClosing a coordinate of a configuration · Closing a coordinate depends only on the other coordinates · Opening a coordinate of a configuration · Opening a coordinate depends only on the other coordinates

Used byRusso's formula on a single fiber · Aizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Duminil-Copin–Tassion differential inequality · Mean-field differential inequality for inhomogeneous percolation

LemmaOpening a coordinate preserves its pivotality#✓fully proved

Opening e does not change whether e is pivotal.

@[simp] lemma isPivotal_setOpen (e : E) (A : Set (ConfigSpace E)) (ω : ConfigSpace E) :
    IsPivotal e A (setOpen e ω) ↔ IsPivotal e A ω

Uses 4

Statement usesConfiguration space of a statistical-mechanics model · Pivotal coordinate for an event · Opening a coordinate of a configuration

Proof usesClosing a coordinate of a configuration

LemmaClosing a coordinate preserves its pivotality#✓fully proved

Closing e does not change whether e is pivotal.

@[simp] lemma isPivotal_setClosed (e : E) (A : Set (ConfigSpace E)) (ω : ConfigSpace E) :
    IsPivotal e A (setClosed e ω) ↔ IsPivotal e A ω

Uses 4

Statement usesConfiguration space of a statistical-mechanics model · Pivotal coordinate for an event · Closing a coordinate of a configuration

Proof usesOpening a coordinate of a configuration

TheoremPivotal coordinates of an increasing event#✓fully proved

For an increasing event A, the coordinate e is pivotal at ω iff setClosed e ω ∉ A and setOpen e ω ∈ A.

theorem isPivotal_iff_of_isIncreasing {e : E} {A : Set (ConfigSpace E)}
    (hA : IsIncreasing A) (ω : ConfigSpace E) :
    IsPivotal e A ω ↔ (setClosed e ω ∉ A ∧ setOpen e ω ∈ A)

Uses 6 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Pivotal coordinate for an event · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Proof usesClosed configuration lies below the opened one

Used byRusso's formula on a single fiber · Aizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Duminil-Copin–Tassion differential inequality · Mean-field differential inequality for inhomogeneous percolation

DefinitionBernoulli weight of a single coordinate#✓fully proved

The weight of coordinate e in configuration ω with parameter p: p if ω e is open (true), 1 - p otherwise.

noncomputable def edgeWeight (p : ℝ) (ω : ConfigSpace E) (e : E) : ℝ :=
  if ω e then p else 1 - p

Uses 1 · Used by 14

Statement usesConfiguration space of a statistical-mechanics model

Used byOSSS Bernoulli weight equals the configuration weight · Bernoulli product weight of a configuration · Configuration weight splits at one coordinate · Nonnegativity of the configuration weight · Derivative of the configuration weight · Derivative of a single coordinate weight · Russo's formula on a single fiber · Product of coordinate weights off one coordinate · Off-coordinate weight depends only on the other coordinates · \(q = 1\) probability of an edge pattern is its Bernoulli weight · Russo's formula · Russo's formula · Probability of a finitely dependent event as a polynomial in \(p\) · Mass of a configuration on a finite index set is its product weight

DefinitionProduct of coordinate weights off one coordinate#✓fully proved

The product of the coordinate weights over all coordinates except e.

noncomputable def weightOff (p : ℝ) (e : E) (ω : ConfigSpace E) : ℝ :=
  ∏ j ∈ univ.erase e, edgeWeight p ω j

Uses 2 · Used by 11

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli weight of a single coordinate

Used byConfiguration weight splits at one coordinate · Derivative of the configuration weight · Derivative of the event weight before grouping · Russo's formula · Contribution of one coordinate to Russo's formula · Russo's formula on a single fiber · Off-coordinate weight depends only on the other coordinates · Russo's formula · Sharp threshold from influences · Russo's formula · Differentiability in \(p\) of the probability of a cylinder event

DefinitionBernoulli product weight of a configuration#✓fully proved

The product weight ∏ e, edgeWeight p ω e of a configuration; for p ∈ [0, 1] the probability of ω under independent Bernoulli(p) coordinates.

noncomputable def configWeight (p : ℝ) (ω : ConfigSpace E) : ℝ :=
  ∏ e, edgeWeight p ω e

Uses 2 · Used by 21

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli weight of a single coordinate

Used byPivotal-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 · Configuration weight splits at one coordinate · Configuration weight as a product weight · Nonnegativity of the configuration weight · Derivative of the configuration weight · Derivative of the event weight before grouping · Weight of the event that a coordinate is pivotal · Nonnegativity of the pivotal weight · Bernoulli weight of an event · Contribution of one coordinate to Russo's formula · Russo's formula on a single fiber · \(q = 1\) measure equals Bernoulli percolation on graph-edge events · \(q = 1\) probability of an edge pattern is its Bernoulli weight · Russo's formula · Duminil-Copin–Tassion differential inequality · Russo's formula · Bernoulli product measure of an event on a finite index set · Probability of a finitely dependent event as a polynomial in \(p\) · Mass of a configuration on a finite index set is its product weight

DefinitionBernoulli weight of an event#✓fully proved

The weight ∑ ω ∈ A, configWeight p ω of an event A; for p ∈ [0, 1] its probability under independent Bernoulli(p) coordinates.

noncomputable def prob (p : ℝ) (A : Set (ConfigSpace E)) : ℝ :=
  ∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * configWeight p ω

Uses 2 · Used by 32

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

Used byKKL on the interior of \((1/2, q)\) implies its event form there · Kahn–Kalai–Linial inequality · KKL inequality with constant 2 at \(p\) implies its event form · Event probability as the OSSS expectation of its indicator · Sharp-threshold bound assuming the KKL inequality on \((1/2, q)\) · Sharp-threshold window bound assuming the KKL inequality on \((1/2, q)\) · Variance of an event indicator is \(P(A)(1 - P(A))\) · Sharp-threshold bound under the \(p\)-biased KKL hypothesis · Sharp-threshold window under the \(p\)-biased KKL hypothesis · Sharp-threshold bound from the conditional KKL statement · Russo's formula · Derivative of the event weight before grouping · Russo's formula · Event weight as a product-weight probability · Increasing-event probabilities are monotone in the parameter · Sharp threshold from a KKL-type influence inequality · Russo's formula · Sharp threshold from influences · Box-crossing probability as a polynomial in the density · Duminil-Copin–Tassion differential inequality · Mean-field lower bound · Russo's formula · Probability of an event under Bernoulli product measure · Russo's formula · Russo's formula for the Bernoulli product measure · Sharpness of the phase transition · Russo's formula · Differentiability in \(p\) of the probability of a cylinder event · Bernoulli product measure of an event on a finite index set · Russo's formula · Probability of a finitely dependent event as a polynomial in \(p\) · Probability of a finitely dependent event as a finite weight

DefinitionWeight of the event that a coordinate is pivotal#✓fully proved

The weight of the event that coordinate e is pivotal for A.

noncomputable def pivotalProb (p : ℝ) (A : Set (ConfigSpace E)) (e : E) : ℝ :=
  ∑ ω, (Set.indicator {ω | IsPivotal e A ω} (fun _ => (1 : ℝ)) ω) * configWeight p ω

Uses 3 · Used by 16

Statement usesConfiguration space of a statistical-mechanics model · Pivotal coordinate for an event · Bernoulli product weight of a configuration

Used byPivotal-probability influence as the OSSS influence of an indicator · Russo's formula · Russo's formula · Nonnegativity of the pivotal weight · Contribution of one coordinate to Russo's formula · Increasing-event probabilities are monotone in the parameter · Influence of an edge on an event · Russo's formula · Sharp threshold from influences · Duminil-Copin–Tassion differential inequality · Russo's formula · Russo's formula · Russo's formula for the Bernoulli product measure · Russo's formula · Russo's formula · Russo's formula

LemmaConfiguration weight as a product weight#✓fully proved

configWeight is the product weight StatMech.pweight for Bernoulli coordinate weights.

lemma configWeight_eq_pweight (p : ℝ) (ω : ConfigSpace E) :
    configWeight p ω = pweight (fun _ b => if b then p else 1 - p) ω

Uses 3

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight of a configuration · Product weight of a configuration

LemmaNonnegativity of the configuration weight#✓fully proved

The product weight configWeight p ω is nonnegative for p ∈ [0, 1].

lemma configWeight_nonneg {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (ω : ConfigSpace E) :
    0 ≤ configWeight p ω

Uses 3 · Used by 1

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

Proof usesBernoulli weight of a single coordinate

Used byNonnegativity of the pivotal weight

LemmaNonnegativity of the pivotal weight#✓fully proved

The pivotal weight pivotalProb p A e is nonnegative for p ∈ [0, 1].

lemma pivotalProb_nonneg {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (A : Set (ConfigSpace E))
    (e : E) : 0 ≤ pivotalProb p A e

Uses 5 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Weight of the event that a coordinate is pivotal

Proof usesPivotal coordinate for an event · Bernoulli product weight of a configuration · Nonnegativity of the configuration weight

Used byIncreasing-event probabilities are monotone in the parameter

LemmaEvent weight as a product-weight probability#✓fully proved

prob is StatMech.wprob for Bernoulli coordinate weights.

lemma prob_eq_wprob (p : ℝ) (A : Set (ConfigSpace E)) :
    prob p A = wprob (fun _ b => if b then p else 1 - p) A

Uses 3

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli weight of an event · Weighted probability of an event

LemmaConfiguration weight splits at one coordinate#✓fully proved

The product weight splits as the weight of e times the weight of the other coordinates.

lemma configWeight_eq (p : ℝ) (e : E) (ω : ConfigSpace E) :
    configWeight p ω = edgeWeight p ω e * weightOff p e ω

Uses 4 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight of a configuration · Bernoulli weight of a single coordinate · Product of coordinate weights off one coordinate

Used byRusso's formula on a single fiber · Russo's formula · Russo's formula

LemmaOff-coordinate weight depends only on the other coordinates#✓fully proved

weightOff p e ω depends only on the values of ω off e.

lemma weightOff_congr (p : ℝ) (e : E) {ω ω' : ConfigSpace E}
    (h : ∀ e', e' ≠ e → ω e' = ω' e') : weightOff p e ω = weightOff p e ω'

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Product of coordinate weights off one coordinate

Proof usesBernoulli weight of a single coordinate

Used byContribution of one coordinate to Russo's formula

LemmaDerivative of a single coordinate weight#✓fully proved

The derivative in p of a coordinate weight is 1 if the coordinate is open, -1 otherwise.

lemma hasDerivAt_edgeWeight (ω : ConfigSpace E) (e : E) (p : ℝ) :
    HasDerivAt (fun p => edgeWeight p ω e) (if ω e then 1 else -1) p

Uses 2 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli weight of a single coordinate

Used byDerivative of the configuration weight

LemmaDerivative of the configuration weight#✓fully proved

The derivative in p of the product weight (product rule).

lemma hasDerivAt_configWeight (ω : ConfigSpace E) (p : ℝ) :
    HasDerivAt (fun p => configWeight p ω)
      (∑ e, weightOff p e ω * (if ω e then (1 : ℝ) else -1)) p

Uses 5 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight of a configuration · Product of coordinate weights off one coordinate

Proof usesBernoulli weight of a single coordinate · Derivative of a single coordinate weight

Used byDerivative of the event weight before grouping

LemmaDerivative of the event weight before grouping#✓fully proved

The derivative in p of prob p A, before grouping by pivotal coordinates.

lemma hasDerivAt_prob (A : Set (ConfigSpace E)) (p : ℝ) :
    HasDerivAt (fun p => prob p A)
      (∑ ω, A.indicator (fun _ => (1 : ℝ)) ω *
        ∑ e, weightOff p e ω * (if ω e then (1 : ℝ) else -1)) p

Uses 5 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli weight of an event · Product of coordinate weights off one coordinate

Proof usesBernoulli product weight of a configuration · Derivative of the configuration weight

Used byRusso's formula · Sharp threshold from influences · Differentiability in \(p\) of the probability of a cylinder event

LemmaOpening a coordinate of a split configuration#✓fully proved

Opening e in the configuration with value b at e and η elsewhere.

lemma setOpen_symm (e : E) (b : Bool) (η : {j : E // j ≠ e} → Bool) :
    setOpen e ((Equiv.funSplitAt e Bool).symm (b, η))
      = (Equiv.funSplitAt e Bool).symm (true, η)

Uses 2 · Used by 1

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

Used byContribution of one coordinate to Russo's formula

LemmaClosing a coordinate of a split configuration#✓fully proved

Closing e in the configuration with value b at e and η elsewhere.

lemma setClosed_symm (e : E) (b : Bool) (η : {j : E // j ≠ e} → Bool) :
    setClosed e ((Equiv.funSplitAt e Bool).symm (b, η))
      = (Equiv.funSplitAt e Bool).symm (false, η)

Uses 2 · Used by 1

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

Used byContribution of one coordinate to Russo's formula

LemmaRusso's formula on a single fiber#✓fully proved

Russo's formula on one fiber {ωt, ωf} of configurations differing only at e.

lemma russo_per_eta (p : ℝ) (A : Set (ConfigSpace E)) (hA : IsIncreasing A) (e : E)
    (ωt ωf : ConfigSpace E)
    (hwo : weightOff p e ωt = weightOff p e ωf)
    (hto : setOpen e ωt = ωt) (htc : setClosed e ωt = ωf)
    (ht : ωt e = true) (hf : ωf e = false) :
    A.indicator (fun _ => (1 : ℝ)) ωt * (weightOff p e ωt * if ωt e then 1 else -1) +
        A.indicator (fun _ => (1 : ℝ)) ωf * (weightOff p e ωf * if ωf e then 1 else -1) =
      {ω | IsPivotal e A ω}.indicator (fun _ => (1 : ℝ)) ωt * configWeight p ωt +
        {ω | IsPivotal e A ω}.indicator (fun _ => (1 : ℝ)) ωf * configWeight p ωf

Uses 12 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Pivotal coordinate for an event · Bernoulli product weight of a configuration · Closing a coordinate of a configuration · Opening a coordinate of a configuration · Product of coordinate weights off one coordinate

Proof usesConfiguration weight splits at one coordinate · Bernoulli weight of a single coordinate · Pivotality depends only on the other coordinates · Pivotal coordinates of an increasing event · Closed configuration lies below the opened one

Used byContribution of one coordinate to Russo's formula

LemmaContribution of one coordinate to Russo's formula#✓fully proved

The contribution of coordinate e to the derivative of prob p A is pivotalProb p A e, for increasing A.

lemma russo_per_edge (p : ℝ) (A : Set (ConfigSpace E)) (hA : IsIncreasing A) (e : E) :
    ∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * (weightOff p e ω * (if ω e then (1 : ℝ) else -1))
      = pivotalProb p A e

Uses 12 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Weight of the event that a coordinate is pivotal · Product of coordinate weights off one coordinate

Proof usesPivotal coordinate for an event · Bernoulli product weight of a configuration · Russo's formula on a single fiber · Closing a coordinate of a configuration · Closing a coordinate of a split configuration · Opening a coordinate of a configuration · Opening a coordinate of a split configuration · Off-coordinate weight depends only on the other coordinates

Used byRusso's formula · Russo's formula · Russo's formula

TheoremRusso's formula#✓fully proved

Russo's formula (Russo 1981; Margulis 1974): for an increasing event A on a finite set of coordinates, p ↦ prob p A has derivative ∑ e, pivotalProb p A e at every p.

theorem hasDerivAt_prob_eq_sum_pivotalProb
    (A : Set (ConfigSpace E)) (hA : IsIncreasing A) (p : ℝ) :
    HasDerivAt (fun p => prob p A) (∑ e, pivotalProb p A e) p

Uses 7 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Weight of the event that a coordinate is pivotal · Bernoulli weight of an event

Proof usesDerivative of the event weight before grouping · Contribution of one coordinate to Russo's formula · Product of coordinate weights off one coordinate

Used byRusso's formula · Russo's formula · Russo's formula · Russo's formula

TheoremRusso's formula#✓fully proved

Russo's formula, deriv form: d/dp prob p A = ∑ e, pivotalProb p A e for increasing A.

theorem deriv_prob_eq_sum_pivotalProb
    (A : Set (ConfigSpace E)) (hA : IsIncreasing A) (p : ℝ) :
    deriv (fun p => prob p A) p = ∑ e, pivotalProb p A e

Uses 5 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Weight of the event that a coordinate is pivotal · Bernoulli weight of an event

Proof usesRusso's formula

Used byIncreasing-event probabilities are monotone in the parameter · Russo's formula · Sharp threshold from influences

31 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.