Skip to content

Finite- and infinite-volume FK measures on ℤ^d

15 fully proved

A. The wired random-cluster measure on a finite graph

DefinitionWired random-cluster weight#✓fully proved

The unnormalized wired random-cluster weight edgeProduct G p ω · q ^ k¹(ω), where k¹ counts clusters after wiring all boundary vertices together.

noncomputable def wiredFkWeight (p q : ℝ) (ω : ConfigSpace (Sym2 V)) : ℝ :=
  edgeProduct G p ω * q ^ numClustersWired G bdry ω
Uses 3 · Used by 34
Statement usesConfiguration space of a statistical-mechanics model · Bernoulli edge product · Number of open clusters with wired boundary conditions
Used byFK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Continuity in \(t\) of wired \(q = 2\) edge marginals on a finite graph · Free-wired log-normalizer gap \(\le |\partial|\log q/|E|\) for \(q \ge 1\) · Tilted mean of open edges equals the wired FK expectation · Wired and free FK weights within a factor \(q^{|\partial|}\), \(q \ge 1\) · Sandwich \(Z^w \le Z \le q^{|\partial|} Z^w\) for \(q \ge 1\) · Wired partition function at logistic \(p\) as a tilted sum · Wired box measure as a finite sum over box configurations · Holley cross inequality for wired and \(q = 1\) laws, \(q \ge 1\) · Wired law at most the \(q = 1\) law on increasing events, \(q \ge 1\) · Holley cross inequality for wired and Bernoulli weights, \(q \ge 1\) · Boundary clique gives the wired random-cluster measure · Free–wired domination on a finite graph for \(q \ge 1\) · Free box measure dominated by the wired one for \(q \ge 1\) · Holley's condition for free and wired probabilities when \(q \ge 1\) · Holley's condition for free and wired weights when \(q \ge 1\) · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Wired random-cluster measure as a probability mass function · Wired random-cluster probability of a configuration · Wired random-cluster partition function · FKG inequality for the wired measure when \(q \ge 1\) · Closed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Domain Markov property for the wired box measure · Wired random-cluster probabilities are positive · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{n+1}\) at most in \(\Lambda_n\) · Wired \(\Lambda_{n+1}\) measure of a \(\Lambda_n\) cylinder event as a sum · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Wired FK edge marginals are at most one · Nonnegativity of wired FK edge marginals · Boundary-preserving automorphisms preserve the wired FK probability · Boundary-matching isomorphisms preserve wired FK probabilities

DefinitionWired random-cluster partition function#✓fully proved

The wired partition function: the sum of wiredFkWeight over all configurations.

noncomputable def wiredFkZ (p q : ℝ) : ℝ :=
  ∑ ω : ConfigSpace (Sym2 V), wiredFkWeight G bdry p q ω
Uses 2 · Used by 32
Statement usesConfiguration space of a statistical-mechanics model · Wired random-cluster weight
Used byFK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Continuity in \(t\) of wired \(q = 2\) edge marginals on a finite graph · Free-wired log-normalizer gap \(\le |\partial|\log q/|E|\) for \(q \ge 1\) · Wired per-edge ambient tilted log normalizer · Wired tilted log normalizer as a cumulant generating function · Tilted mean of open edges equals the wired FK expectation · Sandwich \(Z^w \le Z \le q^{|\partial|} Z^w\) for \(q \ge 1\) · Wired partition function at logistic \(p\) as a tilted sum · Wired box measure as a finite sum over box configurations · Holley cross inequality for wired and \(q = 1\) laws, \(q \ge 1\) · Wired law at most the \(q = 1\) law on increasing events, \(q \ge 1\) · Boundary clique gives the wired random-cluster measure · Free–wired domination on a finite graph for \(q \ge 1\) · Free box measure dominated by the wired one for \(q \ge 1\) · Holley's condition for free and wired probabilities when \(q \ge 1\) · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Wired random-cluster measure as a probability mass function · Wired random-cluster probability of a configuration · FKG inequality for the wired measure when \(q \ge 1\) · Closed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Domain Markov property for the wired box measure · Wired random-cluster probabilities are positive · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{n+1}\) at most in \(\Lambda_n\) · Wired \(\Lambda_{n+1}\) measure of a \(\Lambda_n\) cylinder event as a sum · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Wired FK edge marginals are at most one · Nonnegativity of wired FK edge marginals · Boundary-preserving automorphisms preserve the wired FK probability · Boundary-matching isomorphisms preserve wired FK probabilities

DefinitionWired random-cluster probability of a configuration#✓fully proved

The wired random-cluster probability of a configuration, wiredFkWeight / wiredFkZ.

noncomputable def wiredFkProb (p q : ℝ) (ω : ConfigSpace (Sym2 V)) : ℝ :=
  wiredFkWeight G bdry p q ω / wiredFkZ G bdry p q
Uses 3 · Used by 95
Statement usesConfiguration space of a statistical-mechanics model · Wired random-cluster weight · Wired random-cluster partition function
Used byWired \(q = 2\) origin-to-boundary probability at most Bernoulli · 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 · Continuity in \(t\) of wired \(q = 2\) edge marginals on a finite graph · Wired \(q = 2\) edge density is monotone in \(t\) · Right-continuity of the wired \(q = 2\) edge density in \(t\) · Average wired edge density as the mean of edge marginals · Tilted mean of open edges equals the wired FK expectation · Expectation under the wired FK measure · Expected wired open-edge count is the sum of edge marginals · Wired box-boundary connection probability is monotone in \(p\) at \(q = 2\) · Wired box bound \((2dp)^m\) on the open-walk event for \(q \ge 1\) · Wired box measure as a finite sum over box configurations · Holley cross inequality for wired and \(q = 1\) laws, \(q \ge 1\) · Wired law at most the \(q = 1\) law on increasing events, \(q \ge 1\) · Boundary clique gives the wired random-cluster measure · Boundary wirings lie between free and wired when \(q \ge 1\) · Free–wired domination on a finite graph for \(q \ge 1\) · Free box measure dominated by the wired one for \(q \ge 1\) · Holley's condition for free and wired probabilities when \(q \ge 1\) · Wirings with the boundary clique dominate the wired measure, \(q \ge 1\) · Wired box measure dominates the induced-wiring measure for \(q \ge 1\) · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Conditional outer wired probability at most the inner wired one, \(q \ge 1\) · Domination by the inner wired measure under a coarser induced wiring · Inner wired domination for vertex sets of \(\mathbb{Z}^d\) · Outer wired all-open probability at most the inner wired one · Inner wired domination of the restricted outer wired measure · Wired random-cluster measure as a probability mass function · FKG inequality for wired \(q = 2\) box measures on smaller-box events · FKG lattice condition for the wired measure when \(q \ge 1\) · FKG inequality for the wired measure when \(q \ge 1\) · Translation covariance of wired box masses · Wired box measure of an all-open event equals its box mass · Difference of wired all-open masses of an edge set and its translate · Wired translation invariance from wired placements of every shift · Equal wired probabilities from eventually equal translated masses · Wired placement for a shift via eventually equal box masses · Closed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Secant bound gives free–wired density agreement off a countable set · Off-centre carrier vanishes by translation covariance · Free density is at most each translated wired marginal · Translated wired marginals converge to the wired density · Equal wired densities from equal translated marginals · Domain Markov property for the wired box measure · Wired \(q = 2\) increasing-event probabilities do not grow with the box · Wired random-cluster probabilities are positive · Conditional wired decrease on inner increasing events for \(q \ge 1\) · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{n+1}\) at most in \(\Lambda_n\) · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{m+1}\) at most in \(\Lambda_m\), \(m \ge n\) · Wired box measures decrease on increasing cylinder events at \(q = 2\) · Wired \(\Lambda_{n+1}\) measure of a \(\Lambda_n\) cylinder event as a sum · Wired box measures decrease on inner increasing events for \(q \ge 1\) · Per-box \(q = 2\) uniqueness off a countable set of tilts · Wired-marginal difference between a box and its translate · Secant bound gives \(q = 2\) edge-event uniqueness off a countable set · Per-box uniqueness of the random-cluster measures off a countable set · Wired unit-edge marginal at \(0\) on \(\Lambda_{\lfloor\sqrt n\rfloor}\) · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Two-sided wired \(q = 2\) bulk bounds from the wired sandwich · Wired \(q = 2\) bulk sandwich from equal wired edge densities · Free off-centre lower bound by the recentred small-box marginal · Wired unit-edge marginals converge to the wired density · Wired unit-edge marginal in the square-root box · Upper bound on wired bulk edge marginals · Wired off-centre sandwich from wired rotation residues · Wired off-centre upper bound by the recentred small-box marginal · Average wired \(q = 2\) edge density of a box as a mean of marginals · Wired FK edge marginals are at most one · Nonnegativity of wired FK edge marginals · Wired \(q = 2\) edge density lies in \((0, 1)\) · Wired uniform bulk deviation at \(q = 2\) · Boundary-preserving automorphisms preserve wired FK edge marginals · Box symmetries preserve the wired \(q = 2\) density of box edges · Boundary-preserving automorphisms preserve the wired FK probability · Translation covariance of FK edge marginals on boxes · Boundary-matching isomorphisms transport FK edge marginals · Boundary-matching isomorphisms preserve wired FK probabilities · Wired off-centre sandwich hypothesis · Wired \(q = 2\) box edge marginals are at least the wired density · Ergodicity of the wired random-cluster measure · Translation invariance of free and wired densities if marginals merge · Constant wired density gives a lower bound on expected open edges · Wired lower bound on expected open edges along a box-symmetry orbit · Equal wired densities from merging wired marginals · Translation invariance of the wired density given merging marginals · Translation invariance of the wired \(q = 2\) infinite-volume measure · Wired box integral of an edge indicator is the wired edge marginal · Wired all-open probability on a translated box · Translated wired box mass equals the centered box mass

DefinitionWired random-cluster measure as a probability mass function#✓fully proved

The wired random-cluster measure on a finite graph, as a probability mass function.

