Two-point functions of infinite-volume FK measures

14 fully proved

A. Monotone limits along chains of measures

DefinitionSupremum of the masses of an event along a measure sequence#✓fully proved

The supremum over n of the masses μ n A of an event A.

noncomputable def ivTwoPointSup (μ : ℕ → ProbabilityMeasure (ConfigSpace E))
    (A : Set (ConfigSpace E)) : NNReal :=
  ⨆ n, (μ n) A

Uses 1 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model

Used byFree infinite-volume two-point function in a box

DefinitionInfimum of the masses of an event along a measure sequence#✓fully proved

The infimum over n of the masses μ n A of an event A.

noncomputable def ivTwoPointInf (μ : ℕ → ProbabilityMeasure (ConfigSpace E))
    (A : Set (ConfigSpace E)) : NNReal :=
  ⨅ n, (μ n) A

Uses 1 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model

Used byMasses of clopen increasing events converge along decreasing measures · Wired infinite-volume two-point function in a box

LemmaMasses of clopen increasing events converge along decreasing measures#✓fully proved

Along a stochastically decreasing sequence of measures, the mass of a clopen increasing event converges to its infimum.

lemma ivTwoPointInf_isLimit (μ : ℕ → ProbabilityMeasure (ConfigSpace E))
    (hchain : ∀ n, (μ (n + 1) : Measure (ConfigSpace E)) ≼ (μ n : Measure (ConfigSpace E)))
    {A : Set (ConfigSpace E)} (hAclopen : IsClopen A) (hAinc : IsIncreasing A) :
    Tendsto (fun n => (μ n) A) atTop (𝓝 (ivTwoPointInf μ A))

Uses 5 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Infimum of the masses of an event along a measure sequence · Increasing event · Stochastic domination of measures on configurations

Proof usesStochastic domination compares real-valued masses

Used byConvergence to the wired two-point function under stochastic decrease

B. Restriction to a box and box connection events

DefinitionRestriction of a configuration of \(\mathbb{Z}^d\) to a box#✓fully proved

Restriction of a configuration of ℤ^d to the edges of the box Λ_n.

def boxRestrict (d n : ℕ) (ω : ConfigSpace (Sym2 (Site d))) :
    ConfigSpace (Sym2 (boxVerts d n)) :=
  fun eb => ω (edgeIncl d n eb)

Uses 4 · Used by 111

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

Used byBernoulli box cylinder probability equals its probability on the box · Bernoulli percolation restricted to a box is Bernoulli on the box · 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 · Box-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)\) · 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\) · Event that the box origin connects to the box boundary · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · 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 · 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 · Wired translation invariance from wired placements of every shift · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · 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 · 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 · 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 · 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 · Cylinder events of a box are clopen · Box restriction pulls increasing events back to increasing events · Cylinder events of a box are measurable · 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 · Restriction to \(\Lambda_n\) factors through \(\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\) · 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 \(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 · Free infinite-volume mass function on a box for \(q \ge 1\) · 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\) · Free \(q = 2\) infinite-volume mass function on a box · Wired \(q = 2\) infinite-volume mass function on a box · Free unit-edge marginals converge to the free density · Wired unit-edge marginals converge to the wired density · Free \(q = 2\) edge density lies in \((0, 1)\) · Wired \(q = 2\) edge density lies in \((0, 1)\) · Box symmetries preserve the free \(q = 2\) density of box edges · Box symmetries preserve the wired \(q = 2\) density of box edges · 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 · Disjoint-box cap hypothesis for multi-open events · Conditional product cap for multi-open events in boxes · Constant free density gives an upper bound on expected open edges · Equal free densities from merging free marginals · Constant wired density gives a lower bound on expected open edges · Equal wired densities from merging wired marginals · Wired box products approximate infinite-volume products · Upper decorrelation of the wired measure from factorization · Domain monotonicity of wired \(q = 2\) box measures · 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 · Wired translation invariance from the placement hypothesis

LemmaCylinder events of a box are clopen#✓fully proved

Cylinder events of the box Λ_N are clopen.

lemma isClopen_boxRestrict_preimage {d : ℕ} (N : ℕ)
    (S : Set (ConfigSpace (Sym2 (boxVerts d N)))) : IsClopen (boxRestrict d N ⁻¹' S)

Uses 6 · Used by 5

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\) · Site of the hypercubic lattice

