Two-point connectivity with and without percolation

9 fully proved

A. Two-point connectivity and infinite clusters

DefinitionTwo-point connectivity of a bond measure on \(\mathbb{Z}^d\)#✓fully proved

The two-point connectivity μ(x ↔ y) of a measure on bond configurations of ℤ^d.

noncomputable def infiniteTwoPointReal
    (μ : Measure (ConfigSpace (Sym2 (Site d)))) (x y : Site d) : ℝ :=
  μ.real {ω | StatMech.Lattice.Connected d ω x y}

Uses 3 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Connection by an open path · Site of the hypercubic lattice

Used byJoint percolation at most connectivity given no two infinite clusters · Uniform decay of two-point connectivity without percolation · Two-point lower bound from FKG, invariance, uniqueness and percolation

DefinitionEvent that the open cluster of a site is infinite#✓fully proved

The event {x ↔ ∞} that the open cluster of x is infinite.

def clusterInfiniteEvent (d : ℕ) (x : Site d) :
    Set (ConfigSpace (Sym2 (Site d))) :=
  {ω | (cluster d ω x).Infinite}

Uses 3 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Open cluster of a site

Used byJoint percolation at most connectivity given no two infinite clusters · Two-point lower bound from FKG, invariance, uniqueness and percolation · Disconnected sites in infinite clusters give two infinite clusters

LemmaDisconnected sites in infinite clusters give two infinite clusters#✓fully proved

If x and y both lie in infinite clusters, either they are connected or there are at least two infinite clusters.

lemma two_infinite_clusters_of_not_connected (x y : Site d) :
    clusterInfiniteEvent d x ∩ clusterInfiniteEvent d y ⊆
      {ω | StatMech.Lattice.Connected d ω x y} ∪ atLeastTwoInfinite d

Uses 9 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Event that the open cluster of a site is infinite · Connection by an open path · Site of the hypercubic lattice · Event of at least two infinite open clusters

Proof usesOpen cluster of a site · Open subgraph of a bond configuration · Set of infinite open clusters · Number of infinite open clusters

Used byJoint percolation at most connectivity given no two infinite clusters

LemmaJoint percolation at most connectivity given no two infinite clusters#✓fully proved

With at most one infinite cluster almost surely, μ(x ↔ ∞, y ↔ ∞) ≤ μ(x ↔ y).

lemma infinite_cluster_inter_le_twoPoint
    (μ : Measure (ConfigSpace (Sym2 (Site d)))) [IsFiniteMeasure μ]
    (huniq : μ (atLeastTwoInfinite d) = 0) (x y : Site d) :
    μ.real (clusterInfiniteEvent d x ∩ clusterInfiniteEvent d y) ≤
      infiniteTwoPointReal μ x y

Uses 7 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Event that the open cluster of a site is infinite · Two-point connectivity of a bond measure on \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Event of at least two infinite open clusters

Proof usesDisconnected sites in infinite clusters give two infinite clusters · Connection by an open path

Used byTwo-point lower bound from FKG, invariance, uniqueness and percolation

LemmaTwo-point lower bound from FKG, invariance, uniqueness and percolation#✓fully proved

If μ satisfies the FKG inequality for the events {x ↔ ∞} (hPA), is translation invariant on them (hTI), has at most one infinite cluster almost surely (huniq), and percolates (htheta), then μ(0 ↔ x) ≥ θ² for every x.

lemma infiniteTwoPoint_uniform_pos_of_fkg_unique
    (μ : Measure (ConfigSpace (Sym2 (Site d)))) [IsFiniteMeasure μ]
    (hPA : ∀ x : Site d,
      μ.real (clusterInfiniteEvent d (origin d)) *
          μ.real (clusterInfiniteEvent d x) ≤
        μ.real (clusterInfiniteEvent d (origin d) ∩ clusterInfiniteEvent d x))
    (hTI : ∀ x : Site d,
      μ.real (clusterInfiniteEvent d x) =
        μ.real (clusterInfiniteEvent d (origin d)))
    (huniq : μ (atLeastTwoInfinite d) = 0)
    (htheta : 0 < μ.real (percolationEvent d)) :
    ∃ c : ℝ, 0 < c ∧ ∀ x : Site d,
      c ≤ infiniteTwoPointReal μ (origin d) x