noncomputable def wiredFkPMF {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) :
    PMF (ConfigSpace (Sym2 V)) :=
  PMF.ofFintype (fun ω => ENNReal.ofReal (wiredFkProb G bdry p q ω)) <| by
    rw [← ENNReal.ofReal_sum_of_nonneg fun ω _ => wiredFkProb_nonneg G bdry hp hp1 hq ω,
      wiredFkProb_sum_eq_one G bdry hp hp1 hq]
    simp
Uses 6 · Used by 10
Statement usesConfiguration space of a statistical-mechanics model · Bernoulli edge product · Wired random-cluster probability of a configuration · Wired random-cluster weight · Wired random-cluster partition function · Number of open clusters with wired boundary conditions
Used byFK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Wired box measure as a finite sum over box configurations · Free box measure dominated by the wired one for \(q \ge 1\) · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Wired random-cluster measure on a box · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{n+1}\) at most in \(\Lambda_n\) · Wired \(\Lambda_{n+1}\) measure of a \(\Lambda_n\) cylinder event as a sum · Per-box uniqueness of the random-cluster measures off a countable set

B. Boxes of ℤ^d

AbbreviationVertices of the box \((-n, n)^d\)#✓fully proved

The vertices of the box Λ_n = [-n, n]^d ⊆ ℤ^d, as a subtype.

