Bernoulli product measures and cylinder events

DefinitionBernoulli distribution on the Booleans#✓fully proved

The Bernoulli distribution on Bool with success probability p: mass p on true and 1 - p on false. This is Mathlib's ProbabilityTheory.bernoulliMeasure true false p, with the parameter given as an ℝ≥0 bounded by 1.

noncomputable def bernoulliMeasure (p : ℝ≥0) (hp : p ≤ 1) : Measure Bool :=
  ProbabilityTheory.bernoulliMeasure true false ⟨p, p.2, hp⟩

Used by 50

Used byBernoulli product weight computes product-measure integrals · Bernoulli point masses sum to one · Bernoulli product measure as a weighted probability · BK criterion for Bernoulli product measures · Van den Berg–Kesten inequality · Union bound from the three-event BK inequality · BK inequality on countable configuration spaces · Inhomogeneous Bernoulli product measure · BK inequality for inhomogeneous Bernoulli measures on a finite set · BK inequality for inhomogeneous measures on a countable set · Reimer equality for events determined by disjoint coordinates · Reimer's inequality for mixed monotone events, Bernoulli measure · BK inequality for decreasing events · Reimer's inequality for Bernoulli measures, assuming the core case · Reimer's inequality for disjoint events · Agreement of the two critical probabilities · Bernoulli product pulled back along an injection is Bernoulli · Wired \(q = 2\) percolation probability at most the Bernoulli one · \(p_c(2) < 1\) from anchored dual-circuit enclosure · Positivity of the critical probability (Hammersley's bound) · Monotonicity in \(p\) of the Bernoulli percolation probability · \(\theta_2(p) \le \theta_{2+k}(p)\) for Bernoulli percolation · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Duminil-Copin–Tassion differential inequality · Mean-field lower bound · Translation invariance of the Bernoulli product measure · Exponential decay below p̃_c · Exploration independence of a cluster inside a set · Exponential decay from a one-step recursion · Bernoulli weight of a single edge · Sharpness of the phase transition, conditional form · Equality of the Duminil-Copin–Tassion threshold and \(p_c\) · Sharpness of the phase transition · Positivity of the Duminil-Copin–Tassion threshold · Mass of a configuration under a finite Bernoulli product measure · Bernoulli distribution agrees with the library Bernoulli measure · Point masses of the Bernoulli distribution · Bernoulli product measure on configuration space · Bernoulli product measure of a cylinder event · Probability of an event as a sum of configuration masses · Mass of a configuration under a finite Bernoulli product measure, real form · Mass of a configuration on a finite index set is its product weight · Log-modularity of Bernoulli product weights · Configuration masses sum to one · Bernoulli zero-one law for infinite groups acting finite-to-one · Independence of coordinates under the Bernoulli product measure · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition

LemmaBernoulli distribution agrees with the library Bernoulli measure#✓fully proved

bernoulliMeasure p hp is Mathlib's ProbabilityTheory.bernoulliMeasure true false p.

lemma bernoulliMeasure_eq (p : ℝ≥0) (hp : p ≤ 1) :
    bernoulliMeasure p hp = ProbabilityTheory.bernoulliMeasure true false ⟨p, p.2, hp⟩

Uses 1

Statement usesBernoulli distribution on the Booleans

DefinitionBernoulli product measure on configuration space#✓fully proved

The Bernoulli product measure on ConfigSpace E: the coordinates are independent and each is true with probability p (Measure.infinitePi of bernoulliMeasure p hp). See also Mathlib's ProbabilityTheory.setBernoulli, the same product measure on Set E.

noncomputable def bernoulliProductMeasure (p : ℝ≥0) (hp : p ≤ 1) :
    Measure (ConfigSpace E) :=
  Measure.infinitePi (fun _ : E => bernoulliMeasure p hp)

Uses 2 · Used by 69

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli distribution on the Booleans

