The wired infinite-volume limit at q = 2

5 fully proved

A. Monotonicity in the volume

LemmaWired \(q = 2\) increasing-event probabilities do not grow with the box#✓fully proved

At q = 2, enlarging the wired box from Λ_m to Λ_(m+1) does not increase the probability of an increasing cylinder event of Λ_N, N ≤ m.

lemma fkWiredLimit_succ_le (N m : ℕ) (hNm : N ≤ m) {p : ℝ}
    (hp : 0 < p) (hp1 : p < 1)
    {S : Set (ConfigSpace (Sym2 (boxVerts d N)))} (hS : IsIncreasing S) :
    (wiredFiniteMeasure d (m + 1) hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S)
      ≤ (wiredFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S)

Uses 16 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Wired random-cluster measure on a box · Increasing event · Site of the hypercubic lattice

Proof usesVertex boundary of a box · Nearest-neighbour graph on a box · Restriction of a configuration from \(\Lambda_m\) to \(\Lambda_n\) · Restriction to \(\Lambda_n\) factors through \(\Lambda_m\) · Monotonicity of restriction between boxes · Inclusion of box edges into \(\mathbb{Z}^d\) · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired box measures decrease on increasing cylinder events at \(q = 2\) · Wired random-cluster probability of a configuration · Box \((-n, n)^d\) in the hypercubic lattice

Used byWired box probabilities of increasing cylinder events converge · Domain monotonicity of wired \(q = 2\) box measures

B. The limit

DefinitionInfimum of wired box probabilities of a box event#✓fully proved

The infimum over k of φ¹_(N+k)(S) for an event S of the box Λ_N, at q = 2.

noncomputable def fkWiredLimitValue (N : ℕ) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (S : Set (ConfigSpace (Sym2 (boxVerts d N)))) : ℝ :=
  ⨅ k, (wiredFiniteMeasure d (N + k) hp hp1 (by norm_num : (0 : ℝ) < 2)
      : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S)

Uses 5 · Used by 8

Statement usesConfiguration space of a statistical-mechanics model · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Wired random-cluster measure on a box · Site of the hypercubic lattice

Used byRight-continuity of the wired \(q = 2\) edge density in \(t\) · Free density is at most each translated wired marginal · Wired infinite-volume measure as limit on increasing cylinder events · Wired box probabilities of increasing cylinder events converge · Wired infinite-volume probability equals the infimum over boxes · Wired \(q = 2\) box edge marginals are at least the wired density · Constant wired density gives a lower bound on expected open edges · Upper decorrelation of the wired measure from factorization

LemmaWired box probabilities of increasing cylinder events converge#✓fully proved

At q = 2 the wired box probabilities of an increasing cylinder event converge to fkWiredLimitValue.

lemma fk_wired_limit_exists (N : ℕ) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    {S : Set (ConfigSpace (Sym2 (boxVerts d N)))} (hS : IsIncreasing S) :
    Tendsto (fun m => (wiredFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S)) atTop
      (𝓝 (fkWiredLimitValue N hp hp1 S))

Uses 8 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Infimum of wired box probabilities of a box event · Wired random-cluster measure on a box · Increasing event · Site of the hypercubic lattice

Proof usesWired \(q = 2\) increasing-event probabilities do not grow with the box

Used byWired infinite-volume measure as limit on increasing cylinder events · Wired infinite-volume probability equals the infimum over boxes

LemmaWired infinite-volume probability equals the infimum over boxes#✓fully proved

At q = 2 the chosen wired infinite-volume measure gives an increasing cylinder event the value fkWiredLimitValue.

lemma fkWiredLimit_wiredInfiniteVolume_eq (N : ℕ) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    {S : Set (ConfigSpace (Sym2 (boxVerts d N)))} (hS : IsIncreasing S) :
    (wiredInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S)
      = fkWiredLimitValue N hp hp1 S

Uses 13 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Infimum of wired box probabilities of a box event · Wired infinite-volume random-cluster measure · Increasing event · Site of the hypercubic lattice

Proof usesWired box probabilities of increasing cylinder events converge · Cylinder events of a box are clopen · Wired random-cluster measure on a box · Wired infinite-volume measure is a subsequential weak limit · Weak convergence of probability measures on configuration space · Portmanteau theorem for clopen events

Used byRight-continuity of the wired \(q = 2\) edge density in \(t\) · Free density is at most each translated wired marginal · Wired infinite-volume measure as limit on increasing cylinder events · Wired \(q = 2\) box edge marginals are at least the wired density · Constant wired density gives a lower bound on expected open edges · Upper decorrelation of the wired measure from factorization

TheoremWired infinite-volume measure as limit on increasing cylinder events#✓fully proved

Existence of the wired infinite-volume random-cluster measure as the limit of wired box measures, on increasing cylinder events at q = 2: φ¹_m(S) → φ¹(S) as m → ∞. The general statement (all q ≥ 1, weak convergence) is in Grimmett, The Random-Cluster Model (2006), Chapter 4.

theorem fk_wired_infinite_measure (N : ℕ) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    {S : Set (ConfigSpace (Sym2 (boxVerts d N)))} (hS : IsIncreasing S) :
    Tendsto (fun m => (wiredFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S)) atTop
      (𝓝 ((wiredInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S)))

Uses 10 · Used by 24

Statement usesConfiguration space of a statistical-mechanics model · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Wired random-cluster measure on a box · Wired infinite-volume random-cluster measure · Increasing event · Site of the hypercubic lattice

Proof usesInfimum of wired box probabilities of a box event · Wired infinite-volume probability equals the infimum over boxes · Wired box probabilities of increasing cylinder events converge

Used byWired \(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\) · 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 · 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 · Per-box \(q = 2\) uniqueness off a countable set of tilts · Secant bound gives \(q = 2\) edge-event uniqueness 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 · Equal wired densities from merging wired marginals · Wired box products approximate infinite-volume products · Decay of the edge-indicator functional from equal wired densities · Wired translation invariance from the placement hypothesis

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.