Ordering of free and wired subsequential limits

3 fully proved

A. Domination passes to weak limits

LemmaFree limit at most wired limit along a common subsequence, \(q \ge 1\)#✓fully proved

If free and wired box measures converge weakly to ν₀ and ν₁ along a common subsequence and q ≥ 1, then ν₀(A) ≤ ν₁(A) for every clopen increasing event A.

lemma weakLimit_extremality_of_common_subseq (d : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    {ν₀ ν₁ : ProbabilityMeasure (ConfigSpace (Sym2 (Lattice.Site d)))}
    {ψ : ℕ → ℕ}
    (h₀ : WeakConvergesTo
      (fun n => freeFiniteMeasure d (ψ n) hp hp1 (zero_lt_one.trans_le hq)) ν₀)
    (h₁ : WeakConvergesTo
      (fun n => wiredFiniteMeasure d (ψ n) hp hp1 (zero_lt_one.trans_le hq)) ν₁)
    {A : Set (ConfigSpace (Sym2 (Lattice.Site d)))}
    (hAclopen : IsClopen A) (hAinc : IsIncreasing A) :
    (ν₀ : Measure (ConfigSpace (Sym2 (Lattice.Site d)))).real A
      ≤ (ν₁ : Measure (ConfigSpace (Sym2 (Lattice.Site d)))).real A

Uses 9 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Free random-cluster measure on a box · Wired random-cluster measure on a box · Increasing event · Site of the hypercubic lattice · Weak convergence of probability measures on configuration space

Proof usesFree box measure dominated by the wired one for \(q \ge 1\) · Stochastic domination compares real-valued masses · Portmanteau theorem for clopen events

Used byOrdered free and wired subsequential limits exist for \(q \ge 1\)

B. Existence of ordered limit pairs

LemmaCommon subsequence with free and wired weak limits#✓fully proved

Free and wired box measures have weak limits along a common strictly increasing subsequence.

lemma exists_common_subseq_weak_limits (d : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) :
    ∃ (ψ : ℕ → ℕ) (ν₀ ν₁ : ProbabilityMeasure (ConfigSpace (Sym2 (Lattice.Site d)))),
      StrictMono ψ ∧
        WeakConvergesTo (fun n => freeFiniteMeasure d (ψ n) hp hp1 hq) ν₀ ∧
        WeakConvergesTo (fun n => wiredFiniteMeasure d (ψ n) hp hp1 hq) ν₁

Uses 5 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Free random-cluster measure on a box · Wired random-cluster measure on a box · Site of the hypercubic lattice · Weak convergence of probability measures on configuration space

Used byOrdered free and wired subsequential limits exist for \(q \ge 1\)

LemmaOrdered free and wired subsequential limits exist for \(q \ge 1\)#✓fully proved

For q ≥ 1 there are a subsequence and weak limits φ0 (free) and φ1 (wired) along it with φ0(A) ≤ φ1(A) for all clopen increasing A.

lemma exists_infiniteVolume_extremal (d : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q) :
    ∃ (ψ : ℕ → ℕ) (φ0 φ1 : ProbabilityMeasure (ConfigSpace (Sym2 (Lattice.Site d)))),
      StrictMono ψ ∧
        WeakConvergesTo
          (fun n => freeFiniteMeasure d (ψ n) hp hp1 (zero_lt_one.trans_le hq)) φ0 ∧
        WeakConvergesTo
          (fun n => wiredFiniteMeasure d (ψ n) hp hp1 (zero_lt_one.trans_le hq)) φ1 ∧
        ∀ A : Set (ConfigSpace (Sym2 (Lattice.Site d))),
          IsClopen A → IsIncreasing A →
            (φ0 : Measure (ConfigSpace (Sym2 (Lattice.Site d)))).real A
              ≤ (φ1 : Measure (ConfigSpace (Sym2 (Lattice.Site d)))).real A

Uses 8

Statement usesConfiguration space of a statistical-mechanics model · Free random-cluster measure on a box · Wired random-cluster measure on a box · Increasing event · Site of the hypercubic lattice · Weak convergence of probability measures on configuration space

Proof usesCommon subsequence with free and wired weak limits · Free limit at most wired limit along a common subsequence, \(q \ge 1\)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.