abbrev boxVerts (d n : ℕ) : Type := {x : Site d // x ∈ box d n}
Uses 2 · Used by 422
Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice
Used byBernoulli box cylinder probability equals its probability on the box · Bernoulli percolation restricted to a box is Bernoulli on the box · Positive planar percolation at some \(p < 1\) via the Ising model · Monotonicity in \(p\) of the Bernoulli percolation probability · Wired \(q = 2\) origin-to-boundary probability at most Bernoulli · 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 · Pointwise convergence of box centered free energies · Free edge densities on a box as left derivatives · Wired edge densities on a box as right derivatives · Wired edge densities on a box bounded by right derivatives · Box-edge marginal uniqueness off a countable set under tilt data · Edge-marginal uniqueness off a countable set from convex free energy · Finite-volume tilt data for a box edge at \(q = 2\) · Collapse of average edge densities to the free density · Infinite-volume edge densities as one-sided derivatives · Convex free-energy hypothesis for a box edge at \(q = 2\) · Convex free energy gives wired density at \(p'\) at most free at \(p > p'\) · Tilt data give wired density at \(p'\) at most free density at \(p > p'\) · Left-continuity of the free \(q = 2\) edge density in \(t\) · Free \(q = 2\) edge density is monotone in \(t\) · Free \(q = 2\) edge density is monotone in \(p\) on \((0, 1)\) · Wired \(q = 2\) edge density is monotone in \(t\) · Right-continuity of the wired \(q = 2\) edge density in \(t\) · Ambient tilted log normalizer ignores the decidability instance · Non-bulk edge fraction bound from a boundary bound on their count · Limits of tilted log normalizers on a fixed box are attained · A limit shared with growing boxes is one fixed-box graph's value · Tilted log normalizers on a fixed box take finitely many values · Average wired density collapse at \(q = 2\) · Wired box-boundary connection probability is monotone in \(p\) at \(q = 2\) · Box edge with a lattice-edge image is a box-graph edge · Open self-avoiding walk in a box gives \(m\) distinct open box edges · Extended box configuration keeps box edge states · Bernoulli bound \(p^m\) for a fixed self-avoiding walk in the box · Open edges of an extended box configuration are box edges · Wired box bound \((2dp)^m\) on the open-walk event for \(q \ge 1\) · Wired box measure as a finite sum over box configurations · Wired probability that the origin reaches the box boundary · Origin as a vertex of the box graph · Box configuration as a coloring of the next larger box · Restriction of a box coloring to the inner box · Box configurations as box-graph colorings with boundary color \(0\) · Free box measure dominated by the wired one for \(q \ge 1\) · Assumed doubling, boundedness and oscillation data along \(K_j\) · Negative log ambient normalizer of a box · Number of edges of a box · Isomorphism of a box with its translated copy in the predicate part · Isomorphism of a box with its translated copy in the complement part · \(\Lambda_n\) has \(d \cdot 2n(2n+1)^{d-1}\) edges · Dyadic convergence data for the ambient tilted log normalizer · Negative log ambient normalizer of the box \(\Lambda_n\) · Edge count of the box \(\Lambda_n\) · Box free-energy doubling bound along \(K_j\) holds for \(d, q \ge 1\) · Doubling bound for the box free energy when \(q \ge 1\) · Van Hove subadditivity of the box free energy for \(q \ge 1\) · Per-edge free energy converges along \(K_j\) for \(d, q \ge 1\) · Edge-normalized box free energy of the random-cluster model · Per-edge box free energy · Van Hove limit · Uniform upper bound on the box free energy for \(d, n, q \ge 1\) · Box free energy \(-\log Z^E\) of the random-cluster model · Box Fekete data from a uniform bound and an oscillation bound · Additive doubling bound for \(-\log Z\) of the free \(q = 2\) FK model · The hyperplane block has at most \(2d|J|\) edges · Orthant blocks have the FK partition function of \(\Lambda_K\) · Vertex degrees in a box are at most \(2d\) · Doubling inequality for \(-\log Z\) of the free \(q = 2\) FK model · Orthant tag of a site of \(\Lambda_{2K+1}\) · Coordinate description of the sites with a given orthant tag · Bound on the edge gap \(|E(\Lambda_{2K+1})| - 2^d |E(\Lambda_K)|\) · \(\Lambda_{2K+1}\) has at least \(2^d\) times as many edges as \(\Lambda_K\) · Lower bound \(n(2n+1)^{d-1}\) on the number of edges of \(\Lambda_n\) · Hyperplane set of \(\Lambda_{2K+1}\) · The hyperplane set has at most \(d(4K+3)^{d-1}\) sites · Hyperplane set lies in the union of the coordinate slabs · Coordinate slab of \(\Lambda_{2K+1}\) · A coordinate slab has at most \((4K+3)^{d-1}\) sites · Translation of \(\Lambda_K\) onto an orthant block of \(\Lambda_{2K+1}\) · The all-tag restriction has the partition function of \(\Lambda_{2K+1}\) · Isomorphism from the all-tag restriction to \(\Lambda_{2K+1}\) · At most \(2d|J|\) edges straddle an orthant tag · An edge leaving an orthant ends on a coordinate hyperplane · An edge between differently tagged sites meets a coordinate hyperplane · Edges straddling a tag are incident to the hyperplane set · Summability of doubling corrections relative to edge counts · Untagged sites are exactly those on a coordinate hyperplane · Wired box measure dominates the induced-wiring measure for \(q \ge 1\) · Domain Markov property for the wired measure on nested boxes · Edge product of a glued configuration factorizes · Component decomposition of the wired glued graph · Component map into the wired glued graph · Wired open graph of a glued configuration · Glued and inner graphs have the same connections on the box · Wiring induced on a box through the outer graph · Induced wiring lies below the inner boundary clique · Inner open graph with the induced wiring · Inner open edges viewed in the larger box · Outer component avoiding the inner box · Wired cluster count of a glued configuration splits additively · Outer open graph plus the outer boundary clique · Outer vertex whose outer component avoids the inner box · Outer components avoiding the inner box · Open edges of an outer configuration outside the inner box · Number of outer components avoiding the inner box · Outer Bernoulli edge factor of an outer configuration · Gluing a box configuration into an outer configuration · Outer weight factor of an outer configuration · Wired glued open graph is the union of inner and outer graphs · Event that the box origin connects to the box boundary · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Event that a box edge is open · Vertex boundary of a box · Nearest-neighbour graph on a box · Inclusion of box edges into \(\mathbb{Z}^d\) · Extension of a box configuration by closed edges · Free random-cluster measure on a box · Wired random-cluster measure on a box · FKG inequality for free \(q = 2\) box measures on smaller-box events · FKG inequality for the free \(q = 2\) infinite-volume measure · FKG inequality for the wired \(q = 2\) infinite-volume measure · Wired \(q = 2\) measure dominates the free one on increasing cylinders · FKG inequality for wired \(q = 2\) box measures on smaller-box events · Convergence and ordering of free and wired limits at \(q = 2\) · Convergence and ordering at \(q = 2\) in subsequence form · Translation covariance of free box masses · Translation covariance of wired box masses · Wired box measure of an all-open event equals its box mass · Wired all-open probabilities converge to the infinite-volume value · Free box measure of an all-open event equals its box mass · Free all-open probabilities converge to the infinite-volume value · Free translation invariance from free placements of every shift · Equal free probabilities from eventually equal translated masses · Free placement for a shift via eventually equal box masses · Difference of wired all-open masses of an edge set and its translate · Wired translation invariance from wired placements of every shift · Equal wired probabilities from eventually equal translated masses · Wired placement for a shift via eventually equal box masses · Closed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Origin-to-\(\partial\Lambda_n\) event as an event on \(\Lambda_{n+1}\) · Conditional free probabilities depend only on the outer configuration · Domain Markov property · Conditional free measure as an induced-wiring measure · Free \(q=2\) box masses of increasing cylinders tend to infinite volume · Free \(q = 2\) box measures are bounded by the limit value · Free \(q = 2\) box measures of increasing cylinders converge · Free \(q = 2\) infinite-volume mass of increasing cylinders as a box limit · One-step growth of free \(q = 2\) measures of increasing cylinders · Free \(q = 2\) box measures of increasing cylinders are monotone · Limit of free \(q = 2\) box measures of a cylinder event · Fibre-mass factorization of random-cluster probabilities · Conditional free measure dominates the smaller free box for \(q \ge 1\) · Free measure is dominated by induced-wiring measures for \(q \ge 1\) · Random-cluster weight of a glued configuration factorizes · Free box measure of a cylinder event as a finite sum · Increasing box events gain free \(q = 2\) probability in the next box · Next-box free measure of a cylinder event as a finite sum · Decomposition of the free measure over the outer configuration · One-step box monotonicity of free measures for \(q \ge 1\) · Cluster decomposition of the glued configuration · Cluster map into the glued configuration · Injectivity of the free cluster map · Cluster map on inner clusters · Cluster map on avoiding outer clusters · Surjectivity of the free cluster map · Open graph of a glued configuration · Glued open edges at outer vertices are outer edges · Inner-graph connections are glued-graph connections · Conditional partition function in terms of the induced wiring · Wiring induced on a box by outer open edges · Adjacency criterion for the free induced wiring · Inner open graph with the free induced wiring · Glued connections between inner vertices are inner-graph connections · Outer open connections give connections in the inner graph · Outer open cluster avoiding the inner box · An outer cluster avoids the inner box iff its representative does · Cluster count of a glued configuration splits additively · Outer open clusters avoiding the inner box · Outer vertex whose outer open cluster avoids the inner box · Avoiding the inner box is constant on outer open clusters · A vertex whose outer cluster avoids the inner box lies outside it · Outer open graph lies in the glued open graph · Glued connections from an avoiding vertex are outer connections · Number of outer open clusters avoiding the inner box · Glued open graph is the union of inner and outer open edges · Outer factor of the weight of a glued configuration · Positivity of the outer weight factor · Fibre masses of the free measure sum to one · Secant bound gives free–wired density agreement off a countable set · Off-centre carrier tends to zero · Off-centre carrier vanishes by translation covariance · Free density is at most each translated wired marginal · Translated wired marginals converge to the wired density · Equal wired densities from equal translated marginals · Number of annulus vertices between consecutive boxes · Inclusion of the annulus wiring into the extra-wired graph · Restriction of a wiring to the annulus vertices · Vertices of the annulus between consecutive boxes · Box as an induced subgraph of the next box · Inclusion of box vertices into the next box · Domain Markov property for the wired box measure · Extended-graph components as inner components plus annulus vertices · Extra-wired components as inner plus annulus-wiring components · Map from inner and annulus-wiring components to extra-wired ones · Map from inner wired components and annulus vertices to components · Extension of a configuration closing the annulus edges · Annulus constant counting the components of an extra wiring · Extended open graph with the inner box boundary wired · Extended wired graph with an extra wiring added · Vertex on the boundary of the inner box · Inclusion of box edges into the next box · Edges of the next box coming from the inner box · Configurations closed off the inner edges as inner-box configurations · Restriction of a next-box configuration to the inner edges · Open graph of a box configuration with the box boundary wired · Inclusion of the wired inner graph into the extended wired graph · Inclusion of the wired inner graph into the extra-wired graph · Wiring with every edge inside the annulus · Vertex of the next box lying in the inner box · Number of next-box edges not coming from the inner box · Wired infinite-volume measure as limit on increasing cylinder events · Wired box probabilities of increasing cylinder events converge · Wired \(q = 2\) increasing-event probabilities do not grow with the box · Infimum of wired box probabilities of a box event · Wired infinite-volume probability equals the infimum over boxes · A connection to outside the box passes through the box boundary · Event that two sites are joined by open edges inside a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Free box measure of a box connection event is the two-point function · Free infinite-volume two-point function in a box · Convergence to the free two-point function under stochastic increase · Cylinder events of a box are clopen · Box restriction pulls increasing events back to increasing events · Cylinder events of a box are measurable · Wired infinite-volume two-point function in a box · Convergence to the wired two-point function under stochastic decrease · Outer projection agrees with the configuration off \(\Lambda_n\) · Boundary connection of \(\Lambda_n\) is a \(\Lambda_m\) cylinder event · Boundary connection inside \(\Lambda_n\) reaches outside \(\Lambda_{n-1}\) · One-step decrease of the events \(0 \leftrightarrow \partial\Lambda_n\) · Open path from the origin out of \(\Lambda_n\) gives \(0 \leftrightarrow \partial\Lambda_n\) inside \(\Lambda_n\) · Inner vertices next to the annulus lie on \(\partial\Lambda_n\) · Open lattice edges between box vertices are open box edges · Restriction of a configuration from \(\Lambda_m\) to \(\Lambda_n\) · Restriction to \(\Lambda_n\) factors through \(\Lambda_m\) · Monotonicity of restriction between boxes · Box inclusion maps the origin to the origin · Inclusion of \(\Lambda_n\) into \(\Lambda_m\) for \(n \le m\) · Conditional wired decrease on inner increasing events for \(q \ge 1\) · Boundary-connection event of \(\Lambda_n\) as an event on \(\Lambda_m\) · Paths to \(\partial\Lambda_{n+1}\) pass through \(\partial\Lambda_n\) · Open connections in a box are open connections in \(\mathbb{Z}^d\) · Leaving \(\Lambda_n\) implies connecting to \(\partial\Lambda_n\) · Edge inclusion into \(\mathbb{Z}^d\) factors through \(\Lambda_m\) · Configurations with a given outer part form its conditioning fibre · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Origin-to-boundary connection is an increasing event · Boundary-connection event of \(\Lambda_n\) on \(\Lambda_m\) is increasing · Cylinder form of the \(\Lambda_n\) boundary connection is measurable · Open edges of \(\Lambda_n\) are open edges of \(\Lambda_{n+1}\) · Open edges of a box are open edges of \(\mathbb{Z}^d\) · Outer part of a configuration on \(\Lambda_{n+1}\) · Outer projection closes the edges of \(\Lambda_n\) · Outer projection keeps the edges outside \(\Lambda_n\) · Outer projection is idempotent · Masses of the conditioning fibres sum to one · Infinite-volume limit of the wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_k\) · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{n+1}\) at most in \(\Lambda_n\) · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{m+1}\) at most in \(\Lambda_m\), \(m \ge n\) · Wired box measures decrease on increasing cylinder events at \(q = 2\) · Wired \(\Lambda_{n+1}\) measure of a \(\Lambda_n\) cylinder event as a sum · Wired \(\Lambda_{n+1}\) measure decomposed over outer configurations · Wired box measures decrease on inner increasing events for \(q \ge 1\) · Wired–free gap in the \(q = 2\) density of a box edge · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Van Hove tiling bound for the edge partition function · Graph isomorphism between a sub-box and a tiling cell · Translation between a sub-box and a tiling cell · Per-edge free energy of a box in the tilt variable · Per-edge negative log edge partition function of a box · Per-box \(q = 2\) uniqueness off a countable set of tilts · Convergence of the per-edge free energy of boxes · Per-edge free energy of boxes converges for \(d \ge 1\) · Restriction of a box to all tiling tags · Sub-box as an induced subgraph of a larger box · Membership of a box vertex in a sub-box · Negative log edge partition function of a box · Tiling cell of a box vertex · Wired-marginal difference between a box and its translate · Secant bound gives \(q = 2\) edge-event uniqueness off a countable set · Convex limit of centered tilt free energies of boxes for \(d, q \ge 1\) · Per-box uniqueness of the random-cluster measures off a countable set · Total deviation of free unit-edge marginals from a free density · Free infinite-volume mass function on a box for \(q \ge 1\) · Free unit-edge marginal at \(0\) on \(\Lambda_{\lfloor\sqrt n\rfloor}\) · Wired unit-edge marginal at \(0\) on \(\Lambda_{\lfloor\sqrt n\rfloor}\) · Total deviation of wired unit-edge marginals from a wired density · Wired infinite-volume mass function on a box for \(q \ge 1\) · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free average edge density collapse on boxes · Free densities of genuine box edges as left derivatives · Wired average edge density collapse on boxes · Wired densities of genuine box edges as right derivatives · Per-coordinate free energy on a box · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Free \(q = 2\) infinite-volume mass function on a box · Homogeneous free-energy data on a box at \(q = 2\) · Wired \(q = 2\) infinite-volume mass function on a box · Two-sided free \(q = 2\) bulk bounds from the free sandwich · Free \(q = 2\) bulk sandwich from equal free edge densities · Two-sided wired \(q = 2\) bulk bounds from the wired sandwich · Wired \(q = 2\) bulk sandwich from equal wired edge densities · Bulk edges of \(\Lambda_n\) · Adjacent box vertices differ by a signed unit vector · Vanishing shell edge fraction when \((n - m(n))/n \to 0\) · Lower bound on free bulk edge marginals · Total deviation of free unit-edge marginals from the density · Free off-centre lower bound by the recentred small-box marginal · Free off-centre sandwich from free rotation residues · Free rotation residue for a box pair · Unit edge \(\{0, \pm e_j\}\) of a box · Free unit-edge marginals converge to the free density · Wired unit-edge marginals converge to the wired density · Free unit-edge marginal in the square-root box · Wired unit-edge marginal in the square-root box · Wired bulk edges of \(\Lambda_n\) · Upper bound on wired bulk edge marginals · Total deviation of wired unit-edge marginals from the density · Wired off-centre sandwich from wired rotation residues · Wired off-centre upper bound by the recentred small-box marginal · Wired rotation residue for a box pair · Box symmetries preserve the free \(q = 2\) density of any pair of sites · All box edges have the same free \(q = 2\) density · Box symmetries preserve the wired \(q = 2\) density of any pair of sites · All box edges have the same wired \(q = 2\) density · Average wired \(q = 2\) edge density of a box as a mean of marginals · Free \(q = 2\) edge density lies in \((0, 1)\) · Free growing-box collapse at \(q = 2\) · Free uniform bulk deviation at \(q = 2\) · Wired \(q = 2\) edge density lies in \((0, 1)\) · Wired uniform bulk deviation at \(q = 2\) · Box symmetries preserve the free \(q = 2\) density of box edges · Box symmetries preserve the wired \(q = 2\) density of box edges · Translation covariance of FK edge marginals on boxes · Translation from the centered box onto a translated box · Restriction of a box symmetry to a box · Translation invariance of the free \(q = 2\) infinite-volume measure · Free off-centre sandwich hypothesis · Free \(q = 2\) box edge marginals are at most the free density · Wired off-centre sandwich hypothesis · Wired \(q = 2\) box edge marginals are at least the wired density · Translate of a vertex of \(\Lambda_N\) as a vertex of \(\Lambda_{N+r}\) · Translate of an edge of \(\Lambda_N\) as an edge of \(\Lambda_{N+r}\) · Ergodicity of the wired random-cluster measure · Event that every edge of a set of box edges is open, on a box · Disjoint-box cap hypothesis for multi-open events · Conditional product cap for multi-open events in boxes · Unordered pair of two sites of a box \(\Lambda_N\) · Translation invariance of free and wired densities if marginals merge · Free edge density is constant on orbits of a box symmetry · Constant free density gives an upper bound on expected open edges · Free upper bound on expected open edges along a box-symmetry orbit · Equal free densities from merging free marginals · Translation invariance of the free density given merging marginals · Wired edge density is constant on orbits of a box symmetry · Constant wired density gives a lower bound on expected open edges · Wired lower bound on expected open edges along a box-symmetry orbit · Equal wired densities from merging wired marginals · Translation invariance of the wired density given merging marginals · Box edge set included into \(\Lambda_m\) and translated by \(v\) · Translation invariance of the wired \(q = 2\) infinite-volume measure · Wired box products approximate infinite-volume products · Every finite family of edge sets is realized in some box · Finite-box product domination from the factorization bound · Realized edge sets stay realized in larger boxes · Upper decorrelation of the wired measure from factorization · Domain monotonicity of wired \(q = 2\) box measures · Domain monotonicity for translated pairs of multi-open events · Disjoint-box factorization bound for box measures · All-open Dirac mass satisfies the factorization bound · Domain monotonicity for edge sets realized in a box · Wired \(q = 2\) measure is ergodic under the factorization bound · Domain monotonicity of wired multi-open probabilities · Free box integral of an edge indicator is the free edge marginal · Wired box integral of an edge indicator is the wired edge marginal · Decay of the edge-indicator functional from equal wired densities · Free translation invariance from the placement hypothesis · Free placement gives shift homogeneity on all-open events · Equal free probabilities for \(t\) and \(v + t\) from matching box limits · Free placement hypothesis for a shift via box-mass limits · Identity shift satisfies the free placement hypothesis · Wired all-open probability on a translated box · Translated wired box mass equals the centered box mass · Translated free box mass of an edge set · Translated free box mass equals the centred box probability · Translated free box masses converge to the free infinite-volume value · Translated wired box masses converge to the infinite-volume mass · Translated box edges are shifted centered box edges · Images of translated edge sets are shifted images · Wired translation invariance from the placement hypothesis · Wired placement gives shift homogeneity on all-open events · Wired shift invariance of an all-open event from matching limits · Wired shift invariance of an all-open event from decaying differences · Wired placement hypothesis for a shift · Identity shift satisfies the wired placement hypothesis · Origin–site covariance in a box · Free-boundary site magnetization in a box · Edge with exactly one endpoint in a cut set · Boundary error of the finite-volume mean-field inequality · Cut mass of a box set rooted at the field ghost · Boundary correlation of an edge crossing a cut · Pairs of a box site and an outside lattice neighbour · Finite-volume mean-field inequality for the Ising model · Origin magnetization with the outer-layer field switched off · Minimal origin-to-site magnetization ratio in a box · Mean-field lower bound for the spontaneous magnetization · Oriented cut mass over cuts \(T \ni 0, x\) with \(y \notin T\) · \(\beta\)-derivative of the origin magnetization in a box

DefinitionNearest-neighbour graph on a box#✓fully proved

The nearest-neighbour graph on the box Λ_n, induced from the hypercubic lattice.

def boxGraph (d n : ℕ) : SimpleGraph (boxVerts d n) :=
  SimpleGraph.comap Subtype.val (hypercubicLattice d)
Uses 4 · Used by 236
Statement usesVertices of the box \((-n, n)^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)
Used byPositive planar percolation at some \(p < 1\) via the Ising model · Monotonicity in \(p\) of the Bernoulli percolation probability · Wired \(q = 2\) origin-to-boundary probability at most Bernoulli · 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 · Pointwise convergence of box centered free energies · Left-continuity of the free \(q = 2\) edge density in \(t\) · Free \(q = 2\) edge density is monotone in \(p\) on \((0, 1)\) · Wired \(q = 2\) edge density is monotone in \(t\) · Right-continuity of the wired \(q = 2\) edge density in \(t\) · Non-bulk edge fraction bound from a boundary bound on their count · A limit shared with growing boxes is one fixed-box graph's value · Average wired density collapse at \(q = 2\) · Wired box-boundary connection probability is monotone in \(p\) at \(q = 2\) · Box edge with a lattice-edge image is a box-graph edge · Open self-avoiding walk in a box gives \(m\) distinct open box edges · Bernoulli bound \(p^m\) for a fixed self-avoiding walk in the box · Wired box bound \((2dp)^m\) on the open-walk event for \(q \ge 1\) · Wired box measure as a finite sum over box configurations · Wired probability that the origin reaches the box boundary · Free box measure dominated by the wired one for \(q \ge 1\) · Assumed doubling, boundedness and oscillation data along \(K_j\) · Negative log ambient normalizer of a box · Number of edges of a box · Isomorphism of a box with its translated copy in the predicate part · Isomorphism of a box with its translated copy in the complement part · \(\Lambda_n\) has \(d \cdot 2n(2n+1)^{d-1}\) edges · Dyadic convergence data for the ambient tilted log normalizer · Negative log ambient normalizer of the box \(\Lambda_n\) · Edge count of the box \(\Lambda_n\) · Box free-energy doubling bound along \(K_j\) holds for \(d, q \ge 1\) · Doubling bound for the box free energy when \(q \ge 1\) · Van Hove subadditivity of the box free energy for \(q \ge 1\) · Per-edge free energy converges along \(K_j\) for \(d, q \ge 1\) · Edge-normalized box free energy of the random-cluster model · Per-edge box free energy · Van Hove limit · Uniform upper bound on the box free energy for \(d, n, q \ge 1\) · Box free energy \(-\log Z^E\) of the random-cluster model · Box Fekete data from a uniform bound and an oscillation bound · Additive doubling bound for \(-\log Z\) of the free \(q = 2\) FK model · The hyperplane block has at most \(2d|J|\) edges · Orthant blocks have the FK partition function of \(\Lambda_K\) · Vertex degrees in a box are at most \(2d\) · Doubling inequality for \(-\log Z\) of the free \(q = 2\) FK model · Bound on the edge gap \(|E(\Lambda_{2K+1})| - 2^d |E(\Lambda_K)|\) · \(\Lambda_{2K+1}\) has at least \(2^d\) times as many edges as \(\Lambda_K\) · Lower bound \(n(2n+1)^{d-1}\) on the number of edges of \(\Lambda_n\) · The all-tag restriction has the partition function of \(\Lambda_{2K+1}\) · Isomorphism from the all-tag restriction to \(\Lambda_{2K+1}\) · At most \(2d|J|\) edges straddle an orthant tag · An edge leaving an orthant ends on a coordinate hyperplane · An edge between differently tagged sites meets a coordinate hyperplane · Edges straddling a tag are incident to the hyperplane set · Summability of doubling corrections relative to edge counts · Wired box measure dominates the induced-wiring measure for \(q \ge 1\) · Domain Markov property for the wired measure on nested boxes · Edge product of a glued configuration factorizes · Component decomposition of the wired glued graph · Component map into the wired glued graph · Glued and inner graphs have the same connections on the box · Induced wiring lies below the inner boundary clique · Inner open graph with the induced wiring · Inner open edges viewed in the larger box · Wired cluster count of a glued configuration splits additively · Open edges of an outer configuration outside the inner box · Outer Bernoulli edge factor of an outer configuration · Wired glued open graph is the union of inner and outer graphs · Event that the box origin connects to the box boundary · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Free random-cluster measure on a box · Wired random-cluster measure on a box · FKG inequality for free \(q = 2\) box measures on smaller-box events · FKG inequality for wired \(q = 2\) box measures on smaller-box events · Translation covariance of free box masses · Translation covariance of wired box masses · Wired box measure of an all-open event equals its box mass · Free box measure of an all-open event equals its box mass · Free translation invariance from free placements of every shift · Equal free probabilities from eventually equal translated masses · Free placement for a shift via eventually equal box masses · Difference of wired all-open masses of an edge set and its translate · Wired translation invariance from wired placements of every shift · Equal wired probabilities from eventually equal translated masses · Wired placement for a shift via eventually equal box masses · Closed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Origin-to-\(\partial\Lambda_n\) event as an event on \(\Lambda_{n+1}\) · Conditional free probabilities depend only on the outer configuration · Domain Markov property · Conditional free measure as an induced-wiring measure · One-step growth of free \(q = 2\) measures of increasing cylinders · Fibre-mass factorization of random-cluster probabilities · Conditional free measure dominates the smaller free box for \(q \ge 1\) · Free measure is dominated by induced-wiring measures for \(q \ge 1\) · Random-cluster weight of a glued configuration factorizes · Free box measure of a cylinder event as a finite sum · Increasing box events gain free \(q = 2\) probability in the next box · Next-box free measure of a cylinder event as a finite sum · Decomposition of the free measure over the outer configuration · One-step box monotonicity of free measures for \(q \ge 1\) · Glued open edges at outer vertices are outer edges · Inner-graph connections are glued-graph connections · Conditional partition function in terms of the induced wiring · Inner open graph with the free induced wiring · Glued connections between inner vertices are inner-graph connections · Outer open connections give connections in the inner graph · Cluster count of a glued configuration splits additively · Glued open graph is the union of inner and outer open edges · Positivity of the outer weight factor · Fibre masses of the free measure sum to one · Secant bound gives free–wired density agreement off a countable set · Off-centre carrier vanishes by translation covariance · Free density is at most each translated wired marginal · Translated wired marginals converge to the wired density · Equal wired densities from equal translated marginals · Inclusion of the annulus wiring into the extra-wired graph · Box as an induced subgraph of the next box · Domain Markov property for the wired box measure · Extended-graph components as inner components plus annulus vertices · Extra-wired components as inner plus annulus-wiring components · Extended open graph with the inner box boundary wired · Open graph of a box configuration with the box boundary wired · Inclusion of the wired inner graph into the extended wired graph · Inclusion of the wired inner graph into the extra-wired graph · Number of next-box edges not coming from the inner box · Wired \(q = 2\) increasing-event probabilities do not grow with the box · A connection to outside the box passes through the box boundary · Event that two sites are joined by open edges inside a box · Free box measure of a box connection event is the two-point function · Convergence to the free two-point function under stochastic increase · Convergence to the wired two-point function under stochastic decrease · Boundary connection of \(\Lambda_n\) is a \(\Lambda_m\) cylinder event · Boundary connection inside \(\Lambda_n\) reaches outside \(\Lambda_{n-1}\) · One-step decrease of the events \(0 \leftrightarrow \partial\Lambda_n\) · Open path from the origin out of \(\Lambda_n\) gives \(0 \leftrightarrow \partial\Lambda_n\) inside \(\Lambda_n\) · Inner vertices next to the annulus lie on \(\partial\Lambda_n\) · Open lattice edges between box vertices are open box edges · Conditional wired decrease on inner increasing events for \(q \ge 1\) · Boundary-connection event of \(\Lambda_n\) as an event on \(\Lambda_m\) · Paths to \(\partial\Lambda_{n+1}\) pass through \(\partial\Lambda_n\) · Open connections in a box are open connections in \(\mathbb{Z}^d\) · Leaving \(\Lambda_n\) implies connecting to \(\partial\Lambda_n\) · Origin-to-boundary connection is an increasing event · Boundary-connection event of \(\Lambda_n\) on \(\Lambda_m\) is increasing · Cylinder form of the \(\Lambda_n\) boundary connection is measurable · Open edges of \(\Lambda_n\) are open edges of \(\Lambda_{n+1}\) · Open edges of a box are open edges of \(\mathbb{Z}^d\) · Masses of the conditioning fibres sum to one · Infinite-volume limit of the wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_k\) · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{n+1}\) at most in \(\Lambda_n\) · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{m+1}\) at most in \(\Lambda_m\), \(m \ge n\) · Wired box measures decrease on increasing cylinder events at \(q = 2\) · Wired \(\Lambda_{n+1}\) measure of a \(\Lambda_n\) cylinder event as a sum · Wired \(\Lambda_{n+1}\) measure decomposed over outer configurations · Wired box measures decrease on inner increasing events for \(q \ge 1\) · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Van Hove tiling bound for the edge partition function · Graph isomorphism between a sub-box and a tiling cell · Per-edge free energy of a box in the tilt variable · Per-edge negative log edge partition function of a box · Per-box \(q = 2\) uniqueness off a countable set of tilts · Convergence of the per-edge free energy of boxes · Per-edge free energy of boxes converges for \(d \ge 1\) · Restriction of a box to all tiling tags · Sub-box as an induced subgraph of a larger box · Negative log edge partition function of a box · Wired-marginal difference between a box and its translate · Secant bound gives \(q = 2\) edge-event uniqueness off a countable set · Convex limit of centered tilt free energies of boxes for \(d, q \ge 1\) · Per-box uniqueness of the random-cluster measures off a countable set · Free unit-edge marginal at \(0\) on \(\Lambda_{\lfloor\sqrt n\rfloor}\) · Wired unit-edge marginal at \(0\) on \(\Lambda_{\lfloor\sqrt n\rfloor}\) · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free average edge density collapse on boxes · Free densities of genuine box edges as left derivatives · Wired average edge density collapse on boxes · Wired densities of genuine box edges as right derivatives · Per-coordinate free energy on a box · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Two-sided free \(q = 2\) bulk bounds from the free sandwich · Free \(q = 2\) bulk sandwich from equal free edge densities · Two-sided wired \(q = 2\) bulk bounds from the wired sandwich · Wired \(q = 2\) bulk sandwich from equal wired edge densities · Bulk edges of \(\Lambda_n\) · Adjacent box vertices differ by a signed unit vector · Vanishing shell edge fraction when \((n - m(n))/n \to 0\) · Lower bound on free bulk edge marginals · Free off-centre lower bound by the recentred small-box marginal · Free off-centre sandwich from free rotation residues · Free rotation residue for a box pair · Free unit-edge marginals converge to the free density · Wired unit-edge marginals converge to the wired density · Free unit-edge marginal in the square-root box · Wired unit-edge marginal in the square-root box · Wired bulk edges of \(\Lambda_n\) · Upper bound on wired bulk edge marginals · Wired off-centre sandwich from wired rotation residues · Wired off-centre upper bound by the recentred small-box marginal · Wired rotation residue for a box pair · All box edges have the same free \(q = 2\) density · All box edges have the same wired \(q = 2\) density · Average wired \(q = 2\) edge density of a box as a mean of marginals · Free \(q = 2\) edge density lies in \((0, 1)\) · Free growing-box collapse at \(q = 2\) · Free uniform bulk deviation at \(q = 2\) · Wired \(q = 2\) edge density lies in \((0, 1)\) · Wired uniform bulk deviation at \(q = 2\) · Box symmetries preserve the free \(q = 2\) density of box edges · Box symmetries preserve the wired \(q = 2\) density of box edges · Translation covariance of FK edge marginals on boxes · Translation invariance of the free \(q = 2\) infinite-volume measure · Free off-centre sandwich hypothesis · Free \(q = 2\) box edge marginals are at most the free density · Wired off-centre sandwich hypothesis · Wired \(q = 2\) box edge marginals are at least the wired density · Ergodicity of the wired random-cluster measure · Disjoint-box cap hypothesis for multi-open events · Conditional product cap for multi-open events in boxes · Translation invariance of free and wired densities if marginals merge · Constant free density gives an upper bound on expected open edges · Free upper bound on expected open edges along a box-symmetry orbit · Equal free densities from merging free marginals · Translation invariance of the free density given merging marginals · Constant wired density gives a lower bound on expected open edges · Wired lower bound on expected open edges along a box-symmetry orbit · Equal wired densities from merging wired marginals · Translation invariance of the wired density given merging marginals · Translation invariance of the wired \(q = 2\) infinite-volume measure · Free box integral of an edge indicator is the free edge marginal · Wired box integral of an edge indicator is the wired edge marginal · Translated wired box mass equals the centered box mass · Translated free box mass equals the centred box probability

DefinitionVertex boundary of a box#✓fully proved

The vertex boundary of the box: sites of Λ_n that are not in Λ_(n-1).

def boxBoundary (d n : ℕ) (x : boxVerts d n) : Prop := (x : Site d) ∈ vertexBoundary d n
Uses 4 · Used by 104
Statement usesVertices of the box \((-n, n)^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Inner vertex boundary of a box
Used byPositive planar percolation at some \(p < 1\) via the Ising model · Monotonicity in \(p\) of the Bernoulli percolation probability · Wired \(q = 2\) origin-to-boundary probability at most Bernoulli · 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 · Wired \(q = 2\) edge density is monotone in \(t\) · Right-continuity of the wired \(q = 2\) edge density in \(t\) · Non-bulk edge fraction bound from a boundary bound on their count · Average wired density collapse at \(q = 2\) · Wired box-boundary connection probability is monotone in \(p\) at \(q = 2\) · Wired box bound \((2dp)^m\) on the open-walk event for \(q \ge 1\) · Wired box measure as a finite sum over box configurations · Wired probability that the origin reaches the box boundary · Box configurations as box-graph colorings with boundary color \(0\) · Free box measure dominated by the wired one for \(q \ge 1\) · Wired box measure dominates the induced-wiring measure for \(q \ge 1\) · Domain Markov property for the wired measure on nested boxes · Induced wiring lies below the inner boundary clique · Wired cluster count of a glued configuration splits additively · Outer open graph plus the outer boundary clique · Wired glued open graph is the union of inner and outer graphs · Event that the box origin connects to the box boundary · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Wired random-cluster measure on a box · FKG inequality for wired \(q = 2\) box measures on smaller-box events · Translation covariance of wired box masses · Wired box measure of an all-open event equals its box mass · Difference of wired all-open masses of an edge set and its translate · Wired translation invariance from wired placements of every shift · Equal wired probabilities from eventually equal translated masses · Wired placement for a shift via eventually equal box masses · Closed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Origin-to-\(\partial\Lambda_n\) event as an event on \(\Lambda_{n+1}\) · Secant bound gives free–wired density agreement off a countable set · Off-centre carrier vanishes by translation covariance · Free density is at most each translated wired marginal · Translated wired marginals converge to the wired density · Equal wired densities from equal translated marginals · Domain Markov property for the wired box measure · Extended-graph components as inner components plus annulus vertices · Extra-wired components as inner plus annulus-wiring components · Open graph of a box configuration with the box boundary wired · Inclusion of the wired inner graph into the extended wired graph · Inclusion of the wired inner graph into the extra-wired graph · Wired \(q = 2\) increasing-event probabilities do not grow with the box · A connection to outside the box passes through the box boundary · Boundary connection of \(\Lambda_n\) is a \(\Lambda_m\) cylinder event · Boundary connection inside \(\Lambda_n\) reaches outside \(\Lambda_{n-1}\) · One-step decrease of the events \(0 \leftrightarrow \partial\Lambda_n\) · Open path from the origin out of \(\Lambda_n\) gives \(0 \leftrightarrow \partial\Lambda_n\) inside \(\Lambda_n\) · Inner vertices next to the annulus lie on \(\partial\Lambda_n\) · Conditional wired decrease on inner increasing events for \(q \ge 1\) · Boundary-connection event of \(\Lambda_n\) as an event on \(\Lambda_m\) · Paths to \(\partial\Lambda_{n+1}\) pass through \(\partial\Lambda_n\) · Leaving \(\Lambda_n\) implies connecting to \(\partial\Lambda_n\) · Origin-to-boundary connection is an increasing event · Boundary-connection event of \(\Lambda_n\) on \(\Lambda_m\) is increasing · Cylinder form of the \(\Lambda_n\) boundary connection is measurable · Masses of the conditioning fibres sum to one · Infinite-volume limit of the wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_k\) · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{n+1}\) at most in \(\Lambda_n\) · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{m+1}\) at most in \(\Lambda_m\), \(m \ge n\) · Wired box measures decrease on increasing cylinder events at \(q = 2\) · Wired \(\Lambda_{n+1}\) measure of a \(\Lambda_n\) cylinder event as a sum · Wired \(\Lambda_{n+1}\) measure decomposed over outer configurations · Wired box measures decrease on inner increasing events for \(q \ge 1\) · Per-box \(q = 2\) uniqueness off a countable set of tilts · Wired-marginal difference between a box and its translate · Secant bound gives \(q = 2\) edge-event uniqueness off a countable set · Per-box uniqueness of the random-cluster measures off a countable set · Wired unit-edge marginal at \(0\) on \(\Lambda_{\lfloor\sqrt n\rfloor}\) · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Wired average edge density collapse on boxes · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Two-sided wired \(q = 2\) bulk bounds from the wired sandwich · Wired \(q = 2\) bulk sandwich from equal wired edge densities · Free off-centre lower bound by the recentred small-box marginal · Wired unit-edge marginals converge to the wired density · Wired unit-edge marginal in the square-root box · Upper bound on wired bulk edge marginals · Wired off-centre sandwich from wired rotation residues · Wired off-centre upper bound by the recentred small-box marginal · Average wired \(q = 2\) edge density of a box as a mean of marginals · Wired \(q = 2\) edge density lies in \((0, 1)\) · Wired uniform bulk deviation at \(q = 2\) · Box symmetries preserve the wired \(q = 2\) density of box edges · Translation covariance of FK edge marginals on boxes · Wired off-centre sandwich hypothesis · Wired \(q = 2\) box edge marginals are at least the wired density · Ergodicity of the wired random-cluster measure · Disjoint-box cap hypothesis for multi-open events · Conditional product cap for multi-open events in boxes · Translation invariance of free and wired densities if marginals merge · Constant wired density gives a lower bound on expected open edges · Wired lower bound on expected open edges along a box-symmetry orbit · Equal wired densities from merging wired marginals · Translation invariance of the wired density given merging marginals · Translation invariance of the wired \(q = 2\) infinite-volume measure · Wired box integral of an edge indicator is the wired edge marginal · Translated wired box mass equals the centered box mass

