Russo–Seymour–Welsh bounds for critical bond percolation on ℤ²

AbbreviationCritical bond percolation measure on the square lattice#✓fully proved

The critical bond percolation measure ℙ_{1/2} on {0, 1}^{Sym2 ℤ²}: every coordinate is open independently with probability 1/2.

noncomputable abbrev criticalBondMeasure : Measure (ConfigSpace (Sym2 (Lattice.Site 2))) :=
  bernoulliProductMeasure (1 / 2 : ℝ≥0) (by norm_num)

Uses 3 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Bernoulli product measure on configuration space

Used byRusso–Seymour–Welsh theorem · Russo–Seymour–Welsh theorem

TheoremRusso–Seymour–Welsh theorem#●ready to prove

Russo–Seymour–Welsh theorem (lower bound) for critical bond percolation on ℤ²: for every α > 0 there is c > 0 with ℙ_{1/2}(open left–right crossing of [0, ⌊αn⌋] × [0, n]) ≥ c for every n.

public theorem_wanted rsw_box_crossing_lower :
    P5 (fun _ => criticalBondMeasure.real)

Sources

• L. Russo, A note on percolation, Z. Wahrsch. Verw. Gebiete 43 (1978); P. D. Seymour and D. J. A. Welsh, Percolation probabilities on the square lattice, Ann. Discrete Math. 3 (1978); G. Grimmett, Percolation, 2nd ed. (1999), §11.7.

Uses 4

Statement usesCritical bond percolation measure on the square lattice · Configuration space of a statistical-mechanics model · Site of the hypercubic lattice · Box-crossing property for a sequence of measures

TheoremRusso–Seymour–Welsh theorem#●ready to prove

Russo–Seymour–Welsh theorem (two-sided form) for critical bond percolation on ℤ²: for every α > 0 there is c > 0 with c ≤ ℙ_{1/2}(open left–right crossing of [0, ⌊αn⌋] × [0, n]) ≤ 1 - c for every n with αn ≥ 1. The upper bound follows from the lower bound for the dual crossing.

public theorem_wanted rsw_box_crossing_two_sided :
    ∀ α : ℝ, 0 < α → ∃ c : ℝ, 0 < c ∧ ∀ n : ℕ, 1 ≤ α * n →
      c ≤ criticalBondMeasure.real (boxCrossingEvent α n) ∧
        criticalBondMeasure.real (boxCrossingEvent α n) ≤ 1 - c

Sources

• L. Russo, A note on percolation, Z. Wahrsch. Verw. Gebiete 43 (1978); P. D. Seymour and D. J. A. Welsh, Percolation probabilities on the square lattice, Ann. Discrete Math. 3 (1978); G. Grimmett, Percolation, 2nd ed. (1999), §11.7.

Uses 4

Statement usesCritical bond percolation measure on the square lattice · Configuration space of a statistical-mechanics model · Site of the hypercubic lattice · Left–right crossing event of a box with given aspect ratio

1 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.