Skip to content

FKG inequality and ordering for infinite-volume FK measures at q = 2

7 fully proved

A. The FKG inequality for the free measures

LemmaFKG inequality for free \(q = 2\) box measures on smaller-box events#✓fully proved

FKG inequality for the free box measure φ⁰_m (q = 2) on two increasing cylinder events of a smaller box Λ_N, N ≤ m.

lemma freeFiniteMeasure_fkg (N m : ℕ) (hNm : N ≤ m) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    {S₁ S₂ : Set (ConfigSpace (Sym2 (boxVerts d N)))}
    (hS₁ : IsIncreasing S₁) (hS₂ : IsIncreasing S₂) :
    (freeFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S₁)
      * (freeFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S₂)
      ≤ (freeFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real
            (boxRestrict d N ⁻¹' S₁ ∩ boxRestrict d N ⁻¹' S₂)
Uses 15 · 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\) · Free random-cluster measure on a box · Increasing event · Site of the hypercubic lattice
Proof usesNearest-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\) · Probability of an ambient FK configuration · FKG inequality for increasing random-cluster events · Free box measure of a cylinder event as a finite sum · Box \((-n, n)^d\) in the hypercubic lattice
Used byFKG inequality for the free \(q = 2\) infinite-volume measure

LemmaFKG inequality for the free \(q = 2\) infinite-volume measure#✓fully proved

FKG inequality for the free infinite-volume measure at q = 2 on increasing cylinder events of a box.

lemma ivp_iv_fkg (N : ℕ) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    {S₁ S₂ : Set (ConfigSpace (Sym2 (boxVerts d N)))}
    (hS₁ : IsIncreasing S₁) (hS₂ : IsIncreasing S₂) :
    (freeInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S₁)
      * (freeInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S₂)
      ≤ (freeInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real
            (boxRestrict d N ⁻¹' S₁ ∩ boxRestrict d N ⁻¹' S₂)
Uses 10
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\) · Free infinite-volume random-cluster measure · Increasing event · Site of the hypercubic lattice
Proof usesFree \(q=2\) box masses of increasing cylinders tend to infinite volume · Free random-cluster measure on a box · FKG inequality for free \(q = 2\) box measures on smaller-box events · Intersection of two increasing events is increasing

B. The FKG inequality for the wired measures

LemmaFKG lattice condition for the wired measure when \(q \ge 1\)#✓fully proved

The wired random-cluster measure satisfies the FKG lattice condition when q ≥ 1.

lemma wiredFkProb_FKGLatticeCondition {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q) :
    FKGLatticeCondition (fun ω => wiredFkProb G bdry p q ω)
Uses 8 · Used by 1
Statement usesConfiguration space of a statistical-mechanics model · Wired random-cluster probability of a configuration · FKG lattice condition
Proof usesRandom-cluster probability with a boundary wiring · Boundary clique gives the wired random-cluster measure · Holley's condition for probabilities with nested wirings, \(q \ge 1\) · Complete graph on the boundary vertices · Boundary wiring relation
Used byFKG inequality for the wired measure when \(q \ge 1\)

LemmaFKG inequality for the wired measure when \(q \ge 1\)#✓fully proved

FKG inequality for the wired random-cluster measure on a finite graph: increasing events are positively correlated when q ≥ 1.

lemma wiredFkProb_positively_associated_events {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    {A B : Set (ConfigSpace (Sym2 V))} (hA : IsIncreasing A) (hB : IsIncreasing B) :
    (∑ ω, wiredFkProb G bdry p q ω * A.indicator (fun _ => (1 : ℝ)) ω)
        * (∑ ω, wiredFkProb G bdry p q ω * B.indicator (fun _ => (1 : ℝ)) ω)
      ≤ ∑ ω, wiredFkProb G bdry p q ω * (A ∩ B).indicator (fun _ => (1 : ℝ)) ω
Uses 9 · Used by 1
Statement usesConfiguration space of a statistical-mechanics model · Wired random-cluster probability of a configuration · Increasing event
Proof usesBernoulli edge product · FKG lattice condition for the wired measure when \(q \ge 1\) · Wired random-cluster weight · Wired random-cluster partition function · Number of open clusters with wired boundary conditions · FKG inequality for increasing events
Used byFKG inequality for wired \(q = 2\) box measures on smaller-box events

LemmaFKG inequality for wired \(q = 2\) box measures on smaller-box events#✓fully proved

FKG inequality for the wired box measure φ¹_m (q = 2) on two increasing cylinder events of a smaller box Λ_N, N ≤ m.

lemma wiredFiniteMeasure_fkg (N m : ℕ) (hNm : N ≤ m) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    {S₁ S₂ : Set (ConfigSpace (Sym2 (boxVerts d N)))}
    (hS₁ : IsIncreasing S₁) (hS₂ : IsIncreasing S₂) :
    (wiredFiniteMeasure d m 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₂)
      ≤ (wiredFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real
            (boxRestrict d N ⁻¹' S₁ ∩ boxRestrict d N ⁻¹' S₂)
Uses 16 · 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\) · 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 random-cluster probability of a configuration · FKG inequality for the wired measure when \(q \ge 1\) · Box \((-n, n)^d\) in the hypercubic lattice
Used byFKG inequality for the wired \(q = 2\) infinite-volume measure

LemmaFKG inequality for the wired \(q = 2\) infinite-volume measure#✓fully proved

FKG inequality for the wired infinite-volume measure at q = 2 on increasing cylinder events of a box.

lemma ivp_iv_fkg_wired (N : ℕ) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    {S₁ S₂ : Set (ConfigSpace (Sym2 (boxVerts d N)))}
    (hS₁ : IsIncreasing S₁) (hS₂ : IsIncreasing S₂) :
    (wiredInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S₁)
      * (wiredInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S₂)
      ≤ (wiredInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real
            (boxRestrict d N ⁻¹' S₁ ∩ boxRestrict d N ⁻¹' S₂)
Uses 10 · 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\) · Wired infinite-volume random-cluster measure · Increasing event · Site of the hypercubic lattice
Proof usesWired infinite-volume measure as limit on increasing cylinder events · Wired random-cluster measure on a box · FKG inequality for wired \(q = 2\) box measures on smaller-box events · Intersection of two increasing events is increasing
Used byWired \(q = 2\) measure is ergodic under the factorization bound

C. Ordering of the infinite-volume measures

LemmaWired \(q = 2\) measure dominates the free one on increasing cylinders#✓fully proved

At q = 2 the free infinite-volume measure gives every increasing cylinder event at most the probability the wired one gives it.

lemma ivp_iv_monotone (N : ℕ) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    {S : Set (ConfigSpace (Sym2 (boxVerts d N)))} (hS : IsIncreasing S) :
    (freeInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S)
      ≤ (wiredInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S)
Uses 15 · 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\) · Free infinite-volume random-cluster measure · Wired infinite-volume random-cluster measure · Increasing event · Site of the hypercubic lattice
Proof usesFree \(q=2\) box masses of increasing cylinders tend to infinite volume · Wired infinite-volume measure as limit on increasing cylinder events · Free random-cluster measure on a box · Free box measure dominated by the wired one for \(q \ge 1\) · Box restriction pulls increasing events back to increasing events · Cylinder events of a box are measurable · Wired random-cluster measure on a box · Stochastic domination compares real-valued masses
Used byConvergence and ordering of free and wired limits at \(q = 2\) · Convergence and ordering at \(q = 2\) in subsequence form

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.