C. Box measures on the configuration space of ℤ^d

DefinitionInclusion of box edges into \(\mathbb{Z}^d\)#✓fully proved

The inclusion of edges of the box into edges of ℤ^d.

def edgeIncl (d n : ℕ) : Sym2 (boxVerts d n) → Sym2 (Site d) :=
  Sym2.map (Subtype.val : boxVerts d n → Site d)
Uses 3 · Used by 157
Statement usesVertices of the box \((-n, n)^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice
Used byBernoulli box cylinder probability equals its probability on the box · Bernoulli percolation restricted to a box is Bernoulli on the box · Positive planar percolation at some \(p < 1\) via the Ising model · Wired \(q = 2\) origin-to-boundary probability at most Bernoulli · 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 edge densities on a box as left derivatives · Wired edge densities on a box as right derivatives · Wired edge densities on a box bounded by right derivatives · Finite-volume tilt data for a box edge at \(q = 2\) · Collapse of average edge densities to the free density · Infinite-volume edge densities as one-sided derivatives · Convex free-energy hypothesis for a box edge at \(q = 2\) · Convex free energy gives wired density at \(p'\) at most free at \(p > p'\) · Tilt data give wired density at \(p'\) at most free density at \(p > p'\) · Left-continuity of the free \(q = 2\) edge density in \(t\) · Free \(q = 2\) edge density is monotone in \(t\) · Free \(q = 2\) edge density is monotone in \(p\) on \((0, 1)\) · Wired \(q = 2\) edge density is monotone in \(t\) · Right-continuity of the wired \(q = 2\) edge density in \(t\) · Average wired density collapse at \(q = 2\) · Wired box-boundary connection probability is monotone in \(p\) at \(q = 2\) · Box edge with a lattice-edge image is a box-graph edge · Open self-avoiding walk in a box gives \(m\) distinct open box edges · Extended box configuration keeps box edge states · Bernoulli bound \(p^m\) for a fixed self-avoiding walk in the box · Open edges of an extended box configuration are box edges · Wired box bound \((2dp)^m\) on the open-walk event for \(q \ge 1\) · Free box measure dominated by the wired one for \(q \ge 1\) · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Extension of a box configuration by closed edges · FKG inequality for free \(q = 2\) box measures on smaller-box events · FKG inequality for wired \(q = 2\) box measures on smaller-box events · Wired box measure of an all-open event equals its box mass · Wired all-open probabilities converge to the infinite-volume value · Free box measure of an all-open event equals its box mass · Free all-open probabilities converge to the infinite-volume value · Free translation invariance from free placements of every shift · Equal free probabilities from eventually equal translated masses · Free placement for a shift via eventually equal box masses · Wired translation invariance from wired placements of every shift · Equal wired probabilities from eventually equal translated masses · Wired placement for a shift via eventually equal box masses · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · One-step growth of free \(q = 2\) measures of increasing cylinders · Free box measure of a cylinder event as a finite sum · Next-box free measure of a cylinder event as a finite sum · Secant bound gives free–wired density agreement off a countable set · Free density is at most each translated wired marginal · Translated wired marginals converge to the wired density · Equal wired densities from equal translated marginals · Wired \(q = 2\) increasing-event probabilities do not grow with the box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Free box measure of a box connection event is the two-point function · Convergence to the free two-point function under stochastic increase · Cylinder events of a box are clopen · Box restriction pulls increasing events back to increasing events · Convergence to the wired two-point function under stochastic decrease · Open lattice edges between box vertices are open box edges · Restriction to \(\Lambda_n\) factors through \(\Lambda_m\) · Edge inclusion into \(\mathbb{Z}^d\) factors through \(\Lambda_m\) · Cylinder form of the \(\Lambda_n\) boundary connection is measurable · Open edges of \(\Lambda_n\) are open edges of \(\Lambda_{n+1}\) · Open edges of a box are open edges of \(\mathbb{Z}^d\) · Infinite-volume limit of the wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_k\) · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{n+1}\) at most in \(\Lambda_n\) · Wired \(\Lambda_{n+1}\) measure of a \(\Lambda_n\) cylinder event as a sum · Wired–free gap in the \(q = 2\) density of a box edge · Per-box \(q = 2\) uniqueness off a countable set of tilts · Secant bound gives \(q = 2\) edge-event uniqueness off a countable set · Per-box uniqueness of the random-cluster measures off a countable set · Total deviation of free unit-edge marginals from a free density · Total deviation of wired unit-edge marginals from a wired density · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free average edge density collapse on boxes · Free densities of genuine box edges as left derivatives · Wired average edge density collapse on boxes · Wired densities of genuine box edges as right derivatives · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Homogeneous free-energy data on a box at \(q = 2\) · Two-sided free \(q = 2\) bulk bounds from the free sandwich · Free \(q = 2\) bulk sandwich from equal free edge densities · Two-sided wired \(q = 2\) bulk bounds from the wired sandwich · Wired \(q = 2\) bulk sandwich from equal wired edge densities · Lower bound on free bulk edge marginals · Total deviation of free unit-edge marginals from the density · Free off-centre sandwich from free rotation residues · Free rotation residue for a box pair · Free unit-edge marginals converge to the free density · Wired unit-edge marginals converge to the wired density · Upper bound on wired bulk edge marginals · Total deviation of wired unit-edge marginals from the density · Wired off-centre sandwich from wired rotation residues · Wired rotation residue for a box pair · Box symmetries preserve the free \(q = 2\) density of any pair of sites · All box edges have the same free \(q = 2\) density · Box symmetries preserve the wired \(q = 2\) density of any pair of sites · All box edges have the same wired \(q = 2\) density · Free \(q = 2\) edge density lies in \((0, 1)\) · Free growing-box collapse at \(q = 2\) · Free uniform bulk deviation at \(q = 2\) · Wired \(q = 2\) edge density lies in \((0, 1)\) · Wired uniform bulk deviation at \(q = 2\) · Box symmetries preserve the free \(q = 2\) density of box edges · Box symmetries preserve the wired \(q = 2\) density of box edges · Translation invariance of the free \(q = 2\) infinite-volume measure · Free off-centre sandwich hypothesis · Free \(q = 2\) box edge marginals are at most the free density · Wired off-centre sandwich hypothesis · Wired \(q = 2\) box edge marginals are at least the wired density · Ergodicity of the wired random-cluster measure · Disjoint-box cap hypothesis for multi-open events · Free edge density is constant on orbits of a box symmetry · Constant free density gives an upper bound on expected open edges · Free upper bound on expected open edges along a box-symmetry orbit · Equal free densities from merging free marginals · Translation invariance of the free density given merging marginals · Wired edge density is constant on orbits of a box symmetry · Constant wired density gives a lower bound on expected open edges · Wired lower bound on expected open edges along a box-symmetry orbit · Equal wired densities from merging wired marginals · Translation invariance of the wired density given merging marginals · Translation invariance of the wired \(q = 2\) infinite-volume measure · Wired box products approximate infinite-volume products · Every finite family of edge sets is realized in some box · Finite-box product domination from the factorization bound · Realized edge sets stay realized in larger boxes · Upper decorrelation of the wired measure from factorization · Domain monotonicity for translated pairs of multi-open events · Disjoint-box factorization bound for box measures · All-open Dirac mass satisfies the factorization bound · Domain monotonicity for edge sets realized in a box · Wired \(q = 2\) measure is ergodic under the factorization bound · Domain monotonicity of wired multi-open probabilities · Free box integral of an edge indicator is the free edge marginal · Wired box integral of an edge indicator is the wired edge marginal · Decay of the edge-indicator functional from equal wired densities · Free translation invariance from the placement hypothesis · Free placement gives shift homogeneity on all-open events · Equal free probabilities for \(t\) and \(v + t\) from matching box limits · Free placement hypothesis for a shift via box-mass limits · Identity shift satisfies the free placement hypothesis · Translated wired box mass equals the centered box mass · Translated free box mass equals the centred box probability · Translated free box masses converge to the free infinite-volume value · Translated wired box masses converge to the infinite-volume mass · Translated box edges are shifted centered box edges · Images of translated edge sets are shifted images · Wired translation invariance from the placement hypothesis · Wired placement gives shift homogeneity on all-open events · Wired shift invariance of an all-open event from matching limits · Wired shift invariance of an all-open event from decaying differences · Wired placement hypothesis for a shift · Identity shift satisfies the wired placement hypothesis

