Positivity of the random-cluster critical point

29 fully proved

A. Domination of the wired measure by Bernoulli percolation

LemmaMonotonicity of the open subgraph#✓fully proved

The open subgraph is monotone in the configuration.

lemma openGraph_mono {a b : ConfigSpace (Sym2 V)} (h : a ≤ b) :
    openGraph G a ≤ openGraph G b

Uses 2 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Open subgraph of a bond configuration

Used byMonotonicity of the wired graph

LemmaMonotonicity of the wired graph#✓fully proved

The wired graph (open edges plus the boundary clique) is monotone in the configuration.

lemma wiredGraph_mono {a b : ConfigSpace (Sym2 V)} (h : a ≤ b) :
    wiredGraph G bdry a ≤ wiredGraph G bdry b

Uses 5 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Wired open graph

Proof usesMonotonicity of the open subgraph · Complete graph on the boundary vertices · Open subgraph of a bond configuration

Used byWired cluster count is antitone

LemmaWired cluster count is antitone#✓fully proved

The wired cluster count k¹(ω) is antitone in ω.

lemma numClustersWired_antitone {a b : ConfigSpace (Sym2 V)} (h : a ≤ b) :
    numClustersWired G bdry b ≤ numClustersWired G bdry a

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Number of open clusters with wired boundary conditions

Proof usesMonotonicity of the wired graph · Wired open graph

Used byHolley cross inequality for wired and Bernoulli weights, \(q \ge 1\)

LemmaHolley cross inequality for wired and Bernoulli weights, \(q \ge 1\)#✓fully proved

Holley cross inequality between the wired random-cluster weight and the Bernoulli product weight, for q ≥ 1.

