The FK percolation probability as a limit of crossing probabilities

3 fully proved

A. Crossing events

LemmaCrossing events intersect to the percolation event#✓fully proved

The crossing events intersect to the percolation event. See also Percolation.percolationEvent_eq_iInter (Sharpness), the same fact indexed from n + 1.

lemma iInter_crossingEvent_eq_percolationEvent :
    (⋂ n : ℕ, crossingEvent d n) = percolationEvent d

Uses 9 · Used by 2

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 usesConnection by an open path · Box \((-n, n)^d\) in the hypercubic lattice · Open cluster of a site · Every finite set of sites lies in a box · Origin of the hypercubic lattice

Used byWired crossing probabilities converge to the percolation probability · Crossing probabilities converge to the percolation probability

B. The limit

DefinitionWired probability that the origin connects to the outside of a box#✓fully proved

The probability, under the chosen wired infinite-volume measure, that the origin is connected to the complement of Λ_(n-1).

noncomputable def fkBoundaryConnReal (d : ℕ) {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (n : ℕ) : ℝ :=
  ((wiredInfiniteVolume d hp hp1 hq : ProbabilityMeasure (ConfigSpace (Sym2 (Site d)))) :
      Measure (ConfigSpace (Sym2 (Site d)))).real (crossingEvent d n)

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice · One-arm event from the origin

Used byWired crossing probabilities converge to the percolation probability

LemmaWired crossing probabilities converge to the percolation probability#✓fully proved

The crossing probabilities of the wired infinite-volume measure converge to the percolation probability fkTheta.

lemma fkBoundaryConnReal_tendsto_fkTheta {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) :
    Tendsto (fun n => fkBoundaryConnReal d hp hp1 hq n) atTop
      (𝓝 (fkTheta d hp hp1 hq (q := q)))

Uses 12 · Used by 1

Statement usesWired probability that the origin connects to the outside of a box · Wired random-cluster percolation probability \(\theta(p, q)\)

Proof usesConfiguration space of a statistical-mechanics model · Crossing events intersect to the percolation event · Wired infinite-volume random-cluster measure · Connection by an open path · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · One-arm event from the origin · Measurability of the one-arm event · Origin of the hypercubic lattice · Percolation event for the origin

Used byWired infinite-volume boundary connection tends to \(\theta^1(p, q)\)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.