DefinitionExtension of a box configuration by closed edges#✓fully proved

Extend a configuration on the box to ℤ^d by declaring every edge outside the box closed.

noncomputable def extendEdge (d n : ℕ) (ω : ConfigSpace (Sym2 (boxVerts d n))) :
    ConfigSpace (Sym2 (Site d)) :=
  fun e => if h : e ∈ Set.range (edgeIncl d n) then ω h.choose else false
Uses 5 · Used by 19
Statement usesConfiguration space of a statistical-mechanics model · 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
Used byFK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Open self-avoiding walk in a box gives \(m\) distinct open box edges · Extended box configuration keeps box edge states · Bernoulli bound \(p^m\) for a fixed self-avoiding walk in the box · Open edges of an extended box configuration are box edges · Wired box bound \((2dp)^m\) on the open-walk event for \(q \ge 1\) · Wired box measure as a finite sum over box configurations · Free box measure dominated by the wired one for \(q \ge 1\) · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Free random-cluster measure on a box · Wired random-cluster measure on a box · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Free box measure of a cylinder event as a finite sum · Next-box free measure of a cylinder event as a finite sum · Free box measure of a box connection event is the two-point function · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{n+1}\) at most in \(\Lambda_n\) · Wired \(\Lambda_{n+1}\) measure of a \(\Lambda_n\) cylinder event as a sum · Per-box uniqueness of the random-cluster measures off a countable set