Uses 8

Statement usesConfiguration space of a statistical-mechanics model · Event that the open cluster of a site is infinite · Two-point connectivity of a bond measure on \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Event of at least two infinite open clusters · Origin of the hypercubic lattice · Percolation event for the origin

Proof usesJoint percolation at most connectivity given no two infinite clusters

B. Box-boundary connections and the percolation probability

LemmaCrossing probabilities converge to the percolation probability#✓fully proved

For any finite measure, the probability that the origin is connected to the complement of the box of radius n - 1 tends to the percolation probability.

lemma crossingEvent_real_tendsto_percolation
    (μ : Measure (ConfigSpace (Sym2 (Site d)))) [IsFiniteMeasure μ] :
    Tendsto (fun n => μ.real (crossingEvent d n)) atTop
      (nhds (μ.real (percolationEvent d)))

Uses 9 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · One-arm event from the origin · Percolation event for the origin

Proof usesCrossing events intersect to the percolation event · Connection by an open path · Box \((-n, n)^d\) in the hypercubic lattice · Measurability of the one-arm event · Origin of the hypercubic lattice

Used byBox-boundary connection probability tends to percolation probability

LemmaBox-boundary connection probability tends to percolation probability#✓fully proved

For any finite measure, the probability that the origin is connected to the boundary of the box of radius n inside the box tends to the percolation probability.

lemma boxBdryConnEvent_real_tendsto_percolation
    (μ : Measure (ConfigSpace (Sym2 (Site d)))) [IsFiniteMeasure μ] :
    Tendsto (fun n => μ.real (boxBdryConnEvent d n)) atTop
      (nhds (μ.real (percolationEvent d)))

Uses 8 · Used by 7

Statement usesConfiguration space of a statistical-mechanics model · Event that the box origin connects to the box boundary · Site of the hypercubic lattice · Percolation event for the origin

Proof usesBoundary connection inside \(\Lambda_n\) reaches outside \(\Lambda_{n-1}\) · Crossing probabilities converge to the percolation probability · Leaving \(\Lambda_n\) implies connecting to \(\partial\Lambda_n\) · One-arm event from the origin

Used byWired \(q = 2\) percolation probability at most the Bernoulli one · Monotonicity in \(p\) of the Bernoulli percolation probability · 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 · Uniform decay of two-point connectivity without percolation

LemmaA connection to outside the box passes through the box boundary#✓fully proved

A connection from the origin to a site outside the box passes through the box boundary.

lemma connectionEvent_subset_boxBdryConnEvent (n : ℕ) (hn : 1 ≤ n)
    (x : Site d) (hx : x ∉ box d n) :
    {ω | StatMech.Lattice.Connected d ω (origin d) x} ⊆ boxBdryConnEvent d n

Uses 13 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Event that the box origin connects to the box boundary · Connection by an open path · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Origin of the hypercubic lattice

Proof usesOpen path from the origin out of \(\Lambda_n\) gives \(0 \leftrightarrow \partial\Lambda_n\) inside \(\Lambda_n\) · Vertex boundary of a box · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Open connection of a vertex to the boundary · Origin as a vertex of the box graph

Used byUniform decay of two-point connectivity without percolation

LemmaUniform decay of two-point connectivity without percolation#✓fully proved

Without percolation, the two-point connectivity from the origin tends to zero uniformly: for every ε > 0 there is n with μ(0 ↔ x) < ε for all x outside the box of radius n.

lemma infiniteTwoPoint_uniform_decay_of_no_percolation
    (μ : Measure (ConfigSpace (Sym2 (Site d)))) [IsFiniteMeasure μ]
    (htheta : μ.real (percolationEvent d) = 0) :
    ∀ ε : ℝ, 0 < ε → ∃ n : ℕ, 1 ≤ n ∧ ∀ x : Site d, x ∉ box d n →
      infiniteTwoPointReal μ (origin d) x < ε

Uses 10

Statement usesConfiguration space of a statistical-mechanics model · Two-point connectivity of a bond measure on \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Origin of the hypercubic lattice · Percolation event for the origin

Proof usesEvent that the box origin connects to the box boundary · Box-boundary connection probability tends to percolation probability · A connection to outside the box passes through the box boundary · Connection by an open path

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.