Proof usesInclusion of box edges into \(\mathbb{Z}^d\) · Box \((-n, n)^d\) in the hypercubic lattice

Used byFK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Free \(q = 2\) infinite-volume mass of increasing cylinders as a box limit · Wired infinite-volume probability equals the infimum over boxes · Cylinder events of a box are measurable · Per-box uniqueness of the random-cluster measures off a countable set

LemmaCylinder events of a box are measurable#✓fully proved

Cylinder events of the box Λ_N are measurable.

lemma measurableSet_boxRestrict_preimage {d : ℕ} (N : ℕ)
    (S : Set (ConfigSpace (Sym2 (boxVerts d N)))) : MeasurableSet (boxRestrict d N ⁻¹' S)

Uses 5 · Used by 5

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\) · Site of the hypercubic lattice

Proof usesCylinder events of a box are clopen

Used byWired \(q = 2\) measure dominates the free one on increasing cylinders · 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

LemmaBox restriction pulls increasing events back to increasing events#✓fully proved

The preimage of an increasing event under box restriction is increasing.

lemma isIncreasing_boxRestrict_preimage {d : ℕ} (N : ℕ)
    {S : Set (ConfigSpace (Sym2 (boxVerts d N)))} (hS : IsIncreasing S) :
    IsIncreasing (boxRestrict d N ⁻¹' S)

Uses 6 · Used by 1

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\) · Increasing event · Site of the hypercubic lattice

Proof usesInclusion of box edges into \(\mathbb{Z}^d\)

Used byWired \(q = 2\) measure dominates the free one on increasing cylinders

DefinitionEvent that two sites are joined by open edges inside a box#✓fully proved

The event that x and y are joined by open edges inside the box Λ_n.

def boxConnEvent (d n : ℕ) (x y : boxVerts d n) : Set (ConfigSpace (Sym2 (Site d))) :=
  boxRestrict d n ⁻¹' (connEvent (boxGraph d n) x y)

Uses 6 · Used by 10

Statement usesConfiguration space of a statistical-mechanics model · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Event that two vertices are joined by open edges · Site of the hypercubic lattice

Used byBox-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · 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 · Wired infinite-volume two-point function in a box · Convergence to the wired two-point function under stochastic decrease · Cylinder form of the \(\Lambda_n\) boundary connection is measurable · Infinite-volume limit of the wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_k\) · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{n+1}\) at most in \(\Lambda_n\)

C. Connection probabilities of the box measures

LemmaFree box measure of a box connection event is the two-point function#✓fully proved

The free box measure of the connection event in Λ_n is the finite-volume two-point function.

lemma freeFiniteMeasure_real_boxConnEvent (d n : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) (x y : boxVerts d n) :
    (freeFiniteMeasure d n hp hp1 hq : Measure (ConfigSpace (Sym2 (Site d)))).real
        (boxConnEvent d n x y)
      = twoPointFun (boxGraph d n) p q x y

Uses 18

Statement usesConfiguration space of a statistical-mechanics model · Event that two sites are joined by open edges inside a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Free random-cluster measure on a box · Two-point function of the free random-cluster measure · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesRestriction of a configuration of \(\mathbb{Z}^d\) to a box · Event that two vertices are joined by open edges · Inclusion of box edges into \(\mathbb{Z}^d\) · Bernoulli edge product · Extension of a box configuration by closed edges · Ambient random-cluster law as a probability mass function · Probability of an ambient FK configuration · Unnormalized random-cluster weight · Ambient FK normalizer · Number of open clusters

LemmaWired random-cluster probabilities are positive#✓fully proved

Every configuration has positive wired random-cluster probability.

lemma wiredFkProb_pos {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V)
    [DecidableRel G.Adj] (bdry : V → Prop) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) (ω : ConfigSpace (Sym2 V)) :
    0 < wiredFkProb G bdry p q ω

Uses 6

Statement usesConfiguration space of a statistical-mechanics model · Wired random-cluster probability of a configuration

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

D. Infinite-volume two-point functions

DefinitionFree infinite-volume two-point function in a box#✓fully proved

The free infinite-volume two-point function in Λ_N: the supremum over n of φ⁰_n(x ↔ y in Λ_N).