DefinitionFree random-cluster measure on a box#✓fully proved

The free random-cluster measure φ⁰_n on the box Λ_n, pushed to the configuration space of ℤ^d by extendEdge.

noncomputable def freeFiniteMeasure (d n : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) :
    ProbabilityMeasure (ConfigSpace (Sym2 (Site d))) :=
  ⟨((fkPMF (boxGraph d n) hp hp1 hq).toMeasure).map (extendEdge d n),
    inferInstance⟩
Uses 7 · Used by 58
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 · Ambient random-cluster law as a probability mass function · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice
Used byLeft-continuity of the free \(q = 2\) edge density in \(t\) · Free \(q = 2\) edge density is monotone in \(p\) on \((0, 1)\) · Free box measure dominated by the wired one for \(q \ge 1\) · Free infinite-volume random-cluster measure · Free infinite-volume measure is a subsequential weak limit · FKG inequality for free \(q = 2\) box measures on smaller-box events · FKG inequality for the free \(q = 2\) infinite-volume measure · Wired \(q = 2\) measure dominates the free one on increasing cylinders · Convergence and ordering of free and wired limits at \(q = 2\) · Convergence and ordering at \(q = 2\) in subsequence form · Free box measure of an all-open event equals its box mass · Free all-open probabilities converge to the infinite-volume value · Free translation invariance from free placements of every shift · Equal free probabilities from eventually equal translated masses · Common subsequence with free and wired weak limits · Ordered free and wired subsequential limits exist for \(q \ge 1\) · Free limit at most wired limit along a common subsequence, \(q \ge 1\) · Free \(q=2\) box masses of increasing cylinders tend to infinite volume · Free \(q = 2\) box measures are bounded by the limit value · Free \(q = 2\) box measures of increasing cylinders converge · Free \(q = 2\) infinite-volume mass of increasing cylinders as a box limit · One-step growth of free \(q = 2\) measures of increasing cylinders · Free \(q = 2\) box measures of increasing cylinders are monotone · Limit of free \(q = 2\) box measures of a cylinder event · Free box measure of a cylinder event as a finite sum · Free box measures are at most one · Increasing box events gain free \(q = 2\) probability in the next box · Next-box free measure of a cylinder event as a finite sum · Secant bound gives free–wired density agreement off a countable set · Free density is at most each translated wired marginal · Free box measure of a box connection event is the two-point function · Free infinite-volume two-point function in a box · Convergence to the free two-point function under stochastic increase · Per-box \(q = 2\) uniqueness off a countable set of tilts · Secant bound gives \(q = 2\) edge-event uniqueness off a countable set · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Free unit-edge marginals converge to the free density · Free \(q = 2\) edge density lies in \((0, 1)\) · Box symmetries preserve the free \(q = 2\) density of box edges · Translation invariance of the free \(q = 2\) infinite-volume measure · Free \(q = 2\) box edge marginals are at most the free density · Submodule of functions with vanishing free shift decay · Translated free box measure · Constant free density gives an upper bound on expected open edges · Equal free densities from merging free marginals · Cylinder decay along the free box measures · Translation invariance of the free FK measure from cylinder decay · Free box integral of an edge indicator is the free edge marginal · Free shift decay on a dense set of test functions · Free translation invariance from decay on a dense set · Free integral shift decay along a box sequence · Identity shift satisfies the free decay hypothesis · Free translation invariance from integral shift decay · Free translation invariance from the placement hypothesis · Translated free box mass equals the centred box probability · Translated free box masses converge to the free infinite-volume value

