Percolation probability and critical point

DefinitionOpen lattice edge of a bond configuration#✓fully proved

The lattice edge {x, y} is open in the configuration ω: x and y are nearest neighbours and ω s(x, y) = true.

def IsOpenEdge (d : ℕ) (ω : ConfigSpace (Sym2 (Site d))) (x y : Site d) : Prop :=
  (hypercubicLattice d).Adj x y ∧ ω s(x, y) = true

Uses 3 · Used by 10

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Used by\(p_c(2) < 1\) from anchored dual-circuit enclosure · Open cluster maps into the lattice minus its boundary edges · Open subgraph of a bond configuration · Duminil-Copin–Tassion differential inequality · Mean-field lower bound · Open boundary edge of a cluster · Exponential decay below p̃_c · Exploration independence of a cluster inside a set · Sharpness of the phase transition · Finite cluster in \(\mathbb{Z}^2\) gives a closed lattice circuit

DefinitionOpen subgraph of a bond configuration#✓fully proved

The open subgraph of ω: the spanning subgraph of ℤ^d consisting of the open edges.

def openSubgraph (d : ℕ) (ω : ConfigSpace (Sym2 (Site d))) : SimpleGraph (Site d) where
  Adj x y := IsOpenEdge d ω x y
  symm := ⟨fun _ _ h => isOpenEdge_symm h⟩
  loopless := ⟨fun x h => isOpenEdge_irrefl x h⟩

Uses 4 · Used by 47