Used byBernoulli product weight computes product-measure integrals · Harris inequality · Harris inequality for finitely dependent increasing events · Bernoulli product measure as a weighted probability · BK criterion for Bernoulli product measures · Van den Berg–Kesten inequality · Union bound from the three-event BK inequality · BK inequality on countable configuration spaces · Increasing-event probabilities are monotone in the parameter · BK inequality for three increasing events · Inhomogeneous Bernoulli product with constant parameter · Reimer equality for events determined by disjoint coordinates · Reimer's inequality for mixed monotone events, Bernoulli measure · BK inequality for decreasing events · Reimer's inequality for Bernoulli measures, assuming the core case · Reimer's inequality for disjoint events · Reimer's inequality for the XOR and XNOR events · Agreement of the two critical probabilities · Percolation probability as an extended real · Critical bond percolation measure on the square lattice · Bernoulli box cylinder probability equals its probability on the box · Bernoulli percolation restricted to a box is Bernoulli on the box · Bernoulli product pulled back along an injection is Bernoulli · Bernoulli percolation restricted to the plane is planar Bernoulli · \(q = 1\) measure equals Bernoulli percolation on graph-edge events · Wired \(q = 2\) percolation probability at most the Bernoulli one · \(p_c(2) < 1\) from anchored dual-circuit enclosure · Positivity of the critical probability (Hammersley's bound) · Monotonicity in \(p\) of the Bernoulli percolation probability · \(\theta_2(p) \le \theta_{2+k}(p)\) for Bernoulli percolation · Wired \(q = 2\) origin-to-boundary probability at most Bernoulli · Percolation probability of bond percolation · Burton–Keane theorem · Box-crossing probability · Duminil-Copin–Tassion differential inequality · Mean-field lower bound · Translation invariance of the Bernoulli product measure · One-arm probability · Exponential decay below p̃_c · Exploration independence of a cluster inside a set · Exponential decay from a one-step recursion · Probability of an event under Bernoulli product measure · Russo's formula · Russo's formula for the Bernoulli product measure · Sharpness of the phase transition, conditional form · Equality of the Duminil-Copin–Tassion threshold and \(p_c\) · Sharpness of the phase transition · Positivity of the Duminil-Copin–Tassion threshold · Probability of connection inside a set · Mass of a configuration under a finite Bernoulli product measure · Bernoulli product measure of a cylinder event · Bernoulli product measure on bonds is the bond percolation law · Bernoulli product measure of an event on a finite index set · Probability of an event as a sum of configuration masses · Bernoulli product measure of a cylinder event, real-valued form · Probability of a finitely dependent event as a polynomial in \(p\) · Probability of a finitely dependent event as a finite weight · Mass of a configuration under a finite Bernoulli product measure, real form · Mass of a configuration on a finite index set is its product weight · Log-modularity of Bernoulli product weights · Nonnegativity of configuration masses · Configuration masses sum to one · Bernoulli zero-one law for infinite groups acting finite-to-one · Independence of coordinates under the Bernoulli product measure · Ergodicity of Bernoulli measures under free infinite-group actions · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition

LemmaBernoulli product measure on bonds is the bond percolation law#✓fully proved

On bond configurations Sym2 V → Bool, bernoulliProductMeasure is the bond percolation law MathlibExt.Probability.ProductBondPercolation.gbernoulliLaw.

lemma bernoulliProductMeasure_eq_gbernoulliLaw {V : Type*} (p : ℝ≥0) (hp : p ≤ 1) :
    bernoulliProductMeasure (E := Sym2 V) p hp
      = MathlibExt.Probability.ProductBondPercolation.gbernoulliLaw (p : ℝ) p.2 hp

Uses 3

Statement usesBernoulli bond law on \(V\) · Configuration space of a statistical-mechanics model · Bernoulli product measure on configuration space

TheoremMass of a configuration under a finite Bernoulli product measure#✓fully proved

For finite E, the mass of a configuration is the product of its coordinate masses.

theorem apply_singleton [Fintype E] (ω : ConfigSpace E) :
    bernoulliProductMeasure (E := E) p hp {ω} = ∏ e, bernoulliMeasure p hp {ω e}

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli distribution on the Booleans · Bernoulli product measure on configuration space

Used byMass of a configuration under a finite Bernoulli product measure, real form

TheoremMass of a configuration under a finite Bernoulli product measure, real form#✓fully proved

For finite E, the mass of a configuration is the product of its coordinate masses.

theorem real_singleton [Fintype E] (ω : ConfigSpace E) :
    (bernoulliProductMeasure (E := E) p hp).real {ω}
      = ∏ e, (bernoulliMeasure p hp).real {ω e}

Uses 4 · Used by 7

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli distribution on the Booleans · Bernoulli product measure on configuration space

Proof usesMass of a configuration under a finite Bernoulli product measure

Used byBernoulli product weight computes product-measure integrals · Bernoulli product measure as a weighted probability · Duminil-Copin–Tassion differential inequality · Exponential decay below p̃_c · Exploration independence of a cluster inside a set · Mass of a configuration on a finite index set is its product weight · Log-modularity of Bernoulli product weights

TheoremProbability of an event as a sum of configuration masses#✓fully proved

For finite E, the probability of an event is the sum of the masses of its configurations.

theorem real_eq_sum [Fintype E] [DecidableEq E] (S : Set (ConfigSpace E)) :
    (bernoulliProductMeasure (E := E) p hp).real S
      = ∑ ω : ConfigSpace E,
          S.indicator (fun _ => (1 : ℝ)) ω * (bernoulliProductMeasure (E := E) p hp).real {ω}

Uses 3 · Used by 6

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

Proof usesBernoulli distribution on the Booleans

Used byHarris inequality · Bernoulli product measure as a weighted probability · Duminil-Copin–Tassion differential inequality · Exponential decay below p̃_c · Exploration independence of a cluster inside a set · Bernoulli product measure of an event on a finite index set

TheoremNonnegativity of configuration masses#✓fully proved

Configuration masses are nonnegative.

theorem real_singleton_nonneg (ω : ConfigSpace E) :
    0 ≤ (bernoulliProductMeasure (E := E) p hp).real {ω}

Uses 2 · Used by 1

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

Used byHarris inequality

TheoremConfiguration masses sum to one#✓fully proved

For finite E, the configuration masses sum to 1.

theorem sum_real_singleton [Fintype E] [DecidableEq E] :
    ∑ ω : ConfigSpace E, (bernoulliProductMeasure (E := E) p hp).real {ω} = 1

Uses 3 · Used by 1

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

Proof usesBernoulli distribution on the Booleans

Used byHarris inequality

TheoremLog-modularity of Bernoulli product weights#✓fully proved

The configuration weights of a Bernoulli product measure are log-modular: w(a) w(b) = w(a ⊔ b) w(a ⊓ b). In particular they satisfy the FKG lattice condition.

theorem real_singleton_logModular [Fintype E] (a b : ConfigSpace E) :
    (bernoulliProductMeasure (E := E) p hp).real {a}
        * (bernoulliProductMeasure (E := E) p hp).real {b}
      = (bernoulliProductMeasure (E := E) p hp).real {a ⊔ b}
        * (bernoulliProductMeasure (E := E) p hp).real {a ⊓ b}

Uses 4 · Used by 1

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

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

Used byHarris inequality

LemmaPoint masses of the Bernoulli distribution#✓fully proved

The mass of a point under the Bernoulli distribution: p at true, 1 - p at false.

lemma bernoulliMeasure_real_singleton (p : ℝ≥0) (hp : p ≤ 1) (b : Bool) :
    (bernoulliMeasure p hp).real {b} = if b then (p : ℝ) else 1 - p

Uses 1 · Used by 1

Statement usesBernoulli distribution on the Booleans

Used byMass of a configuration on a finite index set is its product weight

LemmaMass of a configuration on a finite index set is its product weight#✓fully proved

On a finite index set, the mass of a configuration is its product weight configWeight.

lemma realSingleton_eq_configWeight [Fintype E] (p : ℝ≥0) (hp : p ≤ 1)
    (ω : ConfigSpace E) :
    (bernoulliProductMeasure (E := E) p hp).real {ω} = configWeight (p : ℝ) ω

Uses 7 · Used by 1

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

Proof usesBernoulli distribution on the Booleans · Point masses of the Bernoulli distribution · Mass of a configuration under a finite Bernoulli product measure, real form · Bernoulli weight of a single coordinate

Used byBernoulli product measure of an event on a finite index set

LemmaBernoulli product measure of an event on a finite index set#✓fully proved

On a finite index set, the Bernoulli product measure of an event is its weight prob p.

lemma finiteRealProb_eq_prob [Fintype E] (p : ℝ≥0) (hp : p ≤ 1)
    (S : Set (ConfigSpace E)) :
    (bernoulliProductMeasure (E := E) p hp).real S = prob (p : ℝ) S

Uses 6 · Used by 2

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

Proof usesProbability of an event as a sum of configuration masses · Bernoulli product weight of a configuration · Mass of a configuration on a finite index set is its product weight

Used byRusso's formula · Probability of a finitely dependent event as a finite weight

DefinitionConfiguration patched from one configuration on a finite set and another off it#✓fully proved

The configuration that agrees with η on the finite set F and with ω off F.

noncomputable def extendOff (F : Finset E) (ω : ConfigSpace E) (η : ConfigSpace ↥F) :
    ConfigSpace E := fun j => if h : j ∈ F then η ⟨j, h⟩ else ω j

Uses 1 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model

Used byDuminil-Copin–Tassion differential inequality · Exponential decay below p̃_c · Exploration independence of a cluster inside a set · Finite projections of increasing events are increasing

LemmaEvents depending on finitely many coordinates are cylinders#✓fully proved

An event whose indicator depends only on the coordinates in F is the cylinder over its projection onto F.

lemma eq_cylinder_restrict_image (A : Set (ConfigSpace E)) (F : Finset E)
    (hA : DependsOn (A.indicator (fun _ => (1 : ℝ))) (F : Set E)) :
    A = cylinder F (F.restrict '' A)

Uses 1 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model

Used by\(q = 1\) measure equals Bernoulli percolation on graph-edge events · Duminil-Copin–Tassion differential inequality · Exponential decay below p̃_c · Exploration independence of a cluster inside a set · Probability of a finitely dependent event as a finite weight

LemmaBernoulli product measure of a cylinder event#✓fully proved

The infinite Bernoulli product measure of a cylinder over F is the finite Bernoulli product measure of its base.

lemma bernoulliProductMeasure_cylinder (p : ℝ≥0) (hp : p ≤ 1) (F : Finset E)
    (S : Set (ConfigSpace ↥F)) :
    bernoulliProductMeasure (E := E) p hp (cylinder F S)
      = bernoulliProductMeasure (E := ↥F) p hp S

Uses 3 · Used by 1

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

Proof usesBernoulli distribution on the Booleans

Used byBernoulli product measure of a cylinder event, real-valued form

LemmaBernoulli product measure of a cylinder event, real-valued form#✓fully proved

Real-valued form of bernoulliProductMeasure_cylinder.

lemma realProb_cylinder (p : ℝ≥0) (hp : p ≤ 1) (F : Finset E)
    (S : Set (ConfigSpace ↥F)) :
    (bernoulliProductMeasure (E := E) p hp).real (cylinder F S)
      = (bernoulliProductMeasure (E := ↥F) p hp).real S

Uses 3 · Used by 6

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

Proof usesBernoulli product measure of a cylinder event

Used byHarris inequality for finitely dependent increasing events · BK inequality on countable configuration spaces · Duminil-Copin–Tassion differential inequality · Exponential decay below p̃_c · Exploration independence of a cluster inside a set · Probability of a finitely dependent event as a finite weight

TheoremProbability of a finitely dependent event as a finite weight#✓fully proved

The probability of an event depending only on the coordinates in F is the finite weight prob p of its projection onto F.

theorem realProb_cylinder_eq_prob (p : ℝ≥0) (hp : p ≤ 1)
    (A : Set (ConfigSpace E)) (F : Finset E)
    (hA : DependsOn (A.indicator (fun _ => (1 : ℝ))) (F : Set E)) :
    (bernoulliProductMeasure (E := E) p hp).real A
      = prob (p : ℝ) (F.restrict '' A)

Uses 6 · Used by 5

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

Proof usesEvents depending on finitely many coordinates are cylinders · Bernoulli product measure of an event on a finite index set · Bernoulli product measure of a cylinder event, real-valued form

Used byIncreasing-event probabilities are monotone in the parameter · Duminil-Copin–Tassion differential inequality · Mean-field lower bound · Sharpness of the phase transition · Probability of a finitely dependent event as a polynomial in \(p\)

TheoremProbability of a finitely dependent event as a polynomial in \(p\)#✓fully proved

The probability of an event depending only on the coordinates in F, as an explicit polynomial in p.

theorem realProb_cylinder_eq_finsum (p : ℝ≥0) (hp : p ≤ 1)
    (A : Set (ConfigSpace E)) (F : Finset E)
    (hA : DependsOn (A.indicator (fun _ => (1 : ℝ))) (F : Set E)) :
    (bernoulliProductMeasure (E := E) p hp).real A
      = ∑ η : ConfigSpace ↥F,
          (F.restrict '' A).indicator (fun _ => (1 : ℝ)) η
            * ∏ e : ↥F, (if η e then (p : ℝ) else 1 - p)

Uses 6 · Used by 3

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

Proof usesBernoulli product weight of a configuration · Bernoulli weight of a single coordinate · Bernoulli weight of an event · Probability of a finitely dependent event as a finite weight

Used by\(q = 1\) measure equals Bernoulli percolation on graph-edge events · Duminil-Copin–Tassion differential inequality · Exponential decay below p̃_c

TheoremDifferentiability in \(p\) of the probability of a cylinder event#✓fully proved

The weight of the projection of an event onto finitely many coordinates is differentiable in p.

theorem differentiable_realProb_cylinder
    (A : Set (ConfigSpace E)) (F : Finset E) :
    Differentiable ℝ (fun q => prob q (F.restrict '' A))

Uses 4 · Used by 3

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

Proof usesDerivative of the event weight before grouping · Product of coordinate weights off one coordinate

Used byIncreasing-event probabilities are monotone in the parameter · Mean-field lower bound · Sharpness of the phase transition

LemmaFinite projections of increasing events are increasing#✓fully proved

The projection of an increasing event onto finitely many coordinates is increasing.

lemma isIncreasing_restrict_image (A : Set (ConfigSpace E)) (hA : IsIncreasing A)
    (F : Finset E) : IsIncreasing (F.restrict '' A)

Uses 3 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Increasing event

Proof usesConfiguration patched from one configuration on a finite set and another off it

Used byIncreasing-event probabilities are monotone in the parameter · Russo's formula

TheoremRusso's formula#✓fully proved

Russo's formula for an increasing event A projected onto finitely many coordinates F: the derivative in p of its weight is the sum over e ∈ F of the weight of the event that e is pivotal (L. Russo, 1981).

theorem hasDerivAt_realProb_cylinder_pivotal
    (A : Set (ConfigSpace E)) (hA : IsIncreasing A) (F : Finset E) (q : ℝ) :
    HasDerivAt (fun q => prob q (F.restrict '' A))
      (∑ e : ↥F, pivotalProb q (F.restrict '' A) e) q

Uses 6 · Used by 1

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 · Finite projections of increasing events are increasing

Used byRusso's formula

TheoremRusso's formula#✓fully proved

Russo's formula, deriv form of hasDerivAt_realProb_cylinder_pivotal.

theorem deriv_realProb_cylinder_pivotal
    (A : Set (ConfigSpace E)) (hA : IsIncreasing A) (F : Finset E) (q : ℝ) :
    deriv (fun q => prob q (F.restrict '' A)) q
      = ∑ e : ↥F, pivotalProb q (F.restrict '' A) e

Uses 5 · Used by 1

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 byDuminil-Copin–Tassion differential inequality

23 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.