DefinitionWired random-cluster measure on a box#✓fully proved

The wired random-cluster measure φ¹_n on the box Λ_n (boundary vertices wired), pushed to the configuration space of ℤ^d by extendEdge.

noncomputable def wiredFiniteMeasure (d n : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) :
    ProbabilityMeasure (ConfigSpace (Sym2 (Site d))) :=
  ⟨((wiredFkPMF (boxGraph d n) (boxBoundary d n) hp hp1 hq).toMeasure).map (extendEdge d n),
    inferInstance⟩
Uses 8 · Used by 88
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 as a probability mass function · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice
Used byWired \(q = 2\) percolation probability at most the Bernoulli one · Wired \(q = 2\) origin-to-boundary probability at most Bernoulli · 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 · Wired \(q = 2\) edge density is monotone in \(t\) · Right-continuity of the wired \(q = 2\) edge density in \(t\) · Wired box-boundary connection probability is monotone in \(p\) at \(q = 2\) · Wired 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\) · Wired box measure as a finite sum over box configurations · Free box measure dominated by the wired one for \(q \ge 1\) · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Wired infinite-volume random-cluster measure · Wired infinite-volume measure is a subsequential weak limit · FKG inequality for the wired \(q = 2\) infinite-volume measure · Wired \(q = 2\) measure dominates the free one on increasing cylinders · FKG inequality for wired \(q = 2\) box measures on smaller-box events · Convergence and ordering of free and wired limits at \(q = 2\) · Convergence and ordering at \(q = 2\) in subsequence form · Wired box measure of an all-open event equals its box mass · Wired all-open probabilities converge to the infinite-volume value · Wired translation invariance from wired placements of every shift · Equal wired probabilities from eventually equal translated masses · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Common subsequence with free and wired weak limits · Ordered free and wired subsequential limits exist for \(q \ge 1\) · Free limit at most wired limit along a common subsequence, \(q \ge 1\) · Secant bound gives free–wired density agreement off a countable set · Free density is at most each translated wired marginal · Translated wired marginals converge to the wired density · Equal wired densities from equal translated marginals · Wired infinite-volume measure as limit on increasing cylinder events · Wired box probabilities of increasing cylinder events converge · Wired \(q = 2\) increasing-event probabilities do not grow with the box · Infimum of wired box probabilities of a box event · Wired infinite-volume probability equals the infimum over boxes · Wired infinite-volume two-point function in a box · Convergence to the wired two-point function under stochastic decrease · Wired \(q = 2\) percolation probability as the limit of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_n\) · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_k\) in \(\Lambda_{k+j}\) is nonincreasing in \(j\) · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_n\) is nonincreasing in \(n\) · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{n+k+1}\) at most in \(\Lambda_{n+k}\) · Infinite-volume limit of the wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_k\) · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{n+1}\) at most in \(\Lambda_n\) · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{m+1}\) at most in \(\Lambda_m\), \(m \ge n\) · Wired box measures decrease on increasing cylinder events at \(q = 2\) · Wired \(\Lambda_{n+1}\) measure of a \(\Lambda_n\) cylinder event as a sum · Per-box \(q = 2\) uniqueness off a countable set of tilts · Secant bound gives \(q = 2\) edge-event uniqueness off a countable set · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Wired unit-edge marginals converge to the wired density · Wired \(q = 2\) edge density lies in \((0, 1)\) · Box symmetries preserve the wired \(q = 2\) density of box edges · Wired \(q = 2\) box edge marginals are at least the wired density · Ergodicity of the wired random-cluster measure · Submodule of functions with vanishing wired shift decay · Disjoint-box cap hypothesis for multi-open events · Translated wired box measure · Conditional product cap for multi-open events in boxes · Constant wired density gives a lower bound on expected open edges · Equal wired densities from merging wired marginals · Translation invariance of the wired \(q = 2\) infinite-volume measure · Wired box products approximate infinite-volume products · Finite-box product domination from the factorization bound · Upper decorrelation of the wired measure from factorization · Domain monotonicity of wired \(q = 2\) box measures · Domain monotonicity for translated pairs of multi-open events · Domain monotonicity for edge sets realized in a box · Wired \(q = 2\) measure is ergodic under the factorization bound · Domain monotonicity of wired multi-open probabilities · Wired box integral of an edge indicator is the wired edge marginal · Decay of the edge-indicator functional from equal wired densities · Cylinder decay along the wired box measures · Translation invariance of the wired FK measure from cylinder decay · Wired shift decay on a dense set of test functions · Wired translation invariance from decay on a dense set · Wired integral shift decay along a box sequence · Identity shift satisfies the wired decay hypothesis · Wired translation invariance from integral shift decay · Translated wired box mass equals the centered box mass · Translated wired box masses converge to the infinite-volume mass · Wired translation invariance from the placement hypothesis · Wired shift invariance of an all-open event from decaying differences