Statement usesConfiguration space of a statistical-mechanics model · Open lattice edge of a bond configuration · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Used byProjection of an induced open subgraph to the lattice · Monotonicity of the open subgraph in the plane · Existence of an open circuit in an annulus · Open circuit lying in an annulus · Measurability of connection inside a set · Step directions of an open walk from the origin · \(p_c(2) < 1\) from anchored dual-circuit enclosure · Positivity of the critical probability (Hammersley's bound) · Plane open connections are open connections in \(\mathbb{Z}^{2+k}\) · Measurability of the one-arm event · Number of infinite clusters is almost surely constant · Translation of the open subgraph as a graph homomorphism · Inverse translation of the open subgraph · Canonical contour of a finite origin cluster · Darts of the canonical contour · Canonical contour is longer than the exit index · Closed face walk of the canonical contour · Open cluster maps into the lattice minus its boundary edges · Discrete Jordan separation for finite open clusters · Exit dart of a finite origin cluster · Exit index of a finite origin cluster · Minimal-period face loop of the exit orbit · Face loop of the exit orbit of a finite cluster · Left exit index of a finite cluster · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle · Lattice clusters agree with general graph clusters · Connection by an open path · Open connection within a set is monotone in the set · Open circuit in a bond configuration · Open subgraph induced on a set of sites · Duminil-Copin–Tassion differential inequality · Mean-field lower bound · Exponential decay below p̃_c · Sharpness of the phase transition · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem · The percolation event is increasing · Percolation gives open self-avoiding walks of every length · Finite cluster in \(\mathbb{Z}^2\) gives a closed lattice circuit · Finite cluster in \(\mathbb{Z}^2\): closed circuit, separated point, odd crossings · Disconnected sites in infinite clusters give two infinite clusters · Open path from the origin out of \(\Lambda_n\) gives \(0 \leftrightarrow \partial\Lambda_n\) inside \(\Lambda_n\) · Open lattice edges between box vertices are open box edges · Open connections in a box are open connections in \(\mathbb{Z}^d\) · Open edges of a box are open edges of \(\mathbb{Z}^d\)

DefinitionConnection by an open path#✓fully proved

x and y are connected by an open path, that is, reachable in openSubgraph d ω.

def Connected (d : ℕ) (ω : ConfigSpace (Sym2 (Site d))) (x y : Site d) : Prop :=
  (openSubgraph d ω).Reachable x y

Uses 3 · Used by 50

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Open subgraph of a bond configuration

Used by\(p_c(2) < 1\) from anchored dual-circuit enclosure · Positivity of the critical probability (Hammersley's bound) · Plane open connections are open connections in \(\mathbb{Z}^{2+k}\) · Percolation in the plane implies percolation in \(\mathbb{Z}^{2+k}\) · Measurability of the one-arm event · Configurations with \(k\) infinite clusters, two merged by opening \(F\) · Number of infinite clusters is almost surely constant · Representative sites of the infinite clusters · Canonical contour of a finite origin cluster · Darts of the canonical contour · Canonical contour is longer than the exit index · Closed face walk of the canonical contour · Discrete Jordan separation for finite open clusters · Exit dart of a finite origin cluster · Exit index of a finite origin cluster · Minimal-period face loop of the exit orbit · Face loop of the exit orbit of a finite cluster · Left exit index of a finite cluster · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle · Open cluster of a site · Lattice clusters agree with general graph clusters · Trifurcation point, without requiring infinite branches · Mean-field lower bound · Exponential decay below p̃_c · One-arm event from the origin · One-arm event from a shifted origin · Exponential decay from a one-step recursion · Sharpness of the phase transition, conditional form · Equality of the Duminil-Copin–Tassion threshold and \(p_c\) · Sharpness of the phase transition · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem · The percolation event is increasing · Measurability of the percolation event · Percolation gives open self-avoiding walks of every length · Finite cluster in \(\mathbb{Z}^2\) gives a closed lattice circuit · Finite cluster in \(\mathbb{Z}^2\): closed circuit, separated point, odd crossings · Wired crossing probabilities converge to the percolation probability · Crossing events intersect to the percolation event · A connection to outside the box passes through the box boundary · Crossing probabilities converge to the percolation probability · Joint percolation at most connectivity given no two infinite clusters · Two-point connectivity of a bond measure on \(\mathbb{Z}^d\) · Uniform decay of two-point connectivity without percolation · Disconnected sites in infinite clusters give two infinite clusters · Boundary connection inside \(\Lambda_n\) reaches outside \(\Lambda_{n-1}\) · Open connections in a box are open connections in \(\mathbb{Z}^d\) · Leaving \(\Lambda_n\) implies connecting to \(\partial\Lambda_n\)

DefinitionOpen cluster of a site#✓fully proved

The open cluster of x: the set of sites connected to x by an open path.

def cluster (d : ℕ) (ω : ConfigSpace (Sym2 (Site d))) (x : Site d) : Set (Site d) :=
  {y | Connected d ω x y}

Uses 3 · Used by 65

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

Used by\(p_c(\mathbb{Z}^2) < 1\) under a no-pinch hypothesis · Open cluster of the origin · Anchored dual-circuit enclosure property · \(p_c(2) < 1\) from anchored dual-circuit enclosure · Positivity of the critical probability (Hammersley's bound) · Percolation in the plane implies percolation in \(\mathbb{Z}^{2+k}\) · Set of infinite open clusters · Configurations with \(k\) infinite clusters, two merged by opening \(F\) · Number of infinite clusters is almost surely constant · Representative sites of the infinite clusters · Existence of an anchored dual cycle around the origin cluster · Canonical contour of a finite origin cluster · Darts of the canonical contour · Canonical contour is longer than the exit index · Closed face walk of the canonical contour · Canonical orbit cycle condition · Primal edges of the canonical contour · Event that every edge of the canonical contour is closed · Open cluster maps into the lattice minus its boundary edges · Dual cycle reaching the left half-plane · Discrete Jordan separation for finite open clusters · Origin cluster's enclosing contour links the two axis exits · Exit dart of a finite origin cluster · Exit dart on the positive horizontal axis · Left and right exit darts lie in the same boundary orbit · Face below the exit edge · Face above the exit edge · Exit index of a finite origin cluster · Minimal-period face loop of the exit orbit · Face loop of the exit orbit of a finite cluster · Axis site lies outside the origin cluster · Inside region of an open cluster in the cut lattice · Exit dart on the negative horizontal axis · Face below the left exit edge · Face above the left exit edge · Left exit index of a finite cluster · Left exit condition at an axis site · Simplicity of the exit orbit's face walk · Anchored dual cycles give the anchored enclosure property · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle · \(p_c(\mathbb{Z}^2) < 1\) via boundary connectivity, assuming linked exits · \(p_c(\mathbb{Z}^2) < 1\) via the canonical contour, assuming anchored cycles · \(p_c(\mathbb{Z}^2) < 1\) via exit dart orbits, assuming linked exits · Lattice clusters agree with general graph clusters · Percolation event for the origin · Trifurcation point, without requiring infinite branches · Mean-field lower bound · Sharpness of the phase transition, conditional form · Equality of the Duminil-Copin–Tassion threshold and \(p_c\) · Sharpness of the phase transition · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem · The percolation event is increasing · Measurability of the percolation event · Percolation gives open self-avoiding walks of every length · Non-percolation means the origin's cluster is finite · Finite cluster in \(\mathbb{Z}^2\) gives a closed lattice circuit · Finite cluster in \(\mathbb{Z}^2\): closed circuit, separated point, odd crossings · Finite cluster in \(\mathbb{Z}^2\) has a reachable point outside it · Finite-cluster event is covered by closed-circuit events · Crossing events intersect to the percolation event · Event that the open cluster of a site is infinite · Disconnected sites in infinite clusters give two infinite clusters

DefinitionOpen subgraph induced on a set of sites#✓fully proved

The open subgraph of ω induced on a set S of sites.

def openSubgraphInduce (d : ℕ) (ω : ConfigSpace (Sym2 (Site d))) (S : Set (Site d)) :
    SimpleGraph S :=
  (openSubgraph d ω).induce S

Uses 3 · Used by 13

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Open subgraph of a bond configuration

Used byOpen vertical crossings separate the sides of a rectangle · Every overlap cluster meets every horizontal crossing · Walk in an induced open subgraph as a lattice walk · Projection of an induced open subgraph to the lattice · Vertical overlap crossings meet every horizontal crossing · RSW gluing from side separation · Measurability of connection inside a set · Connection by an open path within a set · Duminil-Copin–Tassion differential inequality · Mean-field lower bound · Exponential decay below p̃_c · Exploration independence of a cluster inside a set · Sharpness of the phase transition

DefinitionConnection by an open path within a set#✓fully proved

x and y in S are connected by an open path that stays inside S.

def ConnectedWithin (d : ℕ) (ω : ConfigSpace (Sym2 (Site d))) (S : Set (Site d))
    (x y : S) : Prop :=
  (openSubgraphInduce d ω S).Reachable x y

Uses 3 · Used by 32

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Open subgraph induced on a set of sites

Used byOpen vertical crossings separate the sides of a rectangle · Horizontal and vertical crossings meet · Open cluster inside the overlap rectangle · Open connection inside an overlap rectangle · Vertical overlap crossings separate the sides of a rectangle · Vertical overlap crossings meet every horizontal crossing · RSW gluing from side separation · Open left–right crossing of a rectangle at the origin · Open bottom–top crossing of a rectangle at the origin · Open path from the left side of a rectangle to a point · Measurability of the left half-crossing event · Measurability of the right half-crossing event · Open path from a point to the right side of a rectangle · Open left–right crossing of a general rectangle · Measurability of connection inside a set · Measurability of the left–right crossing event · Measurability of the bottom–top crossing event · Open bottom–top crossing of a general rectangle · Open connection within a set is monotone in the set · Box-crossing event · Connection of a site to the box boundary · Duminil-Copin–Tassion differential inequality · Mean-field lower bound · Event of a connection inside a finite set · Open cluster of a site inside a set · Exponential decay below p̃_c · Exploration independence of a cluster inside a set · Crossing inside the box that avoids a cluster · Crossing to the box exterior that avoids a cluster · Sharpness of the phase transition · Positivity of the Duminil-Copin–Tassion threshold · Probability of connection inside a set

TheoremOpen connection within a set is monotone in the set#✓fully proved

Connection inside S implies connection inside any T ⊇ S.

theorem connectedWithin_mono_set (ω : ConfigSpace (Sym2 (Site d)))
    {S T : Set (Site d)} (hST : S ⊆ T) {x y : S}
    (h : ConnectedWithin d ω S x y) :
    ConnectedWithin d ω T ⟨(x : Site d), hST x.2⟩ ⟨(y : Site d), hST y.2⟩

Uses 4 · Used by 4

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

Proof usesOpen subgraph of a bond configuration

Used byRSW gluing from side separation · Duminil-Copin–Tassion differential inequality · Mean-field lower bound · Sharpness of the phase transition

DefinitionOpen circuit in a bond configuration#✓fully proved

A closed walk in the open subgraph that repeats no edge (an open circuit).

def IsOpenCircuit (d : ℕ) (ω : ConfigSpace (Sym2 (Site d))) {x : Site d}
    (w : (openSubgraph d ω).Walk x x) : Prop := w.IsCircuit

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Open subgraph of a bond configuration

Used byOpen circuit lying in an annulus

DefinitionOrigin of the hypercubic lattice#✓fully proved

The origin 0 ∈ ℤ^d.

def origin (d : ℕ) : Site d := fun _ => 0

Uses 1 · Used by 91

Statement usesSite of the hypercubic lattice

Used by\(p_c(\mathbb{Z}^2) < 1\) under a no-pinch hypothesis · Step directions of an open walk from the origin · Positive planar percolation at some \(p < 1\) via the Ising model · Anchored dual-circuit enclosure property · \(p_c(2) < 1\) from anchored dual-circuit enclosure · Positivity of the critical probability (Hammersley's bound) · Percolation in the plane implies percolation in \(\mathbb{Z}^{2+k}\) · Plane embedding fixes the origin · Vertices of a lattice path encoded by a step sequence · Measurability of the one-arm event · Existence of an anchored dual cycle around the origin cluster · Canonical contour of a finite origin cluster · Darts of the canonical contour · Canonical contour is longer than the exit index · Closed face walk of the canonical contour · Canonical orbit cycle condition · Primal edges of the canonical contour · Event that every edge of the canonical contour is closed · Dual cycle reaching the left half-plane · Origin cluster's enclosing contour links the two axis exits · Exit dart of a finite origin cluster · Exit dart on the positive horizontal axis · Left and right exit darts lie in the same boundary orbit · Face below the exit edge · Face above the exit edge · Exit index of a finite origin cluster · Minimal-period face loop of the exit orbit · Face loop of the exit orbit of a finite cluster · Axis site lies outside the origin cluster · Exit dart on the negative horizontal axis · Face below the left exit edge · Face above the left exit edge · Left exit index of a finite cluster · Left exit condition at an axis site · Simplicity of the exit orbit's face walk · Anchored dual cycles give the anchored enclosure property · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle · \(p_c(\mathbb{Z}^2) < 1\) via boundary connectivity, assuming linked exits · \(p_c(\mathbb{Z}^2) < 1\) via the canonical contour, assuming anchored cycles · \(p_c(\mathbb{Z}^2) < 1\) via exit dart orbits, assuming linked exits · Percolation event for the origin · Box-crossing event · Duminil-Copin–Tassion differential inequality · Mean-field lower bound · Exponential decay below p̃_c · One-arm event from the origin · Exponential decay from a one-step recursion · \(\tilde p_c \le p_c\) if \(\theta = 0\) on the set defining \(\tilde p_c\) · Sharpness of the phase transition, conditional form · Equality of the Duminil-Copin–Tassion threshold and \(p_c\) · Exponential decay of the one-arm probability below the threshold · Sharpness of the phase transition · Positivity of the Duminil-Copin–Tassion threshold · Probability of connection inside a set · Densities with a finite set of small Duminil-Copin–Tassion quantity · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · 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 · Spontaneous magnetization of the Ising model · Peierls' theorem · The percolation event is increasing · Measurability of the percolation event · Percolation gives open self-avoiding walks of every length · Non-percolation means the origin's cluster is finite · Finite-volume plus-boundary magnetization at the origin · Origin as a vertex of the box graph · Origin lies in every box · Wired crossing probabilities converge to the percolation probability · Crossing events intersect to the percolation event · A connection to outside the box passes through the box boundary · Crossing probabilities converge to the percolation probability · Uniform decay of two-point connectivity without percolation · Two-point lower bound from FKG, invariance, uniqueness and percolation · Boundary connection inside \(\Lambda_n\) reaches outside \(\Lambda_{n-1}\) · Open path from the origin out of \(\Lambda_n\) gives \(0 \leftrightarrow \partial\Lambda_n\) inside \(\Lambda_n\) · Leaving \(\Lambda_n\) implies connecting to \(\partial\Lambda_n\) · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Simon radius of a finite set · Tail set of plus-state correlations · Window sum of plus-state correlations · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Free origin correlation in a set, extended by zero · Inverse temperatures with an Ising witness \(\varphi_\beta(S) < 1\) · Inverse temperatures with a percolation witness \(\varphi(S) < 1\) · Simon–Lieb inequality in the infinite-volume plus state

DefinitionPercolation event for the origin#✓fully proved

The percolation event {0 ↔ ∞}: the open cluster of the origin is infinite.

def percolationEvent (d : ℕ) : Set (ConfigSpace (Sym2 (Site d))) :=
  {ω | (StatMech.Lattice.cluster d ω (origin d)).Infinite}

Uses 4 · Used by 37

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

Used byAgreement of the two critical probabilities · Agreement of the two percolation events · Wired \(q = 2\) percolation probability at most the Bernoulli one · \(p_c(2) < 1\) from anchored dual-circuit enclosure · Positivity of the critical probability (Hammersley's bound) · Percolation in the plane implies percolation in \(\mathbb{Z}^{2+k}\) · Monotonicity in \(p\) of the Bernoulli percolation probability · \(\theta_2(p) \le \theta_{2+k}(p)\) for Bernoulli percolation · Percolation probability of bond percolation · Mean-field lower bound · Sharpness of the phase transition, conditional form · Equality of the Duminil-Copin–Tassion threshold and \(p_c\) · Sharpness of the phase transition · 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 · Free percolation probability · Free percolation probability is at most one · Nonnegativity of the free percolation probability · Free and wired measures differ at a first-order transition · Wired percolation above the random-cluster critical point · Free percolation from domination and free–wired agreement at \(p'\) · The percolation event is increasing · Measurability of the percolation event · No percolation below the critical point at \(q = 2\) · No wired percolation for \(2dp < 1\) and \(q \ge 1\) · Wired percolation bound \(\theta^1(p, q) \le (2dp)^m\) for \(q \ge 1\) · Percolation gives open self-avoiding walks of every length · Wired random-cluster percolation probability \(\theta(p, q)\) · Non-percolation means the origin's cluster is finite · Wired crossing probabilities converge to the percolation probability · Crossing events intersect to the percolation event · Box-boundary connection probability tends to percolation probability · Crossing probabilities converge to the percolation probability · Uniform decay of two-point connectivity without percolation · Two-point lower bound from FKG, invariance, uniqueness and percolation

DefinitionPercolation probability of bond percolation#✓fully proved

The percolation probability θ_d(p) = ℙ_p(0 ↔ ∞) of Bernoulli bond percolation on ℤ^d with edge density p.

noncomputable def theta (d : ℕ) (p : ℝ≥0) (hp : p ≤ 1) : ℝ :=
  (bernoulliProductMeasure (E := Sym2 (Site d)) p hp).real (percolationEvent d)

Uses 4 · Used by 24

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

Used byAgreement of the two critical probabilities · Positive planar percolation at some \(p < 1\) via the Ising model · Wired \(q = 2\) percolation probability at most the Bernoulli one · Peierls contour bound on the percolation probability · Positive percolation at \(p\) gives \(p_c(d) \le p\) · \(p_c(2) < 1\) from the Peierls contour bound · \(p_c(2) < 1\) from anchored dual-circuit enclosure · Bernoulli critical probability below one for \(d \ge 2\) · Positivity of the critical probability (Hammersley's bound) · Bernoulli critical probability on \(\mathbb{Z}^2\) is below one · Monotonicity in \(p\) of the Bernoulli percolation probability · \(\theta_2(p) \le \theta_{2+k}(p)\) for Bernoulli percolation · Set of densities with no percolation · Mean-field lower bound · Mean-field lower bound for \(\theta(p)\) from a differential inequality · \(p_c \le \tilde p_c\) if \(\theta > 0\) above \(\tilde p_c\) · \(\tilde p_c \le p_c\) if \(\theta = 0\) on the set defining \(\tilde p_c\) · Sharpness of the phase transition, conditional form · Equality of the Duminil-Copin–Tassion threshold and \(p_c\) · Sharpness of the phase transition · 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

DefinitionSet of densities with no percolation#✓fully proved

The set of densities p ∈ [0, 1] at which θ_d(p) = 0.

def subcriticalSet (d : ℕ) : Set ℝ≥0 :=
  {p : ℝ≥0 | ∃ hp : p ≤ 1, theta d p hp = 0}

Uses 1 · Used by 9

Statement usesPercolation probability of bond percolation

Used byAgreement of the two critical probabilities · Positive percolation at \(p\) gives \(p_c(d) \le p\) · \(p_c(2) < 1\) from the Peierls contour bound · \(p_c(2) < 1\) from anchored dual-circuit enclosure · Positivity of the critical probability (Hammersley's bound) · Critical probability of bond percolation on the hypercubic lattice · \(p_c \le \tilde p_c\) if \(\theta > 0\) above \(\tilde p_c\) · \(\tilde p_c \le p_c\) if \(\theta = 0\) on the set defining \(\tilde p_c\) · Equality of the Duminil-Copin–Tassion threshold and \(p_c\)

DefinitionCritical probability of bond percolation on the hypercubic lattice#✓fully proved

The critical probability p_c(d) = sup {p ∈ [0, 1] : θ_d(p) = 0} of bond percolation on ℤ^d.

See also MathlibExt.Probability.ProductBondPercolation.criticalProb, which defines the critical point of a general countable graph through the event that some infinite cluster exists; the two agree for ℤ^d by translation invariance.

noncomputable def pc (d : ℕ) : ℝ≥0 :=
  sSup (subcriticalSet d)

Uses 1 · Used by 20

Statement usesSet of densities with no percolation

Used by\(p_c(\mathbb{Z}^2) < 1\) under a no-pinch hypothesis · Agreement of the two critical probabilities · Positive percolation at \(p\) gives \(p_c(d) \le p\) · \(p_c(2) < 1\) from the Peierls contour bound · \(p_c(2) < 1\) from anchored dual-circuit enclosure · Bernoulli critical probability below one for \(d \ge 2\) · Non-triviality of the percolation critical probability · Positivity of the critical probability (Hammersley's bound) · Bernoulli critical probability on \(\mathbb{Z}^2\) is below one · Nontrivial Bernoulli critical probability on \(\mathbb{Z}^2\) · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle · \(p_c(\mathbb{Z}^2) < 1\) via boundary connectivity, assuming linked exits · \(p_c(\mathbb{Z}^2) < 1\) via the canonical contour, assuming anchored cycles · \(p_c(\mathbb{Z}^2) < 1\) via exit dart orbits, assuming linked exits · \(p_c \le \tilde p_c\) if \(\theta > 0\) above \(\tilde p_c\) · \(\tilde p_c \le p_c\) if \(\theta = 0\) on the set defining \(\tilde p_c\) · Sharpness of the phase transition, conditional form · Equality of the Duminil-Copin–Tassion threshold and \(p_c\) · Sharpness of the phase transition

TheoremLattice clusters agree with general graph clusters#✓fully proved

The open cluster of x in the lattice model is the cluster MathlibExt.Probability.ProductBondPercolation.gcluster of bond percolation on the graph hypercubicLattice d with the same edge configuration.

theorem cluster_eq_gcluster {d : ℕ} (ω : ConfigSpace (Sym2 (Site d))) (x : Site d) :
    StatMech.Lattice.cluster d ω x =
      MathlibExt.Probability.ProductBondPercolation.gcluster (hypercubicLattice d) ω x

Uses 8

Statement usesOpen cluster in a graph · Configuration space of a statistical-mechanics model · Site of the hypercubic lattice · Open cluster of a site · Hypercubic lattice \(\mathbb{Z}^d\)

Proof usesOpen subgraph of a graph · Connection by an open path · Open subgraph of a bond configuration

DefinitionLattice box as a finite set#✓fully proved

The box Λ_n = [-n, n]^d as a finset.

noncomputable def boxFinset (d n : ℕ) : Finset (Site d) := (box_finite d n).toFinset

Uses 2 · Used by 7

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

Used byPairs of sites of a lattice box · Duminil-Copin–Tassion differential inequality · Set of sites not connected to the box boundary · Mean-field lower bound · Box edges with no endpoint in a cluster · Exponential decay below p̃_c · Sharpness of the phase transition

15 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.