Free percolation above the random-cluster critical point

5 fully proved

A. Wired percolation above the critical point

LemmaWired percolation above the random-cluster critical point#✓fully proved

Above the critical point the wired measure percolates: θ¹(p, q) > 0 for p > p_c(q, d).

lemma frp_fkTheta_pos_of_gt_fkPc (d : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) (hpc : fkPc d q < p) :
    0 < fkTheta d hp hp1 hq (q := q)

Uses 8 · Used by 1

Statement usesCritical parameter \(p_c(q)\) of the random-cluster model · Wired random-cluster percolation probability \(\theta(p, q)\)

Proof usesConfiguration space of a statistical-mechanics model · Non-percolating parameters of the wired random-cluster measure · Subcritical set is bounded above by one · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice · Percolation event for the origin

Used byFree percolation from domination and free–wired agreement at \(p'\)

LemmaMeasurability of the percolation event#✓fully proved

The percolation event is measurable.

lemma frp_measurableSet_percolationEvent (d : ℕ) :
    MeasurableSet (Percolation.percolationEvent d)

Uses 10 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · 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 · One-arm event from the origin · Measurability of the one-arm event · Origin of the hypercubic lattice

Used by\(\theta_2(p) \le \theta_{2+k}(p)\) for Bernoulli percolation · Free percolation from domination and free–wired agreement at \(p'\)

LemmaThe percolation event is increasing#✓fully proved

The percolation event is increasing.

lemma frp_isIncreasing_percolationEvent (d : ℕ) :
    IsIncreasing (Percolation.percolationEvent d)

Uses 9 · Used by 1

Statement usesIncreasing event · Site of the hypercubic lattice · Percolation event for the origin

Proof usesConfiguration space of a statistical-mechanics model · Connection by an open path · Open cluster of a site · Hypercubic lattice \(\mathbb{Z}^d\) · Open subgraph of a bond configuration · Origin of the hypercubic lattice

Used byFree percolation from domination and free–wired agreement at \(p'\)

B. Free percolation above the critical point

LemmaFree percolation from domination and free–wired agreement at \(p'\)#✓fully proved

If p_c < p', the free measure at p' is dominated by the free measure at p, and θ⁰(p', q) = θ¹(p', q), then θ⁰(p, q) > 0.

lemma frp_free_percolation_above_pc (d : ℕ) {p p' q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (hp' : 0 < p') (hp1' : p' < 1)
    (hpc' : fkPc d q < p')
    (hmono : (freeInfiniteVolume d hp' hp1' hq : Measure (ConfigSpace (Sym2 (Site d))))
        ≼ (freeInfiniteVolume d hp hp1 hq : Measure (ConfigSpace (Sym2 (Site d)))))
    (huniq : fkThetaFree d hp' hp1' hq (q := q) = fkTheta d hp' hp1' hq (q := q)) :
    0 < fkThetaFree d hp hp1 hq (q := q)

Uses 12 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Critical parameter \(p_c(q)\) of the random-cluster model · Wired random-cluster percolation probability \(\theta(p, q)\) · Free percolation probability · Free infinite-volume random-cluster measure · Site of the hypercubic lattice · Stochastic domination of measures on configurations

Proof usesWired percolation above the random-cluster critical point · The percolation event is increasing · Measurability of the percolation event · Percolation event for the origin · Stochastic domination compares real-valued masses

Used byFree percolation above \(p_c\) from monotonicity and countable agreement

LemmaFree percolation above \(p_c\) from monotonicity and countable agreement#✓fully proved

For p > p_c(q, d), the free measure percolates, θ⁰(p, q) > 0, assuming monotonicity of the free measures in p on (p_c, p) (hmono) and θ⁰ = θ¹ off a countable set (hagree).

lemma frp_free_percolation_above_pc_of_countable_agreement
    (d : ℕ) {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (hpc : fkPc d q < p) (bad : Set ℝ) (hbad : bad.Countable)
    (hmono : ∀ {p' : ℝ} (hp' : 0 < p') (hp1' : p' < 1), fkPc d q < p' →
      (freeInfiniteVolume d hp' hp1' hq : Measure (ConfigSpace (Sym2 (Site d))))
        ≼ (freeInfiniteVolume d hp hp1 hq : Measure (ConfigSpace (Sym2 (Site d)))))
    (hagree : ∀ {p' : ℝ} (hp' : 0 < p') (hp1' : p' < 1), fkPc d q < p' →
      p' ∉ bad →
      fkThetaFree d hp' hp1' hq (q := q) = fkTheta d hp' hp1' hq (q := q)) :
    0 < fkThetaFree d hp hp1 hq (q := q)

Uses 8

Statement usesConfiguration space of a statistical-mechanics model · Critical parameter \(p_c(q)\) of the random-cluster model · Wired random-cluster percolation probability \(\theta(p, q)\) · Free percolation probability · Free infinite-volume random-cluster measure · Site of the hypercubic lattice · Stochastic domination of measures on configurations

Proof usesFree percolation from domination and free–wired agreement at \(p'\)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.