D. Infinite-volume measures

DefinitionFree infinite-volume random-cluster measure#✓fully proved

A free infinite-volume random-cluster measure on ℤ^d: a weak limit of a subsequence of freeFiniteMeasure d n, chosen by Prokhorov compactness.

noncomputable def freeInfiniteVolume (d : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) :
    ProbabilityMeasure (ConfigSpace (Sym2 (Site d))) :=
  (CompactSpace.tendsto_subseq (fun n => freeFiniteMeasure d n hp hp1 hq)).choose
Uses 3 · Used by 50
Statement usesConfiguration space of a statistical-mechanics model · Free random-cluster measure on a box · Site of the hypercubic lattice
Used byBox-edge marginal uniqueness off a countable set under tilt data · Edge-marginal uniqueness off a countable set from convex free energy · Left-continuity of the free \(q = 2\) edge density in \(t\) · Free \(q = 2\) edge density is monotone in \(p\) on \((0, 1)\) · 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 · Free and wired measures differ at self-dual \(p\) for \(q > 4\) if first order · Free and wired measures differ at \(\sqrt{q}/(1+\sqrt{q})\) for \(q > 4\) if first order · Free percolation from domination and free–wired agreement at \(p'\) · Free percolation above \(p_c\) from monotonicity and countable agreement · Free infinite-volume measure is a subsequential weak limit · FKG inequality for the free \(q = 2\) infinite-volume measure · Wired \(q = 2\) measure dominates the free one on increasing cylinders · Convergence and ordering of free and wired limits at \(q = 2\) · Convergence and ordering at \(q = 2\) in subsequence form · Free all-open probabilities converge to the infinite-volume value · Free translation invariance from free placements of every shift · Equal free probabilities from eventually equal translated masses · Free \(q=2\) box masses of increasing cylinders tend to infinite volume · Free \(q = 2\) infinite-volume mass of increasing cylinders as a box limit · Secant bound gives free–wired density agreement off a countable set · Free density is at most each translated wired marginal · Per-box \(q = 2\) uniqueness off a countable set of tilts · Secant bound gives \(q = 2\) edge-event uniqueness off a countable set · Per-box uniqueness of the random-cluster measures off a countable set · Free infinite-volume mass function on a box for \(q \ge 1\) · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free infinite-volume edge density · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Free \(q = 2\) infinite-volume mass function on a box · Free unit-edge marginals converge to the free density · Every lattice edge has the free \(q = 2\) density of \(\{0, e_0\}\) · Free \(q = 2\) edge density lies in \((0, 1)\) · Box symmetries preserve the free \(q = 2\) density of box edges · Translation invariance of the free \(q = 2\) infinite-volume measure · Free \(q = 2\) box edge marginals are at most the free density · Free \(q = 2\) multi-edge homogeneity under a translation · Constant free density gives an upper bound on expected open edges · Equal free densities from merging free marginals · Translation invariance of the free FK measure from cylinder decay · Free translation invariance from decay on a dense set · Free translation invariance from integral shift decay · Free translation invariance from the placement hypothesis · Free placement gives shift homogeneity on all-open events · Equal free probabilities for \(t\) and \(v + t\) from matching box limits · Free placement hypothesis for a shift via box-mass limits · Identity shift satisfies the free placement hypothesis · Translated free box masses converge to the free infinite-volume value

LemmaFree infinite-volume measure is a subsequential weak limit#✓fully proved

freeInfiniteVolume is the weak limit of freeFiniteMeasure along some strictly increasing sequence of box sizes.

lemma freeInfiniteVolume_isLimit (d : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) :
    ∃ φ : ℕ → ℕ, StrictMono φ ∧
      WeakConvergesTo (fun n => freeFiniteMeasure d (φ n) hp hp1 hq)
        (freeInfiniteVolume d hp hp1 hq)
Uses 5 · Used by 3
Statement usesFree random-cluster measure on a box · Free infinite-volume random-cluster measure · Site of the hypercubic lattice · Weak convergence of probability measures on configuration space
Proof usesConfiguration space of a statistical-mechanics model
Used byFree \(q = 2\) infinite-volume mass of increasing cylinders as a box limit · Per-box uniqueness of the random-cluster measures off a countable set · Free translation invariance from integral shift decay

DefinitionWired infinite-volume random-cluster measure#✓fully proved

A wired infinite-volume random-cluster measure on ℤ^d: a weak limit of a subsequence of wiredFiniteMeasure d n, chosen by Prokhorov compactness.

noncomputable def wiredInfiniteVolume (d : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) :
    ProbabilityMeasure (ConfigSpace (Sym2 (Site d))) :=
  (CompactSpace.tendsto_subseq (fun n => wiredFiniteMeasure d n hp hp1 hq)).choose
Uses 3 · Used by 69
Statement usesConfiguration space of a statistical-mechanics model · Wired random-cluster measure on a box · Site of the hypercubic lattice
Used byFK 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 · Box-edge marginal uniqueness off a countable set under tilt data · Edge-marginal uniqueness off a countable set from convex free energy · Wired \(q = 2\) edge density is monotone in \(t\) · Right-continuity of the wired \(q = 2\) edge density in \(t\) · Free and wired measures differ at a first-order transition · Free and wired measures differ at self-dual \(p\) for \(q > 4\) if first order · Free and wired measures differ at \(\sqrt{q}/(1+\sqrt{q})\) for \(q > 4\) if first order · Wired percolation above the random-cluster critical point · No percolation below the critical point at \(q = 2\) · Wired box-boundary connection probability is monotone in \(p\) at \(q = 2\) · Monotonicity of \(\theta^1(p, 2)\) in \(p\) · No wired percolation for \(2dp < 1\) and \(q \ge 1\) · Wired percolation bound \(\theta^1(p, q) \le (2dp)^m\) for \(q \ge 1\) · Wired random-cluster percolation probability \(\theta(p, q)\) · Wired infinite-volume measure is a subsequential weak limit · FKG inequality for the wired \(q = 2\) infinite-volume measure · Wired \(q = 2\) measure dominates the free one on increasing cylinders · Convergence and ordering of free and wired limits at \(q = 2\) · Convergence and ordering at \(q = 2\) in subsequence form · Wired all-open probabilities converge to the infinite-volume value · Wired translation invariance from wired placements of every shift · Equal wired probabilities from eventually equal translated masses · Wired probability that the origin connects to the outside of a box · Wired crossing probabilities converge to the percolation probability · Secant bound gives free–wired density agreement off a countable set · Free density is at most each translated wired marginal · Translated wired marginals converge to the wired density · Equal wired densities from equal translated marginals · Wired infinite-volume measure as limit on increasing cylinder events · Wired infinite-volume probability equals the infimum over boxes · Wired \(q = 2\) percolation probability as the limit of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_n\) · Infinite-volume limit of the wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_k\) · Wired infinite-volume boundary connection tends to \(\theta^1(p, q)\) · Per-box \(q = 2\) uniqueness off a countable set of tilts · Secant bound gives \(q = 2\) edge-event uniqueness off a countable set · Per-box uniqueness of the random-cluster measures off a countable set · Wired infinite-volume mass function on a box for \(q \ge 1\) · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Wired \(q = 2\) infinite-volume mass function on a box · Wired unit-edge marginals converge to the wired density · Every lattice edge has the wired \(q = 2\) density of \(\{0, e_0\}\) · Wired \(q = 2\) edge density lies in \((0, 1)\) · Wired infinite-volume edge density · Box symmetries preserve the wired \(q = 2\) density of box edges · Wired \(q = 2\) box edge marginals are at least the wired density · Ergodicity of the wired random-cluster measure · Wired \(q = 2\) multi-edge homogeneity under a translation · Constant wired density gives a lower bound on expected open edges · Equal wired densities from merging wired marginals · Translation invariance of the wired \(q = 2\) infinite-volume measure · Wired box products approximate infinite-volume products · Upper decorrelation of the wired measure from factorization · Wired \(q = 2\) measure is ergodic under the factorization bound · Decay of the edge-indicator functional from equal wired densities · Translation invariance of the wired FK measure from cylinder decay · Wired translation invariance from decay on a dense set · Wired translation invariance from integral shift decay · Translated wired box masses converge to the infinite-volume mass · Wired translation invariance from the placement hypothesis · Wired placement gives shift homogeneity on all-open events · Wired shift invariance of an all-open event from matching limits · Wired shift invariance of an all-open event from decaying differences · Wired placement hypothesis for a shift · Identity shift satisfies the wired placement hypothesis

LemmaWired infinite-volume measure is a subsequential weak limit#✓fully proved

wiredInfiniteVolume is the weak limit of wiredFiniteMeasure along some strictly increasing sequence of box sizes.

lemma wiredInfiniteVolume_isLimit (d : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) :
    ∃ φ : ℕ → ℕ, StrictMono φ ∧
      WeakConvergesTo (fun n => wiredFiniteMeasure d (φ n) hp hp1 hq)
        (wiredInfiniteVolume d hp hp1 hq)
Uses 5 · Used by 6
Statement usesWired random-cluster measure on a box · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice · Weak convergence of probability measures on configuration space
Proof usesConfiguration space of a statistical-mechanics model
Used byFK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Wired percolation bound \(\theta^1(p, q) \le (2dp)^m\) for \(q \ge 1\) · Wired infinite-volume probability equals the infimum over boxes · Infinite-volume limit of the wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_k\) · Per-box uniqueness of the random-cluster measures off a countable set · Wired translation invariance from integral shift decay

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.