Free and wired infinite-volume limits at q = 2

LemmaConvergence and ordering of free and wired limits at \(q = 2\)#✓fully proved

At q = 2, for an increasing cylinder event S, φ⁰_m(S) → φ⁰(S), φ¹_m(S) → φ¹(S), and φ⁰(S) ≤ φ¹(S).

lemma mvl_infiniteVolume_extremal (N : ℕ) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    {S : Set (ConfigSpace (Sym2 (boxVerts d N)))} (hS : IsIncreasing S) :
    Tendsto (fun m => (freeFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S)) atTop
      (𝓝 ((freeInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' 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)))
    ∧ (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)

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

MathlibExt/Probability/Configuration/ConfigSpace.lean:40

abbrev boxVerts (d n : ℕ) : Type := {x : Site d // x ∈ box d n}

PhyslibExt/StatisticalMechanics/RandomCluster/InfiniteVolume.lean:131

def IsIncreasing (A : Set (ConfigSpace E)) : Prop := IsUpperSet A

MathlibExt/Probability/CorrelationInequalities/IncreasingEvent.lean:55

noncomputable def freeFiniteMeasure (d n : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) :
    ProbabilityMeasure (ConfigSpace (Sym2 (Site d))) :=
  ⟨((fkPMF (boxGraph d n) hp hp1 hq).toMeasure).map (extendEdge d n),
    inferInstance⟩

PhyslibExt/StatisticalMechanics/RandomCluster/InfiniteVolume.lean:179

Uses 12

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 · Free infinite-volume random-cluster measure · Wired random-cluster measure on a box · 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 · Wired \(q = 2\) measure dominates the free one on increasing cylinders

LemmaConvergence and ordering at \(q = 2\) in subsequence form#✓fully proved

Subsequence form of mvl_infiniteVolume_extremal (with the identity subsequence).

StatMech.FK.mvl_infiniteVolume_extremal_subseq · 15 lines

lemma mvl_infiniteVolume_extremal_subseq (N : ℕ) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    {S : Set (ConfigSpace (Sym2 (boxVerts d N)))} (hS : IsIncreasing S) :
    ∃ (ψ : ℕ → ℕ)
      (φ0 φ1 : ProbabilityMeasure (ConfigSpace (Sym2 (Site d)))),
      StrictMono ψ
        ∧ φ0 = freeInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2)
        ∧ φ1 = wiredInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2)
        ∧ Tendsto (fun m => (freeFiniteMeasure d (ψ m) hp hp1 (by norm_num : (0 : ℝ) < 2)
            : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S)) atTop
            (𝓝 ((φ0 : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' 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
            (𝓝 ((φ1 : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S)))
        ∧ (φ0 : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S)
            ≤ (φ1 : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S)

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

MathlibExt/Probability/Configuration/ConfigSpace.lean:40

abbrev boxVerts (d n : ℕ) : Type := {x : Site d // x ∈ box d n}

PhyslibExt/StatisticalMechanics/RandomCluster/InfiniteVolume.lean:131

def IsIncreasing (A : Set (ConfigSpace E)) : Prop := IsUpperSet A

MathlibExt/Probability/CorrelationInequalities/IncreasingEvent.lean:55

abbrev Site (d : ℕ) : Type := Fin d → ℤ

MathlibExt/Combinatorics/SimpleGraph/Lattice/HypercubicLattice.lean:55

noncomputable def freeInfiniteVolume (d : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) :
    ProbabilityMeasure (ConfigSpace (Sym2 (Site d))) :=
  (CompactSpace.tendsto_subseq (fun n => freeFiniteMeasure d n hp hp1 hq)).choose

PhyslibExt/StatisticalMechanics/RandomCluster/InfiniteVolume.lean:199

Uses 12

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 · Free infinite-volume random-cluster measure · Wired random-cluster measure on a box · 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 · Wired \(q = 2\) measure dominates the free one on increasing cylinders

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.