lemma wiredFkWeight_edgeProduct_cross {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    (a b : ConfigSpace (Sym2 V)) :
    wiredFkWeight G bdry p q a * edgeProduct G p b
      ≤ wiredFkWeight G bdry p q (a ⊓ b) * edgeProduct G p (a ⊔ b)

Uses 5 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli edge product · Wired random-cluster weight

Proof usesWired cluster count is antitone · Number of open clusters with wired boundary conditions

Used byHolley cross inequality for wired and \(q = 1\) laws, \(q \ge 1\)

LemmaHolley cross inequality for wired and \(q = 1\) laws, \(q \ge 1\)#✓fully proved

Holley cross inequality between the ambient wired probability and the ambient q = 1 law, for q ≥ 1. The latter is Bernoulli-p only on the graph-edge marginal.

lemma wiredFkProb_fkProbOne_cross {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    (a b : ConfigSpace (Sym2 V)) :
    wiredFkProb G bdry p q a * fkProb G p 1 b
      ≤ wiredFkProb G bdry p q (a ⊓ b) * fkProb G p 1 (a ⊔ b)

Uses 12 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Probability of an ambient FK configuration · Wired random-cluster probability of a configuration

Proof usesBernoulli edge product · Unnormalized random-cluster weight · At \(q = 1\) the random-cluster weight is the Bernoulli product · Ambient FK normalizer · Number of open clusters · Wired random-cluster weight · Holley cross inequality for wired and Bernoulli weights, \(q \ge 1\) · Wired random-cluster partition function · Number of open clusters with wired boundary conditions

Used byWired law at most the \(q = 1\) law on increasing events, \(q \ge 1\)

LemmaWired law at most the \(q = 1\) law on increasing events, \(q \ge 1\)#✓fully proved

For q ≥ 1, the ambient wired law is dominated by fkProb G p 1 on increasing events. The latter is Bernoulli-p on graph edges and uniform on loops and nonedges; the comparison with ordinary Bernoulli percolation therefore applies to graph-edge events.

lemma wiredFkProb_le_fkProbOne_increasing {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    {A : Set (ConfigSpace (Sym2 V))} (hA : IsIncreasing A) :
    (∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * wiredFkProb G bdry p q ω)
      ≤ ∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * fkProb G p 1 ω

Uses 13 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Probability of an ambient FK configuration · Wired random-cluster probability of a configuration · Increasing event

Proof usesBernoulli edge product · Unnormalized random-cluster weight · Ambient FK normalizer · Number of open clusters · Holley cross inequality for wired and \(q = 1\) laws, \(q \ge 1\) · Wired random-cluster weight · Wired random-cluster partition function · Number of open clusters with wired boundary conditions · Holley inequality for increasing events

Used byWired \(q = 2\) origin-to-boundary probability at most Bernoulli · Wired box bound \((2dp)^m\) on the open-walk event for \(q \ge 1\)

B. Bernoulli cylinder probabilities

LemmaBoolean-configuration sum of a coordinatewise product factorizes#✓fully proved

Summing a product of single-coordinate factors over all Boolean configurations: coordinates outside s contribute a factor 2 each.

lemma sum_prod_factor {ι : Type*} [Fintype ι] [DecidableEq ι] (s : Finset ι)
    (h : ι → Bool → ℝ) :
    ∑ ω : ι → Bool, ∏ e ∈ s, h e (ω e)
      = 2 ^ (Fintype.card ι - s.card) * ∏ e ∈ s, (∑ b : Bool, h e b)

Used by 2

Used by\(q = 1\) probability of an edge pattern is its Bernoulli weight · Bernoulli probability that edges \(F\) are all open is \(p^{|F|}\)

LemmaBernoulli probability that edges \(F\) are all open is \(p^{|F|}\)#✓fully proved

Under Bernoulli percolation on a finite graph, a set F of edges is open with probability p^|F|.

lemma fkProbOne_cylinder {p : ℝ} (hp : 0 < p) (hp1 : p < 1) (F : Finset (Sym2 V))
    (hF : F ⊆ G.edgeFinset) :
    ∑ ω : ConfigSpace (Sym2 V),
        (if (∀ e ∈ F, ω e = true) then (1 : ℝ) else 0) * fkProb G p 1 ω = p ^ F.card

Uses 8 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Probability of an ambient FK configuration

Proof usesBernoulli edge product · Unnormalized random-cluster weight · At \(q = 1\) the random-cluster weight is the Bernoulli product · Ambient FK normalizer · Number of open clusters · Boolean-configuration sum of a coordinatewise product factorizes

Used byBernoulli bound \(p^m\) for a fixed self-avoiding walk in the box

C. Open self-avoiding walks

DefinitionPadding a finite lattice word to an infinite word#✓fully proved

Extend a word of m lattice steps to an infinite word by a fixed padding step.

def fkExtWord (m : ℕ) (hd : 0 < d) (w : Fin m → Fin d × Bool) : ℕ → Fin d × Bool :=
  fun k => if hk : k < m then w ⟨k, hk⟩ else (⟨0, hd⟩, false)

Used by 5

Used byEvent of an open self-avoiding walk of \(m\) steps · Event of some open self-avoiding walk is clopen · Event of some open self-avoiding walk is increasing · Percolation gives open self-avoiding walks of every length · Wired box bound \((2dp)^m\) on the open-walk event for \(q \ge 1\)

DefinitionEvent of an open self-avoiding walk of \(m\) steps#✓fully proved

The event that some self-avoiding walk of m steps from the origin is open.

def fkExistsOpenWalk (d m : ℕ) (hd : 0 < d) : Set (ConfigSpace (Sym2 (Site d))) :=
  ⋃ (w : Fin m → Fin d × Bool) (_ : goodWord (fkExtWord m hd w) m), wordEvent (fkExtWord m hd w) m

Uses 5 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Padding a finite lattice word to an infinite word · Site of the hypercubic lattice · Self-avoiding initial segment of an encoded lattice path · Event that an encoded lattice path is open

Used byWired percolation bound \(\theta^1(p, q) \le (2dp)^m\) for \(q \ge 1\) · Event of some open self-avoiding walk is clopen · Event of some open self-avoiding walk is increasing · Percolation gives open self-avoiding walks of every length · Wired box bound \((2dp)^m\) on the open-walk event for \(q \ge 1\)

LemmaSingle-edge open event is clopen#✓fully proved

The event that a given edge is open is clopen.

lemma isClopen_singleOpen (e : Sym2 (Site d)) :
    IsClopen {ω : ConfigSpace (Sym2 (Site d)) | ω e = true}

Uses 2 · Used by 1

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

Used byEvent that a given walk is open is clopen

LemmaEvent that a given walk is open is clopen#✓fully proved

The event that a given walk is open is clopen.

lemma isClopen_wordEvent (g : ℕ → Fin d × Bool) (m : ℕ) : IsClopen (wordEvent g m)

Uses 5 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Event that an encoded lattice path is open

Proof usesSingle-edge open event is clopen · Edges of a lattice path encoded by a step sequence

Used byEvent of some open self-avoiding walk is clopen

LemmaEvent that a given walk is open is increasing#✓fully proved

The event that a given walk is open is increasing.

lemma isIncreasing_wordEvent (g : ℕ → Fin d × Bool) (m : ℕ) : IsIncreasing (wordEvent g m)

Uses 5 · Used by 1

Statement usesIncreasing event · Site of the hypercubic lattice · Event that an encoded lattice path is open

Proof usesConfiguration space of a statistical-mechanics model · Edges of a lattice path encoded by a step sequence

Used byEvent of some open self-avoiding walk is increasing

LemmaEvent of some open self-avoiding walk is clopen#✓fully proved

The open-walk event is clopen.

lemma isClopen_fkExistsOpenWalk (m : ℕ) (hd : 0 < d) : IsClopen (fkExistsOpenWalk d m hd)

Uses 7 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Event of an open self-avoiding walk of \(m\) steps · Site of the hypercubic lattice

Proof usesPadding a finite lattice word to an infinite word · Event that a given walk is open is clopen · Self-avoiding initial segment of an encoded lattice path · Event that an encoded lattice path is open

Used byWired percolation bound \(\theta^1(p, q) \le (2dp)^m\) for \(q \ge 1\) · Wired box bound \((2dp)^m\) on the open-walk event for \(q \ge 1\)

LemmaEvent of some open self-avoiding walk is increasing#✓fully proved

The open-walk event is increasing.

lemma isIncreasing_fkExistsOpenWalk (m : ℕ) (hd : 0 < d) :
    IsIncreasing (fkExistsOpenWalk d m hd)

Uses 8 · Used by 1

Statement usesEvent of an open self-avoiding walk of \(m\) steps · Increasing event · Site of the hypercubic lattice

Proof usesConfiguration space of a statistical-mechanics model · Padding a finite lattice word to an infinite word · Event that a given walk is open is increasing · Self-avoiding initial segment of an encoded lattice path · Event that an encoded lattice path is open

Used byWired box bound \((2dp)^m\) on the open-walk event for \(q \ge 1\)

LemmaPercolation gives open self-avoiding walks of every length#✓fully proved

Percolation from the origin implies an open self-avoiding walk of every length m.

lemma percolationEvent_subset_fkExistsOpenWalk (hd : 0 < d) (m : ℕ) :
    percolationEvent d ⊆ fkExistsOpenWalk d m hd

Uses 18 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Event of an open self-avoiding walk of \(m\) steps · Site of the hypercubic lattice · Percolation event for the origin

Proof usesPadding a finite lattice word to an infinite word · Connection by an open path · Box \((-n, n)^d\) in the hypercubic lattice · Open cluster of a site · Hypercubic lattice \(\mathbb{Z}^d\) · Open subgraph of a bond configuration · Shift of a lattice site in one coordinate · Step directions of an open walk from the origin · Edges of a lattice path encoded by a step sequence · Self-avoiding initial segment of an encoded lattice path · Origin of the hypercubic lattice · Sign of a unit lattice step · Vertices of a lattice path encoded by a step sequence · Event that an encoded lattice path is open

Used byWired percolation bound \(\theta^1(p, q) \le (2dp)^m\) for \(q \ge 1\)

D. Bounds on the wired measure of a walk event

LemmaExtended box configuration keeps box edge states#✓fully proved

Extending a box configuration to ℤ^d keeps the state of box edges.

lemma extendEdge_eq_of_range (n : ℕ) (be : Sym2 (boxVerts d n))
    (ω : ConfigSpace (Sym2 (boxVerts d n))) :
    extendEdge d n ω (edgeIncl d n be) = ω be

Uses 6 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Extension of a box configuration by closed edges

Proof usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byOpen self-avoiding walk in a box gives \(m\) distinct open box edges

LemmaOpen edges of an extended box configuration are box edges#✓fully proved

An edge that is open in an extended box configuration is a box edge.

lemma range_of_extendEdge_true (n : ℕ) (ω : ConfigSpace (Sym2 (boxVerts d n)))
    (e : Sym2 (Site d)) (h : extendEdge d n ω e = true) : e ∈ Set.range (edgeIncl d n)

Uses 6 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Extension of a box configuration by closed edges · Site of the hypercubic lattice

Proof usesBox \((-n, n)^d\) in the hypercubic lattice

Used byBernoulli bound \(p^m\) for a fixed self-avoiding walk in the box

LemmaBox edge with a lattice-edge image is a box-graph edge#✓fully proved

A box edge whose image is a lattice edge is an edge of the box graph.

lemma boxEdge_mem (n : ℕ) (be : Sym2 (boxVerts d n)) (x y : Site d)
    (hadj : (hypercubicLattice d).Adj x y) (heq : edgeIncl d n be = s(x, y)) :
    be ∈ (boxGraph d n).edgeFinset

Uses 6 · Used by 1

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Used byOpen self-avoiding walk in a box gives \(m\) distinct open box edges

LemmaOpen self-avoiding walk in a box gives \(m\) distinct open box edges#✓fully proved

An open self-avoiding walk of m steps that lies in the box gives m distinct box edges that are all open.

lemma exists_boxF (n m : ℕ) (g : ℕ → Fin d × Bool) (hg : goodWord g m)
    (hrange : ∀ k ∈ Finset.range m, edgeOf g k ∈ Set.range (edgeIncl d n)) :
    ∃ F : Finset (Sym2 (boxVerts d n)), F ⊆ (boxGraph d n).edgeFinset ∧ F.card = m ∧
      (extendEdge d n ⁻¹' wordEvent g m ⊆ {ω | ∀ be ∈ F, ω be = true})

Uses 16 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Extension of a box configuration by closed edges · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Edges of a lattice path encoded by a step sequence · Self-avoiding initial segment of an encoded lattice path · Event that an encoded lattice path is open

Proof usesBox edge with a lattice-edge image is a box-graph edge · Extended box configuration keeps box edge states · Hypercubic lattice \(\mathbb{Z}^d\) · Shift of a lattice site in one coordinate · Sign of a unit lattice step · Vertices of a lattice path encoded by a step sequence

Used byBernoulli bound \(p^m\) for a fixed self-avoiding walk in the box

LemmaBernoulli bound \(p^m\) for a fixed self-avoiding walk in the box#✓fully proved

Under Bernoulli percolation on the box, a fixed self-avoiding walk of m steps is open with probability at most p^m.

lemma perWord_box_bound (n m : ℕ) (g : ℕ → Fin d × Bool) (hg : goodWord g m)
    {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    ∑ ω : ConfigSpace (Sym2 (boxVerts d n)),
        (extendEdge d n ⁻¹' wordEvent g m).indicator (fun _ => (1 : ℝ)) ω
          * fkProb (boxGraph d n) p 1 ω ≤ p ^ m

Uses 18 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Extension of a box configuration by closed edges · Probability of an ambient FK configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Self-avoiding initial segment of an encoded lattice path · Event that an encoded lattice path is open

Proof usesInclusion of box edges into \(\mathbb{Z}^d\) · Bernoulli edge product · Open self-avoiding walk in a box gives \(m\) distinct open box edges · Bernoulli probability that edges \(F\) are all open is \(p^{|F|}\) · Unnormalized random-cluster weight · Ambient FK normalizer · Number of open clusters · Open edges of an extended box configuration are box edges · Edges of a lattice path encoded by a step sequence

Used byWired box bound \((2dp)^m\) on the open-walk event for \(q \ge 1\)

LemmaWired box measure as a finite sum over box configurations#✓fully proved

The wired box measure of an event, as a finite sum over box configurations.

lemma wiredFiniteMeasure_real_eq (n : ℕ) {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (A : Set (ConfigSpace (Sym2 (Site d)))) (hA : MeasurableSet A) :
    (wiredFiniteMeasure d n hp hp1 hq : Measure (ConfigSpace (Sym2 (Site d)))).real A
      = ∑ ω : ConfigSpace (Sym2 (boxVerts d n)),
          (extendEdge d n ⁻¹' A).indicator (fun _ => (1 : ℝ)) ω
            * wiredFkProb (boxGraph d n) (boxBoundary d n) p q ω

Uses 14 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Vertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Extension of a box configuration by closed edges · Wired random-cluster measure on a box · Wired random-cluster probability of a configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesBernoulli edge product · Wired random-cluster measure as a probability mass function · Wired random-cluster weight · Wired random-cluster partition function · Number of open clusters with wired boundary conditions

Used byWired box bound \((2dp)^m\) on the open-walk event for \(q \ge 1\)

LemmaWired box bound \((2dp)^m\) on the open-walk event for \(q \ge 1\)#✓fully proved

For q ≥ 1, the wired box measure of the open-walk event is at most (2dp)^m.

lemma wiredFiniteMeasure_fkExistsOpenWalk_le (n m : ℕ) (hd : 0 < d) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q) :
    (wiredFiniteMeasure d n hp hp1 (zero_lt_one.trans_le hq)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (fkExistsOpenWalk d m hd)
      ≤ ((2 * d : ℝ) * p) ^ m

Uses 25 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Event of an open self-avoiding walk of \(m\) steps · Wired random-cluster measure on a box · Site of the hypercubic lattice

Proof usesVertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Bernoulli edge product · Extension of a box configuration by closed edges · Padding a finite lattice word to an infinite word · Probability of an ambient FK configuration · Unnormalized random-cluster weight · Ambient FK normalizer · Event of some open self-avoiding walk is clopen · Event of some open self-avoiding walk is increasing · Number of open clusters · Bernoulli bound \(p^m\) for a fixed self-avoiding walk in the box · Wired box measure as a finite sum over box configurations · Wired random-cluster probability of a configuration · Wired law at most the \(q = 1\) law on increasing events, \(q \ge 1\) · Increasing event · Box \((-n, n)^d\) in the hypercubic lattice · Self-avoiding initial segment of an encoded lattice path · Event that an encoded lattice path is open

Used byWired percolation bound \(\theta^1(p, q) \le (2dp)^m\) for \(q \ge 1\)

E. Positivity of the critical point

LemmaWired percolation bound \(\theta^1(p, q) \le (2dp)^m\) for \(q \ge 1\)#✓fully proved

For q ≥ 1, the wired percolation probability satisfies θ¹(p, q) ≤ (2dp)^m for every m.

lemma fkTheta_le_pow (hd : 0 < d) {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q) (m : ℕ) :
    fkTheta d hp hp1 (zero_lt_one.trans_le hq) (q := q) ≤ ((2 * d : ℝ) * p) ^ m

Uses 13 · Used by 1

Statement usesWired random-cluster percolation probability \(\theta(p, q)\)

Proof usesConfiguration space of a statistical-mechanics model · Event of an open self-avoiding walk of \(m\) steps · Event of some open self-avoiding walk is clopen · Percolation gives open self-avoiding walks of every length · Wired random-cluster measure on a box · Wired box bound \((2dp)^m\) on the open-walk event for \(q \ge 1\) · Wired infinite-volume random-cluster measure · Wired infinite-volume measure is a subsequential weak limit · Site of the hypercubic lattice · Percolation event for the origin · Weak convergence of probability measures on configuration space · Portmanteau theorem for clopen events

Used byNo wired percolation for \(2dp < 1\) and \(q \ge 1\)

LemmaNo wired percolation for \(2dp < 1\) and \(q \ge 1\)#✓fully proved

For q ≥ 1 and 2dp < 1, there is no percolation in the wired measure: θ¹(p, q) = 0.

lemma fkTheta_eq_zero_of_lt (hd : 0 < d) {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    (hsmall : (2 * d : ℝ) * p < 1) :
    fkTheta d hp hp1 (zero_lt_one.trans_le hq) (q := q) = 0

Uses 6 · Used by 2

Statement usesWired random-cluster percolation probability \(\theta(p, q)\)

Proof usesConfiguration space of a statistical-mechanics model · Wired percolation bound \(\theta^1(p, q) \le (2dp)^m\) for \(q \ge 1\) · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice · Percolation event for the origin

Used byPositivity of the random-cluster critical point · Nonempty subcritical set on \(\mathbb{Z}^2\) for \(q \ge 1\)

LemmaSubcritical set is bounded above by one#✓fully proved

The set of p with θ¹(p, q) = 0 is bounded above by 1.

lemma fkSubcriticalSet_bddAbove (d : ℕ) (q : ℝ) : BddAbove (fkSubcriticalSet d q)

Uses 2 · Used by 3

Statement usesNon-percolating parameters of the wired random-cluster measure

Proof usesWired random-cluster percolation probability \(\theta(p, q)\)

Used byWired percolation above the random-cluster critical point · Subcritical parameters are at most the critical point · \(p_c(q)\) equals the self-dual point if percolation starts there, \(q \ge 1\)

LemmaSubcritical parameters are at most the critical point#✓fully proved

Every subcritical p is at most p_c(q, d).

lemma le_fkPc_of_mem {d : ℕ} {q p : ℝ} (hp : p ∈ fkSubcriticalSet d q) : p ≤ fkPc d q

Uses 3 · Used by 4

Statement usesCritical parameter \(p_c(q)\) of the random-cluster model · Non-percolating parameters of the wired random-cluster measure

Proof usesSubcritical set is bounded above by one

Used byInf-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 · Positivity of the random-cluster critical point

TheoremPositivity of the random-cluster critical point#✓fully proved

For d ≥ 1 and q ≥ 1, 0 < p_c(q, d); in fact p_c(q, d) ≥ 1 / (4d).

Reference: G. Grimmett, The Random-Cluster Model, Springer (2006), Section 5.1.

theorem fkPc_pos (hd : 0 < d) {q : ℝ} (hq : 1 ≤ q) : 0 < fkPc d q

Uses 5 · Used by 2

Statement usesCritical parameter \(p_c(q)\) of the random-cluster model

Proof usesNon-percolating parameters of the wired random-cluster measure · Wired random-cluster percolation probability \(\theta(p, q)\) · No wired percolation for \(2dp < 1\) and \(q \ge 1\) · Subcritical parameters are at most the critical point

Used byPositive random-cluster critical point for \(d \ge 2\), \(q \ge 1\) · \(p_c(q)\) equals the self-dual point if percolation starts there, \(q \ge 1\)

LemmaPositive random-cluster critical point for \(d \ge 2\), \(q \ge 1\)#✓fully proved

fkPc_pos for d ≥ 2.

lemma fkPc_pos_of_two_le (hd : 2 ≤ d) {q : ℝ} (hq : 1 ≤ q) : 0 < fkPc d q

Uses 2 · Used by 4

Statement usesCritical parameter \(p_c(q)\) of the random-cluster model

Proof usesPositivity of the random-cluster critical point

Used byInf-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 · \(0 < p_c(q) < 1\) on \(\mathbb{Z}^2\) for \(q \ge 1\) under a Peierls bound

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.