Spin and bond configuration spaces

3 fully proved

Stat Mech

AbbreviationConfiguration space of a statistical-mechanics model#✓fully proved

The configuration space E → Bool of a statistical-mechanics model with sites (or bonds) indexed by E, carrying the product topology and the product σ-algebra.

abbrev ConfigSpace (E : Type*) : Type _ := E → Bool

Used by 1,473

Used byDamped KKL inequality under the \(p\)-biased measure · KKL inequality with constant \(2\) at \(p = 1/2\) · Capped \(p\)-biased per-coordinate estimate in the variable \(u\) · Damped variance equals the variance at \(p = 1/2\) · Noise-damped fiber weight · Hypercontractive bound on the damped fiber weight · Fourier weight of a maximal-element fiber · Log-sum estimate for the fiber weights · Capped estimate with zero weights holds trivially · Capped influence estimate for all \(p\) in \((1/2, q)\) · Capped estimate implies KKL with constant 2 on \((1/2, q)\) · Variance decomposition by maximal element · Fourier total weight equals \(4p(1-p)\) times the total influence · Bound on the high-degree part of the damped total weight · Low-degree case implies the low-range case · Low-degree residual case of the capped estimate · Some truncation level makes the low-degree right side nonnegative · Capped estimate from its low-degree part · Sum of influence powers capped by the maximal influence · Capped per-coordinate hypercontractive estimate · Discrete derivative in a coordinate · Capped-estimate form of KKL implies the indicator-bound form · Bonami–Beckner applied to a discrete derivative · Fourier-form KKL at \(p = 1/2\) conditional on the capped estimate · Conditional Fourier-form KKL holds trivially with constant zero · Summed per-coordinate Bonami–Beckner bound · Bonami–Beckner bound for indicator functions · Fourier-form KKL inequality given the indicator Bonami–Beckner bound · Indicator-bound form of KKL implies the hypercontractive form · Indicator-bound form of KKL with constant 0 holds trivially · Poincaré inequality in Fourier form · Damped influence of a coordinate · Hypercontractive bound on the damped influence · Damped influence is at most the influence · Damped influence at \(\rho = 1\) is the influence · Capped log-sum estimate for damped influences · Log-sum inequality for influences against damped influences · Data-processing inequality for entropy under a two-point mixture · Entropy of a function under a product weight · Conditional entropy in one coordinate · Sub-additivity (tensorization) of entropy · Convexity of the damped total weight · Maximal influence of a Boolean function is at most one · Capped estimate when the maximal influence is at least \(e^{-1}\) · Capped estimate on \((0, 1)\) from concavity of the right side · Small-influence case implies the open-interval case · Small-influence residual case of the capped estimate · Capped estimate in the hypercontractive range with matching \(q'\) · Right side of the capped estimate is nonnegative · Low-range residual case of the capped estimate · Low-range case implies the small-influence case · Capped estimate at \(p = 1/2\) for all \(u \in (0, 1)\) · Target-exponent capped estimate under the gap condition · Target-exponent capped estimate from a domination bound · Damped total weight at \(u = 0\) is at most the total influence · Capped estimate in the hypercontractive range · Capped estimate at the endpoint \(u = 1\) · Damped total weight as a sum of per-coordinate weights · Open-interval case implies the full capped estimate on \((1/2, q)\) · Open-interval residual case of the capped estimate · Per-coordinate damped weight · Fourier-form KKL inequality given the measure–influence bound · Measure–influence form of KKL with constant 0 holds trivially · Edge-isoperimetric inequality · Measure–influence form of KKL implies the indicator-bound form · Bound on \(m - m^{2/(1+\rho^2)}\) by total influence · Squared \(p\)-biased and Walsh coefficients agree at \(p = 1/2\) · \(p\)-biased character at \(p = 1/2\) is the Walsh character up to sign · Total influence at \(p = 1/2\) via \(p\)-biased Fourier coefficients · KKL on the interior of \((1/2, q)\) implies its event form there · Kahn–Kalai–Linial inequality · KKL inequality with constant 2 at \(p\) implies its event form · Pivotal-probability influence as the OSSS influence of an indicator · Logarithm of the reciprocal maximal influence of an event · Event probability as the OSSS expectation of its indicator · Sharp-threshold bound assuming the KKL inequality on \((1/2, q)\) · Sharp-threshold window bound assuming the KKL inequality on \((1/2, q)\) · Variance of an event indicator is \(P(A)(1 - P(A))\) · OSSS Bernoulli weight equals the configuration weight · Capped estimate rewritten in the variable \(u = 1 - \rho^2\) · KKL inequality · KKL inequality with constant 0 holds trivially · Kahn–Kalai–Linial inequality · Kahn–Kalai–Linial inequality · KKL inequality with constant \(c\) for the \(p\)-biased measure · Maximal influence under a product weight · Total influence under a product weight · Coordinatewise complement of a configuration · Reflection of the KKL inequality from \(p\) to \(1 - p\) · Sharp-threshold bound under the \(p\)-biased KKL hypothesis · Sharp-threshold window under the \(p\)-biased KKL hypothesis · Complement swaps the Bernoulli \(p\) and \(1 - p\) weights · Event influence is four times the canonical influence · Influence of a coordinate as Fourier weight · Hypercontractive form of KKL implies the KKL inequality at \(p = 1/2\) · Fourier-form KKL inequality given the hypercontractive bound · Hypercontractive form of KKL with constant 0 holds trivially · Total influence as Fourier weight · Variance as Fourier weight off the empty set · Uniform variance agrees with the canonical Boolean variance · Root step of the OSSS induction · Subtree step of the OSSS induction · Conditional expectation given the other coordinates · Covariance under a product weight · Boolean function computed by a decision tree · Real-valued function computed by a decision tree · Expectation under a product weight · Bernoulli product weight computes product-measure integrals · Configuration with one coordinate flipped · Decision tree querying a list of variables · Decision tree querying every variable · Influence of a coordinate · Influence on an indicator is the pivotal probability · Function depending only on listed coordinates · OSSS inequality · OSSS inequality for the Bernoulli product measure · OSSS covariance inequality over all product weights · Poincaré inequality for Boolean functions under a product measure · Poincaré inequality for the Bernoulli product measure · Covariance form of the Poincaré inequality · Variables queried by a decision tree on an input · Revealment of a variable by a decision tree · Variance under a product weight · Probability of a configuration under a product weight · \(p_c(\mathbb{Z}^2) < 1\) under a no-pinch hypothesis · Open vertical crossings separate the sides of a rectangle · Rotated dual configuration · Capped per-coordinate estimate under the \(p\)-biased measure · \(p\)-biased Fourier coefficient · \(p\)-biased Fourier inversion · Expectations of product functions factor under product measure · \(p\)-biased hypercontractivity on \(\{0, 1\}^n\) · \(p\)-biased influence of a coordinate as Fourier weight · Product noise kernel on the Boolean cube · Conditional \(p\)-biased KKL statement yields KKL with constant \(2\) · \(p\)-biased noise operator via its Markov kernel · Kernel and Fourier noise operators agree · Fourier form of \(p\)-biased hypercontractivity on finite index types · Fourier form of \(p\)-biased hypercontractivity on \(\{0, 1\}^n\) · \(p\)-biased noise operator on the Fourier side · Orthonormality of the \(p\)-biased characters · Parseval's identity under the \(p\)-biased measure · \(p\)-biased character · \(p\)-biased hypercontractivity for a discrete derivative · \(L^q\) norm under the \(p\)-biased measure · \(q\)-th moment under the \(p\)-biased measure · \(p\)-biased KKL inequality conditional on the capped estimate · Trivial KKL inequality with constant \(0\) · Sharp-threshold bound from the conditional KKL statement · Summed per-coordinate \(p\)-biased hypercontractive bound · Tensorization step for \(p\)-biased hypercontractivity · \(p\)-biased total influence as Fourier weight · \(p\)-biased variance as Fourier weight off the empty set · FKG inequality · FKG inequality for increasing events · Holley inequality for increasing events · Holley's coupling theorem · Holley's inequality · Finite measure with prescribed point masses · Normalized point masses give the probability mass function's measure · Harris inequality · Events depending on a coordinate set are closed under unions · Events depending on a coordinate set are closed under intersection · Finitely dependent event is a cylinder over its section · An event depends on the coordinates its indicator depends on · Filling a finite configuration with closed coordinates · Monotonicity of the closed filling map · Positive correlation passes to decreasing intersections · Harris inequality for finitely dependent increasing events · Indicator of an event depends on the coordinates the event depends on · Section of an event on a finite coordinate set · Section of an increasing event is increasing · Complement of an increasing event is decreasing · Complement of a decreasing event is increasing · FKG lattice condition · Indicator of an increasing event is monotone · Intersection of two increasing events is increasing · Decreasing event · Increasing event · Arbitrary intersections of increasing events are increasing · An event is increasing iff its indicator is monotone · Log-modular weights satisfy the FKG lattice condition · Union of two increasing events is increasing · Bernoulli product weight of a configuration · Configuration weight splits at one coordinate · Configuration weight as a product weight · Nonnegativity of the configuration weight · Russo's formula · Bernoulli weight of a single coordinate · Derivative of the configuration weight · Derivative of a single coordinate weight · Derivative of the event weight before grouping · Russo's formula · Pivotal coordinate for an event · Symmetric form of pivotality · Pivotality depends only on the other coordinates · Pivotal coordinates of an increasing event · Closing a coordinate preserves its pivotality · Opening a coordinate preserves its pivotality · Weight of the event that a coordinate is pivotal · Nonnegativity of the pivotal weight · Bernoulli weight of an event · Event weight as a product-weight probability · Contribution of one coordinate to Russo's formula · Russo's formula on a single fiber · Closing a coordinate of a configuration · Closing a coordinate depends only on the other coordinates · Closed configuration lies below the opened one · Closing a coordinate of a split configuration · Opening a coordinate of a configuration · Opening a coordinate depends only on the other coordinates · Opening a coordinate of a split configuration · Product of coordinate weights off one coordinate · Off-coordinate weight depends only on the other coordinates · Agreement of configurations on a set · Agreement on a set under configuration relabeling · Agreement on a set as pointwise equality · Agreement on a set restricts to subsets · Reflexivity of agreement on a set · Symmetry of agreement on a set · Transitivity of agreement on a set · Bernoulli product measure as a weighted probability · BK criterion for Bernoulli product measures · Van den Berg–Kesten inequality · BK inequality for product weights on \(n\) ordered coordinates · BK inequality for product weights on a finite set · Relabeling configurations along a bijection · Configuration relabeling agrees with the library arrow equivalence · Monotonicity of configuration relabeling · Connection event inside a set · Open connection inside a set to a target set · Open connection between two vertices inside a set · Disjoint occurrence of events · Disjoint occurrence is symmetric · Disjoint occurrence of increasing events is increasing · Disjoint occurrence is monotone in both events · Notation for disjoint occurrence · Disjoint occurrence lies in the intersection · Disjoint occurrence on a one-point space is the intersection · Event that an edge is open · Union bound from the three-event BK inequality · Disjoint occurrence preserves finite dependence · BK inequality on countable configuration spaces · Increasing-event probabilities are monotone in the parameter · Occurrence of a finitely dependent event within its window · Section of a disjoint occurrence · BK inequality for three increasing events · Indicator of an event at a prepended configuration · Inhomogeneous Bernoulli product measure · Inhomogeneous Bernoulli product with constant parameter · BK inequality for inhomogeneous Bernoulli measures on a finite set · BK inequality for inhomogeneous measures on a countable set · Membership in a disjoint occurrence · An event occurring on a set contains the configuration · Occurrence is monotone in the coordinate set · Occurrence of an increasing event is monotone in the configuration · Occurrence is monotone in the event · Occurrence of an event on a coordinate set · Occurrence is invariant under relabeling coordinates · Occurrence avoiding the first coordinate passes to the false slice · Occurrence with first coordinate false passes to the false slice · Occurrence with first coordinate true passes to the true slice · Occurrence on a one-point configuration space · Open subgraph of a configuration · Disjoint occurrence commutes with relabeling coordinates · Product weight of a configuration · Product weight factors over the first coordinate · Nonnegativity of the product weight · Product weight is invariant under relabeling coordinates · Slice of an event at the first coordinate · False slice of a disjoint occurrence · True slice of a disjoint occurrence · False slice of an increasing event lies in the true slice · Slices of an increasing event are increasing · Product probability weight has total mass one · Weighted probability of an event · Monotonicity of the weighted probability · Weighted probability by conditioning on the first coordinate · Weighted probability is invariant under relabeling coordinates · Inclusion–exclusion for the weighted probability · Restriction of a doubled configuration to the left copy · Event on the left copy of the doubled ground set · Reimer equality for a left event and a right event · Restriction of a doubled configuration to the right copy · Event on the right copy of the doubled ground set · Weighted disjoint pairs as a doubled-weight probability · Configurations on a finite set as finsets · Support of a configuration as a finset · Event depending only on a set of coordinates · Disjoint occurrence equals intersection for disjoint dependence sets · Down-compression of a family of configurations · Reimer's inequality for events on disjoint coordinate sets · Reimer's inequality on one coordinate · Configuration with a given support · Independence of events on complementary coordinate sets · Event determined by a set of coordinates · Determined-by and depends-on are the same predicate · Reimer equality for events determined by disjoint coordinates · Independence of events determined by disjoint coordinate sets · Event of a family of finsets · Reimer's inequality for two lower families · Reimer's inequality for two upper families · Reimer's inequality · Disjoint occurrence of an increasing and a decreasing event · Reimer's inequality for mixed monotone events, Bernoulli measure · Reimer's inequality for mixed monotone events, product weights · Harris–FKG inequality for an increasing and a decreasing event · Harris–FKG inequality for increasing events · BK inequality for decreasing events · BK inequality for decreasing events under product weights · Flipping every coordinate of a configuration · Coordinate flip as an involutive equivalence · Reimer's inequality for Bernoulli measures, assuming the core case · Reimer's inequality · Reimer's inequality for product weights, assuming the core case · Reimer's inequality on the one-point configuration space · Event that two coordinates agree · Event that two coordinates differ · Negatively correlated events · Reimer's inequality for disjoint events · Reimer's inequality for negatively correlated events · Reimer's inequality for the XOR and XNOR events · Slice inequalities in the one-coordinate BK induction step · Monotone coupling of two measures · Set of coordinatewise ordered configuration pairs · Strassen's theorem, easy direction · Existence of a monotone coupling implies stochastic domination · Marginals of a coupling have equal total mass · Stochastic domination compares real-valued masses · Stochastic domination is reflexive · Stochastic domination of measures on configurations · Stochastic domination is transitive · Strassen's theorem · Measure on ordered pairs from a mass vector · Horizontal and vertical crossings meet · Open cluster inside the overlap rectangle · Every overlap cluster meets every horizontal crossing · Walk in an induced open subgraph as a lattice walk · Projection of an induced open subgraph to the lattice · Infimum of the box-crossing probabilities · Set of long-direction box-crossing probabilities · Box-crossing property with a given aspect ratio · Agreement of the two critical probabilities · Open cluster of the origin · Event that the origin's cluster is infinite · Agreement of the two percolation events · Percolation probability as an extended real · Positively associated measure · Positive association for probability measures is the Harris–FKG inequality · Harris–FKG inequality for a positively associated probability measure · Translate of a bond configuration · Left–right crossing event of a translated rectangle · Bottom–top crossing event of a translated rectangle · Gluing horizontal crossings through a vertical overlap crossing · Measurability of the overlap connection event · Open connection inside an overlap rectangle · Connection event inside an overlap rectangle · Square-root trick · Vertical overlap crossings separate the sides of a rectangle · Vertical overlap crossings meet every horizontal crossing · RSW gluing from side separation · Open left–right crossing of a rectangle at the origin · Left–right crossing event of a rectangle at the origin · Monotonicity of the open subgraph in the plane · Open bottom–top crossing of a rectangle at the origin · Bottom–top crossing event of a rectangle at the origin · Open path from the left side of a rectangle to a point · Left half-crossing event · Measurability of the left half-crossing event · Measurability of the right half-crossing event · Open path from a point to the right side of a rectangle · Right half-crossing event · Existence of an open circuit in an annulus · Open circuit event in an annulus · Open circuit in an annulus centered at the origin · Left–right crossing event of a box with given aspect ratio · Dual left–right crossing of a rectangle · Dual left–right crossing event · Dual bottom–top crossing of a rectangle · Dual bottom–top crossing event · Open left–right crossing of a general rectangle · Left–right crossing event of a general rectangle · Open circuit lying in an annulus · Measurability of connection inside a set · Measurability of the left–right crossing event · Measurability of the bottom–top crossing event · Box-crossing property for a sequence of measures · Uniform two-sided box-crossing property · Open bottom–top crossing of a general rectangle · Bottom–top crossing event of a general rectangle · Critical bond percolation measure on the square lattice · Russo–Seymour–Welsh theorem · Russo–Seymour–Welsh theorem · Left region of a rectangle cut by an open cluster · Condition that every left-right crossing meets the open cluster · Rectangle lattice with an open cluster removed · Sites reachable from the left side of a rectangle · Bernoulli box cylinder probability equals its probability on the box · Bernoulli percolation restricted to a box is Bernoulli on the box · Bernoulli product pulled back along an injection is Bernoulli · Bernoulli percolation restricted to the plane is planar Bernoulli · Event that a dual circuit is closed · Connection to the boundary depends only on graph edges · Step directions of an open walk from the origin · Positive planar percolation at some \(p < 1\) via the Ising model · \(q = 1\) measure equals Bernoulli percolation on graph-edge events · \(q = 1\) probability of an edge pattern is its Bernoulli weight · Wired \(q = 2\) percolation probability at most the Bernoulli one · Anchored dual-circuit enclosure property · \(p_c(2) < 1\) from anchored dual-circuit enclosure · Positivity of the critical probability (Hammersley's bound) · Plane open connections are open connections in \(\mathbb{Z}^{2+k}\) · Percolation in the plane implies percolation in \(\mathbb{Z}^{2+k}\) · Restriction of a configuration to the embedded plane · Monotonicity in \(p\) of the Bernoulli percolation probability · \(\theta_2(p) \le \theta_{2+k}(p)\) for Bernoulli percolation · Wired \(q = 2\) origin-to-boundary probability at most Bernoulli · Event that an encoded lattice path is open · Event of at least two infinite open clusters · Shift-invariant countably valued functions are a.s. constant under ergodicity · Configuration with a finite edge set forced open · Finite energy for opening finite edge sets · Set of infinite open clusters · Measurability of the one-arm event · Configurations with \(k\) infinite clusters, two merged by opening \(F\) · Number of infinite open clusters · Number of infinite clusters is almost surely constant · Zero or one infinite cluster, given ergodicity and \(\mu(N \ge 2) = 0\) · Representative sites of the infinite clusters · Translation of the open subgraph as a graph homomorphism · Inverse translation of the open subgraph · Existence of an anchored dual cycle around the origin cluster · Canonical contour of a finite origin cluster · Darts of the canonical contour · Canonical contour is longer than the exit index · Closed face walk of the canonical contour · Canonical orbit cycle condition · Primal edges of the canonical contour · Event that every edge of the canonical contour is closed · Open cluster maps into the lattice minus its boundary edges · Dual cycle reaching the left half-plane · Discrete Jordan separation for finite open clusters · Origin cluster's enclosing contour links the two axis exits · Exit dart of a finite origin cluster · Exit dart on the positive horizontal axis · Left and right exit darts lie in the same boundary orbit · Face below the exit edge · Face above the exit edge · Exit index of a finite origin cluster · Minimal-period face loop of the exit orbit · Face loop of the exit orbit of a finite cluster · Axis site lies outside the origin cluster · Inside region of an open cluster in the cut lattice · Exit dart on the negative horizontal axis · Face below the left exit edge · Face above the left exit edge · Left exit index of a finite cluster · Left exit condition at an axis site · Simplicity of the exit orbit's face walk · Anchored dual cycles give the anchored enclosure property · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle · \(p_c(\mathbb{Z}^2) < 1\) via boundary connectivity, assuming linked exits · \(p_c(\mathbb{Z}^2) < 1\) via the canonical contour, assuming anchored cycles · \(p_c(\mathbb{Z}^2) < 1\) via exit dart orbits, assuming linked exits · Open cluster of a site · Lattice clusters agree with general graph clusters · Connection by an open path · Connection by an open path within a set · Open connection within a set is monotone in the set · Open circuit in a bond configuration · Open lattice edge of a bond configuration · Open subgraph of a bond configuration · Open subgraph induced on a set of sites · Percolation event for the origin · Percolation probability of bond percolation · Influence of an edge on an event · Sharp threshold from a KKL-type influence inequality · Event that an edge is open · Russo's formula · Sharp threshold from influences · Burton–Keane theorem · Trifurcation point, without requiring infinite branches · Configuration with all edges at a site closed · Number of trifurcation points in a box · Aizenman–Barsky inequality on a finite graph · Configurations with an edge closed and pivotal · Sites connected to \(o\) with ghost edges closed · Closing all ghost edges · Closing all ghost edges but one · Merging configurations on and off a set · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Infinite-volume percolation magnetization · Bond percolation measure on the ghost graph · Product weight of a configuration · Edge weight under an inhomogeneous product measure · Pivotal probability of an edge · Probability under an inhomogeneous product measure · Edges used by an open walk in an induced subgraph · Transfer of an open walk between agreeing configurations · Transfer of an open walk avoiding a fixed edge · Product weight of a configuration off one edge · Box-crossing probability · Box-crossing event · Connection of a site to the box boundary · Box-crossing probability as a polynomial in the density · Duminil-Copin–Tassion differential inequality · Vertices not connected to a target set · Event that a vertex is connected to a target set · Mean-field differential inequality for inhomogeneous percolation · Event that an edge is closed and pivotal · Event that the set of vertices not connected to \(B\) is \(S\) · Product of the edge laws over all other edges · Pivotal edge event · Event that the unconnected set equals a given set · Set of sites not connected to the box boundary · Mean-field lower bound · Event of a connection inside a finite set · Translation invariance of the Bernoulli product measure · Open boundary edge of a cluster · Event that the cluster of the origin inside a set equals a given set · Open cluster of a site inside a set · One-arm probability · Exponential decay below p̃_c · One-arm event from the origin · One-arm event from a shifted origin · Exploration independence of a cluster inside a set · Crossing inside the box that avoids a cluster · Crossing to the box exterior that avoids a cluster · Exponential decay from a one-step recursion · Product weight of an edge configuration · Expectation under Bernoulli product weights · Russo's formula · Probability of an event under Bernoulli product measure · Real-valued indicator that an edge is open · Russo's formula · Russo's formula for the Bernoulli product measure · Russo's formula · Sharpness of the phase transition, conditional form · Equality of the Duminil-Copin–Tassion threshold and \(p_c\) · Sharpness of the phase transition · Positivity of the Duminil-Copin–Tassion threshold · Probability of connection inside a set · Mass of a configuration under a finite Bernoulli product measure · Bernoulli product measure on configuration space · Bernoulli product measure of a cylinder event · Bernoulli product measure on bonds is the bond percolation law · Russo's formula · Differentiability in \(p\) of the probability of a cylinder event · Events depending on finitely many coordinates are cylinders · Configuration patched from one configuration on a finite set and another off it · Bernoulli product measure of an event on a finite index set · Russo's formula · Finite projections of increasing events are increasing · Probability of an event as a sum of configuration masses · Bernoulli product measure of a cylinder event, real-valued form · Probability of a finitely dependent event as a polynomial in \(p\) · Probability of a finitely dependent event as a finite weight · Mass of a configuration under a finite Bernoulli product measure, real form · Mass of a configuration on a finite index set is its product weight · Log-modularity of Bernoulli product weights · Nonnegativity of configuration masses · Configuration masses sum to one · Conditional distribution given the outside of a region · Outside conditional distribution is a version of the conditional probability · Disintegration in product form for the outside conditional distribution · Averaging the outside conditional distribution recovers the measure · σ-algebra of the configuration outside a region · Outside σ-algebra is a sub-σ-algebra of the product σ-algebra · Coordinate projection of a configuration · Product σ-algebra on configuration space is generated by the coordinates · Bernoulli zero-one law for infinite groups acting finite-to-one · Independence of coordinates under the Bernoulli product measure · Ergodicity of Bernoulli measures under free infinite-group actions · Ergodic measure on configuration space · Translation-invariant measure on configuration space · Shift of a configuration by a group element · Configuration shift is the action on functions · Increasing-event probabilities along a decreasing chain are antitone · Stochastic domination from below passes to weak limits · Probability measures agreeing on clopen sets are equal · Weak limit of a decreasing chain is dominated by its terms · Subsequential weak limits are determined by clopen-event limits · Weak limit of an increasing chain dominates its terms · Lower bounds on clopen-event probabilities pass to weak limits · Increasing-event probabilities along an increasing chain are monotone · Upper bounds on clopen-event probabilities pass to weak limits · Weak convergence implies convergence of integrals · Convergence of increasing-event probabilities along an increasing chain · Portmanteau theorem for clopen events · Convergence on clopen events implies weak convergence · Weak convergence of probability measures on configuration space · Convergence of integrals implies weak convergence · Stochastic domination from above passes to weak limits · Griffiths' second inequality for two distinct spins · Field derivative of the magnetization as a sum of covariances · Three-replica variable \(d_w\) · Third Ursell function of the finite Ising model · Global spin flip · Global spin flip as an involutive equivalence · Lebowitz four-point combination · Field derivative of the two-point covariance · GHS gap on an edge equals the third Ursell function · Griffiths–Hurst–Sherman inequality · Set of sites where an agreement configuration is true · Agreement configuration of two spin configurations · Law of the agreement configuration of two replicas · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Conditional two-replica expectation given the agreement · Total two-replica weight of an agreement fibre · Fibre weight integrated against an observable · Conditional expectation of \(t_y\) given the agreement · Conditional expectation of \(u_o u_x\) given the agreement · Two-replica weight in an agreement fibre · Mate of a configuration over an agreement pattern · Field weight of the disagreement set · Splitting a configuration along the agreement set · Completion of agreement-set spins to a full configuration · Expectation with field on the agreement set · Agreement-set Boltzmann weight with doubled couplings and field · Completion of disagreement-set spins to a full configuration · Zero-field expectation on the disagreement set · Zero-field disagreement-set Boltzmann weight · Change of variables from replica pairs to agreement and first copy · GHS concavity of the magnetization in the field · Three-site duplicated-variable factor · Griffiths–Hurst–Sherman inequality · Susceptibility bound \(\chi(h) \le m(h)/h \le 1/h\) from concavity · GHS susceptibility bound \(\chi \le 1/h\) · Inhomogeneous law of the agreement configuration · Spin covariance in the inhomogeneous model · Directional spin sum · Covariance with the directional spin · Two-replica expectation with inhomogeneous couplings · Inhomogeneous conditional expectation given the agreement · Inhomogeneous total weight of an agreement fibre · Inhomogeneous fibre weight integrated against an observable · Inhomogeneous conditional expectation of \(t_y\) · Inhomogeneous conditional expectation of \(u_o u_x\) · Inhomogeneous two-replica weight in an agreement fibre · GHS concavity · Inhomogeneous field weight of the disagreement set · Inhomogeneous expectation with field on the agreement set · Inhomogeneous agreement-set Boltzmann weight · Inhomogeneous zero-field expectation on the disagreement set · Griffiths–Hurst–Sherman inequality · Third Ursell function of the inhomogeneous Ising model · Inhomogeneous zero-field disagreement-set weight · Fibre factorization property for \(u_o u_x\) and \(t_y\) · Configuration merged from two configurations along a set · Splitting a configuration into a set and its complement · Two-replica Ising expectation · Three-replica Ising expectation · Magnetization vanishes at zero field · Susceptibility bound \(\chi(h) \le m(h)/h\) from concavity · Total spin of a configuration · Rotated two-replica sum variable \(t_w\) · Rotated two-replica difference variable \(u_w\) · Monotonicity of correlations · Ginibre's duplicated-variable change of variables · Duplicated-variable involution on configuration pairs · Energy observable of the Ising model · Gibbs expectation with inhomogeneous couplings and site fields · First Griffiths inequality (GKS I) · Nonnegativity of the GKS positivity kernel · Second Griffiths inequality (GKS II) · Griffiths' second inequality for inhomogeneous couplings · Griffiths monotonicity of correlations in the edge set · Being a spin monomial · Finite-volume Ising expectation · Boltzmann weight as a product of cosh-plus-sinh factors · Spin monomial with given exponents · Spin product over a vertex set · Configuration sum of a spin monomial is nonnegative · Unnormalized second Griffiths inequality · Boltzmann weight with inhomogeneous couplings and site fields · Pointwise product of two configurations · Partition function with inhomogeneous couplings and site fields · FKG inequality · Edges cut by a spin configuration · Edges cut by a configuration via the edge disagreement test · Proportionality of the cut sum and the dual even-subgraph sum · Cut space of a graph · Cut space defined through Boolean cut edges · Edge crossing from region-bounding dual walks and a walk decomposition · Edge crossing from closed-walk parities and walk decompositions · Edge crossing from cycle-parity compatibility of even subgraphs · Edge crossing from side colourings of dual walks · Spin disagreement test across an edge · High-temperature expansion · Kramers–Wannier duality · Kramers–Wannier duality · Self-dual edge crossing of K₄ by complementary edges · Spin configuration from crossing parities along walks · Number of disagreeing steps along a walk · Onsager's formula from the spin Kac-Ward identities · Onsager's formula · Increasing clopen events · Convexity of the set of DLR states · Existence of infinite-volume states · Free-boundary Ising measure in a box · Infinite-volume free state as a subsequential weak limit · Box energy with a boundary condition · Finite-volume Gibbs measure on configurations of \(\mathbb{Z}^d\) · Finite-volume Gibbs probability with a boundary condition · Finite-volume Gibbs measure as a probability measure · Finite-volume Boltzmann weight with a boundary condition · Finite-volume partition function with a boundary condition · Consistency of the plus measures under the specification · Weighted mixture of two measures · Configuration glued from inside spins and a boundary condition · Uniqueness of the Gibbs state · Infinite-volume state of a sequence of measures · DLR state of the Ising model on \(\mathbb{Z}^d\) · Ising specification in a box · Ising specification as a Markov kernel · Chosen subsequential weak limit of a sequence of measures · All-minus configuration · Minus-boundary Ising measure in a box · Infinite-volume minus state as a subsequential weak limit · \(\sigma\)-algebra of events determined outside a region · All-plus configuration · Plus-boundary Ising measure in a box · Infinite-volume plus state as a subsequential weak limit · The plus state is a Gibbs (DLR) state · Specification applied to a function · Specification applied to a bounded continuous function · Stochastic domination on increasing clopen events · Stochastic domination implies clopen domination, upper measure finite · Measurable increasing events of the configuration space · Bond configuration open on the edges inside a set · Contour event of a set: opposite spins across every crossing bond · Bond variable of a crossing bond · Configuration with the spins in a set flipped · Minus cluster of a site · Minus cluster of the origin as a finite set · Nearest-neighbour graph on the minus sites · Set of minus sites · Probability of the contour event of a set · Global spin flip of a configuration · Finite-volume magnetization at the origin · Probability that the origin spin is minus · Origin-only minus configuration satisfies the filled-cluster data · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Filled minus cluster of the origin as a finite set · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Integrability of the spin at a site under finite measures · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition · Spontaneous magnetization of the Ising model · Measurability of the spin at a site · Peierls' theorem · Spin at a site as a bounded continuous function · Approximation in measure by events measurable outside every box · Cylinder events of the Ising configuration space · σ-algebra generated by the spins in a finite set · Nonvacuity of the a.s.-tail theorem via the all-plus Dirac mass · All-plus Dirac mass gives the all-plus event probability one · Energy on a set with a boundary condition · Configuration glued from a set and a boundary condition · Finite-volume Gibbs measure on a finite set · Finite-volume Gibbs measure with plus boundary condition · Gibbs probability on a set with a boundary condition · Boltzmann weight on a set with a boundary condition · Partition function on a set with a boundary condition · Boundary influence bound for the minus box measures · Boundary influence bound for the plus box measures · Ergodicity of the plus state · Translation invariance of the plus state · Extreme point of the DLR states · Tail event for lattice spin configurations · Extremality of the plus state · Off-centre domination of all-plus events · Asymptotic shift homogeneity of all-plus events in plus boxes · Continuous functions with decaying shifted integrals · All-plus monomial as a bounded continuous function · All-plus monomial as a continuous function · Shift homogeneity of all-plus events in the plus state · Decay of shifted integrals for minus box measures · Shifted minus-boundary box measure · Decay of shifted integrals for plus box measures · Shifted plus-boundary box measure · Plus-spin indicator at a site as a bounded continuous function · Plus-spin indicator at a site as a continuous function · Subalgebra of cylinder functions · Cylinder functions as bounded continuous functions · Difference between an integral and its shifted version · Decay of shifted cylinder integrals for minus box measures · Decay of shifted cylinder integrals for plus box measures · Set where coupled measures differ is countable under a convex pressure · Coupled measures agree off a countable set, given a convex pressure · Box-edge marginal uniqueness off a countable set under tilt data · Edge-marginal uniqueness off a countable set from convex free energy · Average edge density of the \(q = 2\) random-cluster measure · Convexity of the ambient tilted log normalizer · Continuity in \(p\) of the Bernoulli edge weight · Monotonicity in \(p\) of free \(q = 2\) edge marginals on a finite graph · Continuity in \(t\) of free \(q = 2\) edge marginals on a finite graph · Left-continuity of the free \(q = 2\) edge density in \(t\) · Free \(q = 2\) edge density is monotone in \(p\) on \((0, 1)\) · 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\) · Derivative marginals of a convex pressure agree off a countable set · Free-wired log-normalizer gap \(\le |\partial|\log q/|E|\) for \(q \ge 1\) · Average wired edge density · Average wired edge density as the mean of edge marginals · Convexity of the wired tilted log normalizer · Wired tilted log normalizer as a cumulant generating function · Wired tilted log normalizer has derivative the mean open fraction · 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 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 · 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 · Wired percolation above the random-cluster critical point · Free percolation from domination and free–wired agreement at \(p'\) · Free percolation above \(p_c\) from monotonicity and countable agreement · The percolation event is increasing · Measurability of the percolation event · 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\) · Open self-avoiding walk in a box gives \(m\) distinct open box edges · Extended box configuration keeps box edge states · Event of an open self-avoiding walk of \(m\) steps · Bernoulli probability that edges \(F\) are all open is \(p^{|F|}\) · No wired percolation for \(2dp < 1\) and \(q \ge 1\) · Wired percolation bound \(\theta^1(p, q) \le (2dp)^m\) for \(q \ge 1\) · Event of some open self-avoiding walk is clopen · Single-edge open event is clopen · Event that a given walk is open is clopen · Event of some open self-avoiding walk is increasing · Event that a given walk is open is increasing · Wired cluster count is antitone · Monotonicity of the open subgraph · Bernoulli bound \(p^m\) for a fixed self-avoiding walk in the box · Percolation gives open self-avoiding walks of every length · 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 · 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\) · Monotonicity of the wired graph · Wired random-cluster percolation probability \(\theta(p, q)\) · Closed-circuit event of a dual circuit · Non-percolation means the origin's cluster is finite · Finite cluster in \(\mathbb{Z}^2\) gives a closed lattice circuit · Finite cluster in \(\mathbb{Z}^2\): closed circuit, separated point, odd crossings · Finite cluster in \(\mathbb{Z}^2\) has a reachable point outside it · Finite-cluster event is covered by closed-circuit events · Vertex coloring induced by a coloring of open clusters · Compatibility of a coloring with a bond configuration · Edwards–Sokal joint probability · Finite-volume plus-boundary magnetization at the origin · Random-cluster connection probability · Open connection between two vertices · Correspondence for cluster-constant colorings equal at two vertices · Ising two-point function from the Edwards–Sokal coupling · Ising two-point function equals the \(q = 2\) connection probability · Edwards–Sokal correlation identity · Potts two-point agreement at least \(1/q\) for \(q \ge 2\), \(\beta J > 0\) · Coloring constant on the wired graph · Colorings constant on wired clusters as cluster colorings · Edwards–Sokal weight with fixed boundary color · Spin marginal of the wired Edwards–Sokal measure · Bond marginal of the wired Edwards–Sokal measure · Total wired Edwards–Sokal weight · Open-edge graph with a boundary clique · There are \(q^{k(\omega)}\) colorings constant on the open clusters · Spin configuration constant on open clusters · Cluster-constant colorings as colorings of clusters · Edwards–Sokal spin marginal is the Potts measure · Edwards–Sokal bond marginal is the random-cluster measure · Edwards–Sokal edge factor · Spin marginal of the Edwards–Sokal measure · Bond marginal of the Edwards–Sokal measure · Edwards–Sokal joint weight · Edwards–Sokal weight summed over spins is the random-cluster weight · Edwards–Sokal bond sum is a multiple of the Potts weight · Edwards–Sokal partition function · Ising configuration of a two-state Potts coloring · Open connection of a vertex to the boundary · Wired Edwards–Sokal one-point function · Edwards–Sokal one-point identity · Wired colorings as cluster colorings with a pinned boundary cluster · Wired random-cluster probability of connecting to the boundary · Event mass under the random-cluster measure with a boundary graph · Boundary-graph comparison \(\varphi^{C'}(A) \le q^N \varphi^C(A)\) · Random-cluster probability with a boundary wiring · Empty wiring gives the free random-cluster measure · Boundary clique gives the wired random-cluster measure · Holley's condition for probabilities with nested wirings, \(q \ge 1\) · Free–wired sandwich for boundary graphs inside the boundary clique · Sandwich between the free and all-wired boundary conditions · Disintegration of a boundary-wired measure over conditioning fibres · Random-cluster comparison of boundary conditions for \(q \ge 1\) · Boundary-graph FK measure increases in \(p\) for \(q \ge 1\) · FKG inequality for the random-cluster measure, \(q \ge 1\) · Random-cluster weight with a boundary wiring · Holley's condition for weights with nested wirings, \(q \ge 1\) · Partition function with a boundary wiring · Number of open edges of a configuration · Conditional random-cluster measure with a boundary wiring · Holley's condition for nested-wiring conditional measures, \(q \ge 1\) · Conditional measures increase with the wiring for \(q \ge 1\) · Edges closed in one configuration and open in another · Edge density lies between \(p/(p+q(1-p))\) and \(p\) for \(q \ge 1\) · Edge marginal of a mass function · Probability that an edge is open under the random-cluster measure · Monotone couplings with equal edge marginals agree on up-sets · Mass of an event under a mass function · Comparison inequalities · Random-cluster measure increases stochastically in \(p\) when \(q \ge 1\) · Holley's cross inequality for FK measures, \(p_1 \le p_2\), \(q \ge 1\) · FKG lattice condition for the 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\) · FKG inequality for the random-cluster model · FKG inequality for increasing random-cluster events · Monotonicity of the random-cluster measure in p · 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\) · Partition function of a conditioning fibre · Monotone coupling of two mass functions · Kernel of the Laplacian of the open subgraph · Mixed supermodularity of free and wired cluster counts · Mixed supermodularity of cluster counts for nested wirings · Cluster count plus open-edge count is monotone · Number of clusters under a boundary wiring · Number of open clusters equals the dimension of the Laplacian kernel · Supermodularity of the random-cluster cluster count · Wirings with the boundary clique dominate the wired measure, \(q \ge 1\) · Wired measure conditionally dominated by larger wirings, \(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\) · Random-cluster weight is at most \(q^{|V|}\) for \(q \ge 1\) · Edge partition function is at most \(2^{|E|} q^{|V|}\) for \(q \ge 1\) · Uniform upper bound on the box free energy for \(d, n, q \ge 1\) · Isomorphism invariance of the ambient FK normalizer · Ambient FK normalizer is supermultiplicative under disjoint union · Graph isomorphism restricted to open subgraphs · Subadditivity of \(-\log Z\) along a juxtaposition sequence · FK partition function of a graph with no vertices is one · FK partition function at least the all-closed weight for \(q \ge 1\) · Bound \(-\log Z \le |E|\,(-\log(1-p))\) for \(q \ge 1\) · Peeling bound for \(-\log Z\) of a tagged graph · 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 · Number of open edges in a finite edge set · Glued configuration agrees with the outer one off the inner edge set · Law of total probability over outside configurations · Factorization of the wired FK weight of a glued configuration · Inner vertex with an outside-graph edge lies on the inner boundary · Conditional outer wired probability at most the inner wired one, \(q \ge 1\) · Domination by the inner wired measure under a coarser induced wiring · Conditional outer measure is the induced-wiring FK measure · Conditional outer probability as an induced-wiring probability · Conditioning fibre is the set of gluings · Factorization of the edge weight of a glued configuration · Projection fibres are conditioning fibres · Free inner measure is dominated by the conditional outer measure · Free inner measure is dominated by every induced-wiring measure · Cluster bijection for a glued configuration · Cluster map into the clusters of a glued configuration · Injectivity of the cluster map · Cluster map sends the inner cluster of \(x\) to that of \(\iota x\) · Cluster map sends an outside-only cluster of \(v\) to that of \(v\) · Surjectivity of the cluster map · Cluster graph of a glued configuration · Full-graph edges at non-inner vertices are outside-graph edges · Inner cluster reachability gives full-graph reachability of images · Full-graph and inner cluster reachability agree on embedded vertices · Factorization of the conditioned outer partition function · Wiring induced on the inner graph · Induced-wiring adjacency: distinct and joined in the outside graph · Inner cluster graph with the induced wiring · Full-graph reachability of images gives inner cluster reachability · Outside reachability gives inner cluster reachability · Image of the inner open subgraph in the outer graph · Endpoints of inner image edges are inner vertices · Inner image graph on embedded vertices is the open subgraph · Restriction of an outer configuration to inner edges · Restriction pulls back all-open events to their images · Restricting a glued configuration recovers the inner one · Outside-only property of an outside cluster · Cluster of a vertex is outside-only iff the vertex is · Lattice induced wirings are coarser than the inner boundary clique · Inner wired domination for vertex sets of \(\mathbb{Z}^d\) · Outer wired all-open probability at most the inner wired one · Glued cluster count is induced-wiring count plus outside-only clusters · Projection closing every inner edge · Projected configuration is closed on inner edges · Projection keeps non-inner edges · Idempotence of the inner-edge projection · Outside graph with the wired boundary clique · Outside-graph adjacency: open non-inner edge or boundary pair · Outside graph is a subgraph of the full cluster graph · Full-graph reachability from an outside-only vertex stays outside · Outside-only vertex · Outside-only clusters · Outside-only property is constant on outside clusters · Outside-only vertices are not inner · Graph of open non-inner edges · Number of outside-only clusters · Outer Bernoulli edge weight of a configuration · Positivity of the outer edge weight · Gluing of inner and outer configurations · Glued configuration on inner edges ignores the outer configuration · Glued configuration equals the outer one at each non-inner edge · Glued configuration takes the inner value on inner edges · Glued value on \(\{\iota x, \iota y\}\) is the inner value on \(\{x, y\}\) · Agreeing configuration is the gluing of its own restriction · Outer factor of the FK weight of a glued configuration · Positivity of the outer factor · Full cluster graph as the union of inner image and outside graphs · Outer wired fibre masses sum to one · Inner wired domination of the restricted outer wired measure · Extension of a box configuration by closed edges · Free random-cluster measure on a box · Free infinite-volume random-cluster measure · Free infinite-volume measure is a subsequential weak limit · Wired random-cluster measure on a box · Wired random-cluster measure as a probability mass function · Wired random-cluster probability of a configuration · Wired random-cluster weight · Wired random-cluster partition function · Wired infinite-volume random-cluster measure · Wired 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 · 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 · FKG lattice condition for the wired measure when \(q \ge 1\) · FKG inequality for the wired measure when \(q \ge 1\) · 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 · Event that all edges of a finite set are open · Mass of the all-open event under a weight function · Wired translation invariance from wired placements of every shift · Equal wired probabilities from eventually equal translated 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}\) · 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\) · Wired probability that the origin connects to the outside of a box · Wired crossing probabilities converge to the percolation probability · Crossing events intersect to the percolation event · 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 · 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 · 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 · 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 · 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 · Extended open graph with the inner box boundary wired · Extended wired graph with an extra wiring added · 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 · 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 · Box-boundary connection probability tends to percolation probability · Event that the open cluster of a site is infinite · A connection to outside the box passes through the box boundary · Crossing probabilities converge to the percolation probability · Joint percolation at most connectivity given no two infinite clusters · Two-point connectivity of a bond measure on \(\mathbb{Z}^d\) · Uniform decay of two-point connectivity without percolation · Two-point lower bound from FKG, invariance, uniqueness and percolation · Disconnected sites in infinite clusters give two infinite clusters · 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 · 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 · Infimum of the masses of an event along a measure sequence · Masses of clopen increasing events converge along decreasing measures · Supremum of the masses of an event along a measure sequence · Cylinder events of a box are measurable · Wired random-cluster probabilities are positive · Convergence to the wired two-point function under stochastic decrease · Outer projection agrees with the configuration off \(\Lambda_n\) · Wired \(q = 2\) percolation probability as the limit of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_n\) · Boundary connection of \(\Lambda_n\) is a \(\Lambda_m\) cylinder event · Boundary connection inside \(\Lambda_n\) reaches outside \(\Lambda_{n-1}\) · Events \(0 \leftrightarrow \partial\Lambda_n\) decrease in \(n \ge 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 · Configurations agreeing off \(F\) have equal conditional probabilities · Conditional wired decrease on inner increasing events for \(q \ge 1\) · Configurations agreeing off \(F\) have the same conditioning fibre · 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\) · Configurations with a given outer part form its conditioning fibre · 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 · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_k\) in \(\Lambda_{k+j}\) is nonincreasing in \(j\) · Masses of the conditioning fibres sum to one · 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 · Wired infinite-volume boundary connection tends to \(\theta^1(p, q)\) · Wired \(\Lambda_{n+1}\) measure decomposed over outer configurations · Wired box measures decrease on inner increasing events for \(q \ge 1\) · Countably many parameters admit a separating increasing event · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Van Hove tiling bound for the edge partition function · Configurations closed off the edges of a graph · Each non-edge contributes a factor 2 to the partition function · Per-box \(q = 2\) uniqueness off a countable set of tilts · Edge partition function of the random-cluster model · Interface subadditivity of \(-\log\) of the edge partition function · Per-edge free energy of boxes converges for \(d \ge 1\) · Event that an edge is open · Monotone-coupled laws with equal edge marginals agree on up-sets · Secant bound gives \(q = 2\) edge-event uniqueness off a countable set · Average edge density of a random-cluster measure · 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 infinite-volume mass function on a box for \(q \ge 1\) · Wired infinite-volume mass function on a box for \(q \ge 1\) · Toggle-invariant coordinates are open with probability one half · 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 · Wired \(q = 2\) infinite-volume mass function on a box · Free off-centre lower bound by the recentred small-box marginal · Free unit-edge marginals converge to the free density · Wired unit-edge marginals converge to the wired density · Wired off-centre upper bound by the recentred small-box marginal · Parametric agreement on increasing events off a countable set · Every lattice edge has the free \(q = 2\) density of \(\{0, e_0\}\) · Every lattice edge has the wired \(q = 2\) density of \(\{0, e_0\}\) · Wired FK edge marginals are at most one · Nonnegativity of wired FK edge marginals · Free \(q = 2\) edge density lies in \((0, 1)\) · Wired \(q = 2\) edge density lies in \((0, 1)\) · Wired infinite-volume edge density · Agreement of configurations off an edge set · Logarithmic \(\beta\)-derivative of the random-cluster weight · Number of closed edges · Fibre of configurations agreeing off an edge set · Random-cluster measure conditioned on the edges off a set · Domain Markov property (finite volume) · Conditional probability that an edge is open given the rest · Event that two vertices are joined by open edges · Real-valued indicator that an edge is open · Event depending only on edges outside a set · Bernoulli edge product · Inhomogeneous Bernoulli edge product · Inhomogeneous Bernoulli product over all edges but one · Bernoulli product over the edges other than one edge · Fibre representatives with every edge of a set closed · Finite-energy property · Covariance under the inhomogeneous random-cluster measure · Random-cluster expectation of an observable · Expectation under the inhomogeneous random-cluster measure · Unnormalized inhomogeneous random-cluster expectation · Ambient random-cluster law as a probability mass function · Probability of an ambient FK configuration · Inhomogeneous random-cluster probability · Probability of an event under the inhomogeneous random-cluster measure · Graph automorphisms preserve free FK edge marginals · Boundary-preserving automorphisms preserve wired FK edge marginals · Graph automorphisms preserve the free FK probability · Box symmetries preserve the free \(q = 2\) density of box edges · Automorphism as an isomorphism of open subgraphs · Box symmetries preserve the wired \(q = 2\) density of box edges · Boundary-preserving automorphisms preserve the wired FK probability · Boundary-preserving automorphism as an isomorphism of wired graphs · Unnormalized random-cluster weight · At \(q = 1\) the random-cluster weight is the Bernoulli product · Inhomogeneous random-cluster weight · Ambient FK normalizer · Partition function of the inhomogeneous random-cluster measure · Boundary-matching isomorphisms transport FK edge marginals · Isomorphic graphs have equal free FK probabilities after relabelling · Open-subgraph isomorphism for a pulled-back configuration · Pull-back along a permutation is relabelling · Boundary-matching isomorphisms preserve wired FK probabilities · Wired-graph isomorphism for a pulled-back configuration · Differential formula · Differential formula in β · FK measure induced on a fibre · Total FK weight of a fibre · Number of open clusters · Opening an edge lowers the cluster count by at most one · Opening an edge does not increase the cluster count · Number of open edges · Open subgraph of an edge configuration · Open subgraph as the meet of \(G\) with the open-edge graph · Monotonicity of the open subgraph in the configuration · Toggling a non-edge leaves the open subgraph unchanged · Closing the edges of a set in a configuration · Relabelling of an edge configuration by a vertex permutation · Relabelling as a permutation of the configuration space · Pull-back of an edge configuration along a vertex bijection · Pull-back of configurations as an equivalence · Two-point function of the free random-cluster measure · FKG inequality for connection events for \(q \ge 1\) · Almost-invariant events are trivial under an ergodic measure · Translation invariance of the free \(q = 2\) infinite-volume measure · Free \(q = 2\) box edge marginals are at most the free density · Wired \(q = 2\) box edge marginals are at least the wired density · Ergodicity of the wired random-cluster measure · Event that every edge of a set of box edges is open, on a box · Submodule of functions with vanishing free shift decay · Free \(q = 2\) multi-edge homogeneity under a translation · Monomial indicator as a bounded continuous function · Continuous monomial indicator that every edge of a set is open · Event that every edge of a finite set is open · Submodule of functions with vanishing wired shift decay · Wired \(q = 2\) multi-edge homogeneity under a translation · Disjoint-box cap hypothesis for multi-open events · Translated free box measure · Translated wired box measure · Conditional product cap for multi-open events in boxes · Extreme invariant measures are ergodic · 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 · 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 \(q = 2\) infinite-volume measure · Cylinder approximation of events under a finite measure · Translation-invariant self-mixing measures are ergodic · Self-mixing on cylinder events · Mixing for finite families of cylinder events · Product indicator of a multi-open event · Event that every coordinate of a finite set is open · Pair mixing of multi-open events · Indicator of agreeing with a pattern on a finite set · Upper decay of correlations of multi-open events · Coordinate state as a real number · Far-box product domination of multi-open events · Finite-box disjoint product domination of multi-open events · 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 · 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 · Edge-open indicator as a bounded continuous function · Edge-open indicator as a continuous function · Cylinder algebra generated by edge indicators · Cylinder algebra as bounded continuous functions · Density of cylinder functions among bounded continuous functions · 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 · 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 · Extreme point of the invariant probability measures · Shift-decay functional of a sequence of measures · Free shift decay on a dense set of test functions · Free translation invariance from decay on a dense set · Shift decay extends from a dense set of test functions · Wired shift decay on a dense set of test functions · Wired 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 · Wired integral shift decay along a box sequence · Identity shift satisfies the wired decay hypothesis · Wired 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 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 · 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 · Cluster lower bound for double-current sums · Random-current form of the \(\beta\)-derivative of the magnetization · Four-source lower bound for the pattern sum · Origin–site covariance in a box · Free-boundary site magnetization in a box · Finite-volume mean-field inequality for the Ising model · Origin magnetization with the outer-layer field switched off · Mean-field lower bound for the spontaneous magnetization · \(\beta\)-derivative of the origin magnetization in a box · Bond energy of a configuration · Energy with general couplings and a uniform field · Gibbs expectation with general couplings and a uniform field · Boltzmann weight with general couplings and a uniform field · Partition function with general couplings and a uniform field · Boltzmann weight with couplings · Random-current representation · Correlation function with couplings · Random-current representation with a field for even source sets · Global spin flip · Term of the exponential expansion of an edge weight · Partition function with couplings · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Conditional finite-volume Aizenman–Barsky–Fernández inequality · Two-point spin covariance · Covariance of a spin with a bond variable · Negative Hamiltonian of the Ising model · Ising one-point function · Plus-state two-point function at zero field · Simon–Lieb inequality in the infinite-volume plus state · Simon–Lieb boundary sum against a measure · Spin pair product as a bounded continuous function · Simon–Lieb inequality on a finite graph · Gibbs expectation with a site field · Boltzmann weight with a site field · Partition function with a site field · Ising model as a Physlib canonical ensemble · Hamiltonian agrees with Physlib's Ising energy · Ising Gibbs probability agrees with Physlib's canonical probability · Ising partition function agrees with Physlib's partition function · Edge bond sum is half the sum over ordered adjacent pairs · Configuration equivalence induced by a vertex relabeling · Configurations on a disjoint union as pairs of configurations · Bond variable of an unordered pair · Bond variable takes values \(\pm 1\) · Ising Hamiltonian on a finite graph · Finite-volume Ising Gibbs probability mass function · Gibbs probability of an Ising configuration · Ising Gibbs probabilities sum to one · Boltzmann weight of an Ising configuration · Ising partition function · Positivity of the Ising partition function · Spin of a configuration at a site · Global spin flip · Global spin flip as an involutive equivalence · Lee–Yang circle theorem · Ferromagnetic Lee–Yang polynomial has no zero in the open unit disk · Lee–Yang polynomial of a finite Ising model · Number of minus spins of a configuration · Zero-field Boltzmann weight of a configuration

Config Space

DefinitionCoordinate projection of a configuration#✓fully proved

The coordinate projection ω ↦ ω e of a configuration at the site e.

def eval (e : E) (ω : ConfigSpace E) : Bool := ω e

Uses 1 · Used by 9

Statement usesConfiguration space of a statistical-mechanics model

Used byσ-algebra of the configuration outside a region · Outside σ-algebra is a sub-σ-algebra of the product σ-algebra · Product σ-algebra on configuration space is generated by the coordinates · Uniqueness of the Gibbs state · Ising specification in a box · Ising specification as a Markov kernel · The plus state is a Gibbs (DLR) state · σ-algebra generated by the spins in a finite set · Nonvacuity of the a.s.-tail theorem via the all-plus Dirac mass

TheoremProduct σ-algebra on configuration space is generated by the coordinates#✓fully proved

The product σ-algebra on ConfigSpace E is generated by the coordinate projections; this holds by definition of MeasurableSpace.pi.

theorem measurableSpace_eq_iSup_comap :
    (inferInstance : MeasurableSpace (ConfigSpace E))
      = ⨆ e, MeasurableSpace.comap (eval e) inferInstance

Uses 2 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Coordinate projection of a configuration

Used byUniqueness of the Gibbs state · Nonvacuity of the a.s.-tail theorem via the all-plus Dirac mass

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.