noncomputable def freeIvTwoPoint (d N : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) (x y : boxVerts d N) : NNReal :=
  ivTwoPointSup (fun n => freeFiniteMeasure d n hp hp1 hq) (boxConnEvent d N x y)

Uses 5 · Used by 1

Statement usesEvent that two sites are joined by open edges inside a box · Vertices of the box \((-n, n)^d\) · Free random-cluster measure on a box · Supremum of the masses of an event along a measure sequence · Site of the hypercubic lattice

Used byConvergence to the free two-point function under stochastic increase

DefinitionWired infinite-volume two-point function in a box#✓fully proved

The wired infinite-volume two-point function in Λ_N: the infimum over n of φ¹_n(x ↔ y in Λ_N).

noncomputable def wiredIvTwoPoint (d N : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) (x y : boxVerts d N) : NNReal :=
  ivTwoPointInf (fun n => wiredFiniteMeasure d n hp hp1 hq) (boxConnEvent d N x y)

Uses 5 · Used by 1

Statement usesEvent that two sites are joined by open edges inside a box · Vertices of the box \((-n, n)^d\) · Infimum of the masses of an event along a measure sequence · Wired random-cluster measure on a box · Site of the hypercubic lattice

Used byConvergence to the wired two-point function under stochastic decrease

LemmaConvergence to the free two-point function under stochastic increase#✓fully proved

If the free box measures increase stochastically in n, then φ⁰_n(x ↔ y in Λ_N) converges to freeIvTwoPoint.

lemma freeIvTwoPoint_isLimit (d N : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (hchain : ∀ n, (freeFiniteMeasure d n hp hp1 hq : Measure (ConfigSpace (Sym2 (Site d))))
        ≼ (freeFiniteMeasure d (n + 1) hp hp1 hq : Measure (ConfigSpace (Sym2 (Site d)))))
    (x y : boxVerts d N) :
    Tendsto (fun n => (freeFiniteMeasure d n hp hp1 hq) (boxConnEvent d N x y)) atTop
      (𝓝 (freeIvTwoPoint d N hp hp1 hq x y))

Uses 16

Statement usesConfiguration space of a statistical-mechanics model · Event that two sites are joined by open edges inside a box · Vertices of the box \((-n, n)^d\) · Free random-cluster measure on a box · Free infinite-volume two-point function in a box · Site of the hypercubic lattice · Stochastic domination of measures on configurations

Proof usesNearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Event that two vertices are joined by open edges · Inclusion of box edges into \(\mathbb{Z}^d\) · Open subgraph of an edge configuration · Monotonicity of the open subgraph in the configuration · Increasing event · Box \((-n, n)^d\) in the hypercubic lattice · Convergence of increasing-event probabilities along an increasing chain

LemmaConvergence to the wired two-point function under stochastic decrease#✓fully proved

If the wired box measures decrease stochastically in n, then φ¹_n(x ↔ y in Λ_N) converges to wiredIvTwoPoint.

lemma wiredIvTwoPoint_isLimit (d N : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (hchain : ∀ n, (wiredFiniteMeasure d (n + 1) hp hp1 hq : Measure (ConfigSpace (Sym2 (Site d))))
        ≼ (wiredFiniteMeasure d n hp hp1 hq : Measure (ConfigSpace (Sym2 (Site d)))))
    (x y : boxVerts d N) :
    Tendsto (fun n => (wiredFiniteMeasure d n hp hp1 hq) (boxConnEvent d N x y)) atTop
      (𝓝 (wiredIvTwoPoint d N hp hp1 hq x y))

Uses 16

Statement usesConfiguration space of a statistical-mechanics model · Event that two sites are joined by open edges inside a box · Vertices of the box \((-n, n)^d\) · Wired random-cluster measure on a box · Wired infinite-volume two-point function in a box · Site of the hypercubic lattice · Stochastic domination of measures on configurations

Proof usesNearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Event that two vertices are joined by open edges · Inclusion of box edges into \(\mathbb{Z}^d\) · Masses of clopen increasing events converge along decreasing measures · Open subgraph of an edge configuration · Monotonicity of the open subgraph in the configuration · Increasing event · Box \((-n, n)^d\) in the hypercubic lattice

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.