Russo's formula for percolation

DefinitionProbability of an event under Bernoulli product measure#✓fully proved

The probability ℙ_p(A) of A under the Bernoulli(p) product measure on {0, 1}^E for p ∈ [0, 1]; outside [0, 1] it is the polynomial StatMech.prob p A, so that the function is defined on all of ℝ.

noncomputable def measureProb (A : Set (ConfigSpace E)) (p : ℝ) : ℝ :=
  if h : 0 ≤ p ∧ p ≤ 1 then
    (bernoulliProductMeasure (E := E) ⟨p, h.1⟩ (by exact_mod_cast h.2)).real A
  else prob p A

Uses 3 · Used by 3

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

Used byRusso's formula · Russo's formula for the Bernoulli product measure · Russo's formula

TheoremRusso's formula#✓fully proved

Russo's formula (Margulis–Russo): for an increasing event A on a finite edge set and 0 < p < 1, p ↦ ℙ_p(A) has derivative ∑_e ℙ_p(e is pivotal for A) at p. See also StatMech.hasDerivAt_prob_eq_sum_pivotalProb (the polynomial form, for all p) and StatMech.hasDerivAt_realProb_cylinder_pivotal (cylinder events on an infinite edge set).

theorem russo_derivative (A : Set (ConfigSpace E)) (hA : IsIncreasing A)
    {p : ℝ} (h0 : 0 < p) (h1 : p < 1) :
    HasDerivAt (fun p => measureProb A p) (∑ e, pivotalProb p A e) p

Uses 8 · Used by 2

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

Proof usesBernoulli product measure on configuration space · Bernoulli product measure of an event on a finite index set · Russo's formula · Bernoulli weight of an event

Used byRusso's formula for the Bernoulli product measure · Russo's formula

TheoremRusso's formula#✓fully proved

Russo's formula, deriv form: d/dp ℙ_p(A) = ∑_e ℙ_p(e is pivotal for A) for an increasing event A and 0 < p < 1.

theorem russo_formula (A : Set (ConfigSpace E)) (hA : IsIncreasing A)
    {p : ℝ} (h0 : 0 < p) (h1 : p < 1) :
    deriv (fun p => measureProb A p) p = ∑ e, pivotalProb p A e

Uses 5

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

Proof usesRusso's formula

TheoremRusso's formula for the Bernoulli product measure#✓fully proved

Russo's formula for p : ℝ≥0, packaged with the identification of measureProb A p with (bernoulliProductMeasure p hp).real A.

theorem russo_derivative_measure (A : Set (ConfigSpace E)) (hA : IsIncreasing A)
    (p : ℝ≥0) (hp : p ≤ 1) (h0 : 0 < (p : ℝ)) (h1 : (p : ℝ) < 1) :
    HasDerivAt (fun q => measureProb A q) (∑ e, pivotalProb (p : ℝ) A e) (p : ℝ)
      ∧ measureProb A (p : ℝ) = (bernoulliProductMeasure (E := E) p hp).real A

Uses 7

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Probability of an event under Bernoulli product measure · Bernoulli product measure on configuration space · Weight of the event that a coordinate is pivotal

Proof usesRusso's formula · Bernoulli weight of an event

DefinitionReal-valued indicator that an edge is open#✓fully proved

The indicator ω_e ∈ {0, 1} (as a real number) that the edge e is open in ω.

noncomputable def openInd (ω : ConfigSpace E) (e : E) : ℝ := if ω e then 1 else 0

Uses 1 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model

Used byRusso's formula

TheoremRusso's formula#✓fully proved

Russo's formula in pivotal-factor form: for increasing A and 0 < p < 1, d/dp ℙ_p(A) = (p(1 - p))⁻¹ ∑_e 𝔼_p[1_A (ω_e - p)].

theorem hasDerivAt_prob_eq_pivotalFactor (A : Set (ConfigSpace E))
    (hA : IsIncreasing A) {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1) :
    HasDerivAt (fun p => prob p A)
      ((1 / (p * (1 - p))) *
        ∑ e, ∑ ω, A.indicator (fun _ => (1 : ℝ)) ω *
          ((openInd ω e - p) * configWeight p ω)) p

Uses 11

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Real-valued indicator that an edge is open · Bernoulli product weight of a configuration · Bernoulli weight of an event

Proof usesConfiguration weight splits at one coordinate · Bernoulli weight of a single coordinate · Russo's formula · Weight of the event that a coordinate is pivotal · Contribution of one coordinate to Russo's formula · Product of coordinate weights off one coordinate

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.