DLR states of the Ising model

DefinitionMeasurable increasing events of the configuration space#✓fully proved

The measurable increasing events of the configuration space.

def upMeasSystem (E : Type*) : Set (Set (ConfigSpace E)) :=
  {A | MeasurableSet A ∧ IsUpperSet A}
Uses 1
Statement usesConfiguration space of a statistical-mechanics model

DefinitionWeighted mixture of two measures#✓fully proved

The mixture a μ⁻ + b μ⁺ of two measures.

noncomputable def gibbsMix (a b : ℝ≥0∞) (μm μp : Measure (ConfigSpace E)) :
    Measure (ConfigSpace E) :=
  a • μm + b • μp
Uses 1
Statement usesConfiguration space of a statistical-mechanics model

DefinitionBox \((-n, n)^d\) as a finite set of sites#✓fully proved

The box Λ_n = [-n, n]^d as a finite set of sites.

noncomputable def boxFinset (d n : ℕ) : Finset (Site d) :=
  (box_finite d n).toFinset
Uses 2 · Used by 27
Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice
Used byPositive planar percolation at some \(p < 1\) via the Ising model · Ordered nearest-neighbour pairs inside the box · Ordered nearest-neighbour pairs touching the box · Box energy with a boundary condition · Uniqueness of the Gibbs state · Ising specification in a box · Ising specification as a Markov kernel · The plus state is a Gibbs (DLR) state · Specification applied to a bounded continuous function · Cluster family: all subsets of the box · Origin-only minus configuration satisfies the filled-cluster data · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · 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 · Peierls' theorem · Boundary bond fraction of a box · Box sites as a set and as a finite set · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · Mean-field lower bound for the spontaneous magnetization · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state

DefinitionOrdered nearest-neighbour pairs touching the box#✓fully proved

Ordered nearest-neighbour pairs with at least one endpoint in Λ_n.

noncomputable def bondPairsTouch (d n : ℕ) : Finset (Site d × Site d) :=
  ((boxFinset d (n + 1)) ×ˢ (boxFinset d (n + 1))).filter
    (fun p => (hypercubicLattice d).Adj p.1 p.2 ∧ (p.1 ∈ box d n ∨ p.2 ∈ box d n))
Uses 4 · Used by 18
Statement usesBox \((-n, n)^d\) as a finite set of sites · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)
Used byPositive planar percolation at some \(p < 1\) via the Ising model · Bonds touching the box · The plus state is a Gibbs (DLR) state · Origin-only minus configuration satisfies the filled-cluster data · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · 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 · Peierls' theorem · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · Mean-field lower bound for the spontaneous magnetization · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state

DefinitionOrdered nearest-neighbour pairs inside the box#✓fully proved

Ordered nearest-neighbour pairs with both endpoints in Λ_n.

noncomputable def bondPairsInternal (d n : ℕ) : Finset (Site d × Site d) :=
  ((boxFinset d n) ×ˢ (boxFinset d n)).filter
    (fun p => (hypercubicLattice d).Adj p.1 p.2)
Uses 3 · Used by 2
Statement usesBox \((-n, n)^d\) as a finite set of sites · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)
Used byBonds inside the box · Mean-field lower bound for the spontaneous magnetization

DefinitionBonds touching the box#✓fully proved

The bonds with at least one endpoint in Λ_n (used for plus and minus boundary conditions).

noncomputable def bondFinsetTouch (d n : ℕ) : Finset (Sym2 (Site d)) :=
  (bondPairsTouch d n).image (fun p => s(p.1, p.2))
Uses 2 · Used by 41
Statement usesOrdered nearest-neighbour pairs touching the box · Site of the hypercubic lattice
Used byPositive planar percolation at some \(p < 1\) via the Ising model · Convexity of the set of DLR states · Consistency of the plus measures under the specification · Uniqueness of the Gibbs state · DLR state of the Ising model on \(\mathbb{Z}^d\) · Minus-boundary Ising measure in a box · Plus-boundary Ising measure in a box · The plus state is a Gibbs (DLR) state · Anchored closed-walk decoding of cluster contours in \(\mathbb{Z}^2\) · Peierls count of connected clusters by contour length · Connected clusters in a box with contour length \(\ell\) · Peierls series bound on the cluster-family contour sum · Peierls series bound on the connected-cluster contour sum · Connected face-boundary graphs at the axis for all connected clusters · Connected face-boundary graphs at the axis for all realised contours · Tight axis circuit data: contour edges in one axis-face component · Hole-free clusters with contour length \(\ell\) · Hole-free connected cluster through the origin · Winding hypothesis for outer contours on \(\mathbb{Z}^2\) · Contours of length \(\ell\) realised by connected clusters in a box · Outer contour map: clusters as interiors of boundary circuits · Boltzmann weight of a closed walk in the circuit sum · Peierls series bound on the origin-cluster contour sum · Peierls bound on the probability that the origin is minus · Filled-cluster winding hypothesis · Origin-only minus configuration satisfies the filled-cluster data · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · 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 · Peierls' theorem · Boundary bond fraction of a box · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · Mean-field lower bound for the spontaneous magnetization · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state

DefinitionBonds inside the box#✓fully proved

The bonds with both endpoints in Λ_n (used for the free boundary condition).

noncomputable def bondFinsetInternal (d n : ℕ) : Finset (Sym2 (Site d)) :=
  (bondPairsInternal d n).image (fun p => s(p.1, p.2))
Uses 2 · Used by 3
Statement usesOrdered nearest-neighbour pairs inside the box · Site of the hypercubic lattice
Used byFree-boundary Ising measure in a box · Boundary bond fraction of a box · Mean-field lower bound for the spontaneous magnetization

DefinitionConfiguration glued from inside spins and a boundary condition#✓fully proved

The configuration equal to τ inside the box Λ_n and to the boundary condition η outside.

noncomputable def glue (η : ConfigSpace (Site d)) {n : ℕ}
    (τ : {x // x ∈ box d n} → Bool) : ConfigSpace (Site d) :=
  fun x => if h : x ∈ box d n then τ ⟨x, h⟩ else η x
Uses 3 · Used by 33
Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice
Used byPositive planar percolation at some \(p < 1\) via the Ising model · Convexity of the set of DLR states · Box energy with a boundary condition · Finite-volume Gibbs measure on configurations of \(\mathbb{Z}^d\) · Finite-volume Gibbs measure as a probability measure · Uniqueness of the Gibbs state · Ising specification in a box · Ising specification as a Markov kernel · The plus state is a Gibbs (DLR) state · Specification applied to a bounded continuous function · Minus cluster of the origin as a finite set · Probability of the contour event of a set · Winding hypothesis for outer contours on \(\mathbb{Z}^2\) · Outer contour map: clusters as interiors of boundary circuits · Finite-volume magnetization at the origin · Probability that the origin spin is minus · Filled-cluster winding hypothesis · Origin-only minus configuration satisfies the filled-cluster data · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Filled minus cluster of the origin as a finite set · 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 · Peierls' theorem · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · Mean-field lower bound for the spontaneous magnetization · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state

DefinitionBox energy with a boundary condition#✓fully proved

The box energy -∑_{e ∈ B} σ_e - h ∑_{x ∈ Λ_n} σ_x of the configuration glue η τ.

noncomputable def fvEnergy (η : ConfigSpace (Site d)) (n : ℕ)
    (B : Finset (Sym2 (Site d))) (h : ℝ) (τ : {x // x ∈ box d n} → Bool) : ℝ :=
  - (∑ e ∈ B, bond (glue η τ) e) - h * ∑ x ∈ boxFinset d n, spin (glue η τ) x
Uses 7 · Used by 23
Statement usesConfiguration space of a statistical-mechanics model · Bond variable of an unordered pair · Box \((-n, n)^d\) as a finite set of sites · Configuration glued from inside spins and a boundary condition · Spin of a configuration at a site · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice
Used byPositive planar percolation at some \(p < 1\) via the Ising model · Convexity of the set of DLR states · Finite-volume Gibbs measure as a probability measure · Finite-volume Boltzmann weight with a boundary condition · Uniqueness of the Gibbs state · Ising specification in a box · Ising specification as a Markov kernel · The plus state is a Gibbs (DLR) state · Specification applied to a bounded continuous function · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · 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 · Peierls' theorem · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · Mean-field lower bound for the spontaneous magnetization · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state

DefinitionFinite-volume Boltzmann weight with a boundary condition#✓fully proved

The Boltzmann weight exp (-β H) of an inside configuration τ with boundary condition η.

noncomputable def fvWeight (η : ConfigSpace (Site d)) (n : ℕ)
    (B : Finset (Sym2 (Site d))) (β h : ℝ) (τ : {x // x ∈ box d n} → Bool) : ℝ :=
  Real.exp (-β * fvEnergy η n B h τ)
Uses 4 · Used by 24
Statement usesConfiguration space of a statistical-mechanics model · Box energy with a boundary condition · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice
Used byPositive planar percolation at some \(p < 1\) via the Ising model · Convexity of the set of DLR states · Finite-volume Gibbs probability with a boundary condition · Finite-volume Gibbs measure as a probability measure · Finite-volume partition function with a boundary condition · Uniqueness of the Gibbs state · Ising specification in a box · Ising specification as a Markov kernel · The plus state is a Gibbs (DLR) state · Specification applied to a bounded continuous function · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · 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 · Peierls' theorem · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · Mean-field lower bound for the spontaneous magnetization · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state

DefinitionFinite-volume partition function with a boundary condition#✓fully proved

The finite-volume partition function with boundary condition η.

noncomputable def fvZ (η : ConfigSpace (Site d)) (n : ℕ)
    (B : Finset (Sym2 (Site d))) (β h : ℝ) : ℝ :=
  ∑ τ : {x // x ∈ box d n} → Bool, fvWeight η n B β h τ
Uses 4 · Used by 23
Statement usesConfiguration space of a statistical-mechanics model · Finite-volume Boltzmann weight with a boundary condition · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice
Used byPositive planar percolation at some \(p < 1\) via the Ising model · Convexity of the set of DLR states · Finite-volume Gibbs probability with a boundary condition · Finite-volume Gibbs measure as a probability measure · Uniqueness of the Gibbs state · Ising specification in a box · Ising specification as a Markov kernel · The plus state is a Gibbs (DLR) state · Specification applied to a bounded continuous function · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · 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 · Peierls' theorem · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · Mean-field lower bound for the spontaneous magnetization · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state

DefinitionFinite-volume Gibbs probability with a boundary condition#✓fully proved

The finite-volume Gibbs probability of an inside configuration τ with boundary condition η.

noncomputable def fvProb (η : ConfigSpace (Site d)) (n : ℕ)
    (B : Finset (Sym2 (Site d))) (β h : ℝ) (τ : {x // x ∈ box d n} → Bool) : ℝ :=
  fvWeight η n B β h τ / fvZ η n B β h
Uses 5 · Used by 26
Statement usesConfiguration space of a statistical-mechanics model · Finite-volume Boltzmann weight with a boundary condition · Finite-volume partition function with a boundary condition · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice
Used byPositive planar percolation at some \(p < 1\) via the Ising model · Convexity of the set of DLR states · Finite-volume Gibbs measure on configurations of \(\mathbb{Z}^d\) · Finite-volume Gibbs measure as a probability measure · Uniqueness of the Gibbs state · Ising specification in a box · Ising specification as a Markov kernel · The plus state is a Gibbs (DLR) state · Specification applied to a bounded continuous function · Probability of the contour event of a set · Finite-volume magnetization at the origin · Probability that the origin spin is minus · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · 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 · Peierls' theorem · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · Mean-field lower bound for the spontaneous magnetization · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state

DefinitionFinite-volume Gibbs measure on configurations of \(\mathbb{Z}^d\)#✓fully proved

The finite-volume Gibbs measure in Λ_n with boundary condition η and bond set B, as a measure on configurations of ℤ^d.

noncomputable def fvMeasure (η : ConfigSpace (Site d)) (n : ℕ)
    (B : Finset (Sym2 (Site d))) (β h : ℝ) :
    Measure (ConfigSpace (Site d)) :=
  ∑ τ : {x // x ∈ box d n} → Bool,
    ENNReal.ofReal (fvProb η n B β h τ) • Measure.dirac (glue η τ)
Uses 5 · Used by 23
Statement usesConfiguration space of a statistical-mechanics model · Finite-volume Gibbs probability with a boundary condition · Configuration glued from inside spins and a boundary condition · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice
Used byPositive planar percolation at some \(p < 1\) via the Ising model · Convexity of the set of DLR states · Finite-volume Gibbs measure as a probability measure · Uniqueness of the Gibbs state · DLR state of the Ising model on \(\mathbb{Z}^d\) · Ising specification in a box · Ising specification as a Markov kernel · The plus state is a Gibbs (DLR) state · Specification applied to a function · Specification applied to a bounded continuous function · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · 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 · Peierls' theorem · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · Mean-field lower bound for the spontaneous magnetization · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state

DefinitionFinite-volume Gibbs measure as a probability measure#✓fully proved

The finite-volume Gibbs measure as a ProbabilityMeasure.

noncomputable def fvProbabilityMeasure (η : ConfigSpace (Site d)) (n : ℕ)
    (B : Finset (Sym2 (Site d))) (β h : ℝ) :
    ProbabilityMeasure (ConfigSpace (Site d)) :=
  ⟨fvMeasure η n B β h, fvMeasure_isProbabilityMeasure η n B β h⟩
Uses 9 · Used by 8
Statement usesConfiguration space of a statistical-mechanics model · Box energy with a boundary condition · Finite-volume Gibbs measure on configurations of \(\mathbb{Z}^d\) · Finite-volume Gibbs probability with a boundary condition · Finite-volume Boltzmann weight with a boundary condition · Finite-volume partition function with a boundary condition · Configuration glued from inside spins and a boundary condition · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice
Used byPositive planar percolation at some \(p < 1\) via the Ising model · Free-boundary Ising measure in a box · Minus-boundary Ising measure in a box · Plus-boundary Ising measure in a box · 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

DefinitionAll-plus configuration#✓fully proved

The all-plus configuration.

def plusField (d : ℕ) : ConfigSpace (Site d) := fun _ => true
Uses 2 · Used by 27
Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice
Used byPositive planar percolation at some \(p < 1\) via the Ising model · Uniqueness of the Gibbs state · Plus-boundary Ising measure in a box · The plus state is a Gibbs (DLR) state · Minus cluster of the origin as a finite set · Winding hypothesis for outer contours on \(\mathbb{Z}^2\) · Outer contour map: clusters as interiors of boundary circuits · Boltzmann weight of a closed walk in the circuit sum · Peierls bound on the probability that the origin is minus · Filled-cluster winding hypothesis · Origin-only minus configuration satisfies the filled-cluster data · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Filled minus cluster of the origin as a finite set · 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 · Peierls' theorem · Finite-volume Gibbs measure with plus boundary condition · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · Mean-field lower bound for the spontaneous magnetization · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state

DefinitionAll-minus configuration#✓fully proved

The all-minus configuration.

def minusField (d : ℕ) : ConfigSpace (Site d) := fun _ => false
Uses 2 · Used by 5
Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice
Used byFree-boundary Ising measure in a box · Uniqueness of the Gibbs state · Minus-boundary Ising measure in a box · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Mean-field lower bound for the spontaneous magnetization

DefinitionPlus-boundary Ising measure in a box#✓fully proved

The Ising measure in Λ_n with plus boundary condition.

noncomputable def plusMeasure (d n : ℕ) (β h : ℝ) :
    ProbabilityMeasure (ConfigSpace (Site d)) :=
  fvProbabilityMeasure (plusField d) n (bondFinsetTouch d n) β h
Uses 5 · Used by 26
Statement usesConfiguration space of a statistical-mechanics model · Bonds touching the box · Finite-volume Gibbs measure as a probability measure · All-plus configuration · Site of the hypercubic lattice
Used byPositive planar percolation at some \(p < 1\) via the Ising model · Consistency of the plus measures under the specification · Uniqueness of the Gibbs state · Infinite-volume plus state as a subsequential weak limit · The plus state is a Gibbs (DLR) state · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · 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 · Peierls' theorem · Boundary influence bound for the plus box measures · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · Off-centre domination of all-plus events · Asymptotic shift homogeneity of all-plus events in plus boxes · Continuous functions with decaying shifted integrals · Decay of shifted integrals for plus box measures · Shifted plus-boundary box measure · Decay of shifted cylinder integrals for plus box measures · Finite-volume plus-boundary magnetization at the origin · Mean-field lower bound for the spontaneous magnetization · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state

DefinitionMinus-boundary Ising measure in a box#✓fully proved

The Ising measure in Λ_n with minus boundary condition.

noncomputable def minusMeasure (d n : ℕ) (β h : ℝ) :
    ProbabilityMeasure (ConfigSpace (Site d)) :=
  fvProbabilityMeasure (minusField d) n (bondFinsetTouch d n) β h
Uses 5 · Used by 7
Statement usesConfiguration space of a statistical-mechanics model · Bonds touching the box · Finite-volume Gibbs measure as a probability measure · All-minus configuration · Site of the hypercubic lattice
Used byUniqueness of the Gibbs state · Infinite-volume minus state as a subsequential weak limit · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Boundary influence bound for the minus box measures · Decay of shifted integrals for minus box measures · Shifted minus-boundary box measure · Decay of shifted cylinder integrals for minus box measures

DefinitionFree-boundary Ising measure in a box#✓fully proved

The Ising measure in Λ_n with free boundary condition (internal bonds only).

noncomputable def freeMeasure (d n : ℕ) (β h : ℝ) :
    ProbabilityMeasure (ConfigSpace (Site d)) :=
  fvProbabilityMeasure (minusField d) n (bondFinsetInternal d n) β h
Uses 5 · Used by 2
Statement usesConfiguration space of a statistical-mechanics model · Bonds inside the box · Finite-volume Gibbs measure as a probability measure · All-minus configuration · Site of the hypercubic lattice
Used byInfinite-volume free state as a subsequential weak limit · Mean-field lower bound for the spontaneous magnetization

DefinitionInfinite-volume state of a sequence of measures#✓fully proved

μ is an infinite-volume state of the sequence ρ: some subsequence of ρ converges weakly to μ.

def InfiniteVolumeState (ρ : ℕ → ProbabilityMeasure (ConfigSpace (Site d)))
    (μ : ProbabilityMeasure (ConfigSpace (Site d))) : Prop :=
  ∃ φ : ℕ → ℕ, StrictMono φ ∧ WeakConvergesTo (ρ ∘ φ) μ
Uses 3 · Used by 17
Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Weak convergence of probability measures on configuration space
Used byPositive planar percolation at some \(p < 1\) via the Ising model · Existence of infinite-volume states · Uniqueness of the Gibbs state · Chosen subsequential weak limit of a sequence of measures · The plus state is a Gibbs (DLR) state · 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 · Peierls' theorem · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · Mean-field lower bound for the spontaneous magnetization · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state

LemmaExistence of infinite-volume states#✓fully proved

Every sequence of probability measures on configurations has an infinite-volume state, by Prokhorov compactness.

lemma exists_infiniteVolumeState
    (ρ : ℕ → ProbabilityMeasure (ConfigSpace (Site d))) :
    ∃ μ : ProbabilityMeasure (ConfigSpace (Site d)), InfiniteVolumeState ρ μ
Uses 4 · Used by 16
Statement usesConfiguration space of a statistical-mechanics model · Infinite-volume state of a sequence of measures · Site of the hypercubic lattice
Proof usesWeak convergence of probability measures on configuration space
Used byPositive planar percolation at some \(p < 1\) via the Ising model · Uniqueness of the Gibbs state · Chosen subsequential weak limit of a sequence of measures · The plus state is a Gibbs (DLR) state · 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 · Peierls' theorem · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · Mean-field lower bound for the spontaneous magnetization · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state

DefinitionChosen subsequential weak limit of a sequence of measures#✓fully proved

A subsequential weak limit of ρ, chosen by exists_infiniteVolumeState.

noncomputable def limitState (ρ : ℕ → ProbabilityMeasure (ConfigSpace (Site d))) :
    ProbabilityMeasure (ConfigSpace (Site d)) :=
  (exists_infiniteVolumeState ρ).choose
Uses 4 · Used by 18
Statement usesConfiguration space of a statistical-mechanics model · Infinite-volume state of a sequence of measures · Existence of infinite-volume states · Site of the hypercubic lattice
Used byPositive planar percolation at some \(p < 1\) via the Ising model · Infinite-volume free state as a subsequential weak limit · Uniqueness of the Gibbs state · Infinite-volume minus state as a subsequential weak limit · Infinite-volume plus state as a subsequential weak limit · The plus state is a Gibbs (DLR) state · 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 · Peierls' theorem · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · Mean-field lower bound for the spontaneous magnetization · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state

DefinitionInfinite-volume plus state as a subsequential weak limit#✓fully proved

The plus state: a weak subsequential limit of the plus-boundary box measures. Full-sequence convergence is not claimed here: the library only provides this state as a chosen subsequential limit (see plusState_isInfiniteVolumeState).

noncomputable def plusState (d : ℕ) (β h : ℝ) :
    ProbabilityMeasure (ConfigSpace (Site d)) :=
  limitState (fun n => plusMeasure d n β h)
Uses 4 · Used by 18
Statement usesConfiguration space of a statistical-mechanics model · Chosen subsequential weak limit of a sequence of measures · Plus-boundary Ising measure in a box · Site of the hypercubic lattice
Used byPositive planar percolation at some \(p < 1\) via the Ising model · Uniqueness of the Gibbs state · The plus state is a Gibbs (DLR) state · 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 · Spontaneous magnetization of the Ising model · Peierls' theorem · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · Shift homogeneity of all-plus events in the plus state · Mean-field lower bound for the spontaneous magnetization · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Plus-state two-point function at zero field · Simon–Lieb inequality in the infinite-volume plus state

DefinitionInfinite-volume minus state as a subsequential weak limit#✓fully proved

The minus state: a weak subsequential limit of the minus-boundary box measures.

noncomputable def minusState (d : ℕ) (β h : ℝ) :
    ProbabilityMeasure (ConfigSpace (Site d)) :=
  limitState (fun n => minusMeasure d n β h)
Uses 4 · Used by 1
Statement usesConfiguration space of a statistical-mechanics model · Chosen subsequential weak limit of a sequence of measures · Minus-boundary Ising measure in a box · Site of the hypercubic lattice
Used byUniqueness of the Gibbs state

DefinitionInfinite-volume free state as a subsequential weak limit#✓fully proved

The free state: a weak subsequential limit of the free-boundary box measures.

noncomputable def freeState (d : ℕ) (β h : ℝ) :
    ProbabilityMeasure (ConfigSpace (Site d)) :=
  limitState (fun n => freeMeasure d n β h)
Uses 4
Statement usesConfiguration space of a statistical-mechanics model · Free-boundary Ising measure in a box · Chosen subsequential weak limit of a sequence of measures · Site of the hypercubic lattice

DefinitionDLR state of the Ising model on \(\mathbb{Z}^d\)#✓fully proved

The DLR condition: for every n, the conditional distribution of μ given the spins outside the box Λ_n equals, for μ-almost every η, the finite-volume Gibbs measure fvMeasure η n (bondFinsetTouch d n) β h with boundary condition η.

def IsDLRState (d : ℕ) (β h : ℝ) (μ : Measure (ConfigSpace (Site d)))
    [IsFiniteMeasure μ] : Prop :=
  ∀ n : ℕ, ∀ᵐ η ∂μ,
    (gibbsConditional μ (box d n)) η = fvMeasure η n (bondFinsetTouch d n) β h
Uses 7 · Used by 4
Statement usesConfiguration space of a statistical-mechanics model · Bonds touching the box · Finite-volume Gibbs measure on configurations of \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Conditional distribution given the outside of a region · σ-algebra of the configuration outside a region
Used byConvexity of the set of DLR states · Uniqueness of the Gibbs state · The plus state is a Gibbs (DLR) state · Extreme point of the DLR states

DefinitionFinite intersections of a family of sets#✓fully proved

The finite intersections of sets from S (together with univ), a π-system generating the same σ-algebra.

noncomputable def finInterSystem {Ω : Type*} (S : Set (Set Ω)) : Set (Set Ω) :=
  Set.range (fun F : Finset S => ⋂₀ (Subtype.val '' (F : Set S)))
Used by 1
Used byConvexity of the set of DLR states

DefinitionIsing specification in a box#✓fully proved

The Ising specification in Λ_n: the kernel η ↦ fvMeasure η n B β h, measurable with respect to the spins outside Λ_n.

noncomputable def isingSpec (n : ℕ) (B : Finset (Sym2 (Site d))) (β h : ℝ) :
    @Kernel (ConfigSpace (Site d)) (ConfigSpace (Site d)) (outsideSigma (box d n)) _ :=
  @Kernel.mk (ConfigSpace (Site d)) (ConfigSpace (Site d)) (outsideSigma (box d n)) _
    (fun η => fvMeasure η n B β h)
    (@Measure.measurable_of_measurable_coe (ConfigSpace (Site d)) (ConfigSpace (Site d))
      _ (outsideSigma (box d n)) (fun η => fvMeasure η n B β h)
      (fun _ hs => meas_fvMeasure_coe n B β h hs))
Uses 14 · Used by 2
Statement usesConfiguration space of a statistical-mechanics model · Coordinate projection of a configuration · Bond variable of an unordered pair · Box \((-n, n)^d\) as a finite set of sites · Box energy with a boundary condition · Finite-volume Gibbs measure on configurations of \(\mathbb{Z}^d\) · Finite-volume Gibbs probability with a boundary condition · Finite-volume Boltzmann weight with a boundary condition · Finite-volume partition function with a boundary condition · Configuration glued from inside spins and a boundary condition · Spin of a configuration at a site · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · σ-algebra of the configuration outside a region
Used byConvexity of the set of DLR states · The plus state is a Gibbs (DLR) state

LemmaConvexity of the set of DLR states#✓fully proved

The DLR states form a convex set: a μ₁ + b μ₂ with a + b = 1 is a DLR state if μ₁, μ₂ are.

lemma convex_isDLRState (β h : ℝ) {a b : ℝ≥0∞} (hab : a + b = 1)
    (μ₁ μ₂ : Measure (ConfigSpace (Site d))) [IsFiniteMeasure μ₁] [IsFiniteMeasure μ₂]
    [IsFiniteMeasure (a • μ₁ + b • μ₂)]
    (h₁ : IsDLRState d β h μ₁) (h₂ : IsDLRState d β h μ₂) :
    IsDLRState d β h (a • μ₁ + b • μ₂)
Uses 17
Statement usesConfiguration space of a statistical-mechanics model · DLR state of the Ising model on \(\mathbb{Z}^d\) · Site of the hypercubic lattice
Proof usesBonds touching the box · Finite intersections of a family of sets · Box energy with a boundary condition · Finite-volume Gibbs measure on configurations of \(\mathbb{Z}^d\) · Finite-volume Gibbs probability with a boundary condition · Finite-volume Boltzmann weight with a boundary condition · Finite-volume partition function with a boundary condition · Configuration glued from inside spins and a boundary condition · Ising specification in a box · Box \((-n, n)^d\) in the hypercubic lattice · Conditional distribution given the outside of a region · Disintegration in product form for the outside conditional distribution · σ-algebra of the configuration outside a region · Outside σ-algebra is a sub-σ-algebra of the product σ-algebra

DefinitionStochastic domination on increasing clopen events#✓fully proved

μ ≼c ν: μ(A) ≤ ν(A) for every increasing clopen event A.

def StochasticallyDominatedClopen {E : Type*}
    (μ ν : Measure (ConfigSpace E)) : Prop :=
  ∀ A : Set (ConfigSpace E), IsClopen A → IsUpperSet A → μ.real A ≤ ν.real A
Uses 1 · Used by 2
Statement usesConfiguration space of a statistical-mechanics model
Used byUniqueness of the Gibbs state · Stochastic domination implies clopen domination, upper measure finite

LemmaStochastic domination implies clopen domination, upper measure finite#✓fully proved

ENNReal stochastic domination gives real-mass clopen domination when the upper measure is finite.

lemma StochasticallyDominated.toClopen {E : Type*} [Countable E]
    {μ ν : Measure (ConfigSpace E)} [IsFiniteMeasure ν] (h : μ ≼ ν) : μ ≼c ν
Uses 4
Statement usesConfiguration space of a statistical-mechanics model · Stochastic domination on increasing clopen events · Stochastic domination of measures on configurations
Proof usesStochastic domination compares real-valued masses

DefinitionIncreasing clopen events#✓fully proved

The increasing clopen events, a π-system generating the Borel σ-algebra.

def clopenUpSystem (E : Type*) : Set (Set (ConfigSpace E)) :=
  {A | IsClopen A ∧ IsUpperSet A}
Uses 1 · Used by 1
Statement usesConfiguration space of a statistical-mechanics model
Used byUniqueness of the Gibbs state

TheoremUniqueness of the Gibbs state#✓fully proved

For β, h ≥ 0, if the plus and minus states agree then every DLR state that is a probability measure equals the plus state.

S. Friedli and Y. Velenik, Statistical Mechanics of Lattice Systems, Cambridge University Press (2017), Chapter 3.

theorem gsi_gibbs_unique_of_phases_eq (β h : ℝ) (hβ : 0 ≤ β) (hh : 0 ≤ h)
    (μ : Measure (ConfigSpace (Site d))) [IsProbabilityMeasure μ]
    (hμ : IsDLRState d β h μ)
    (hphase : (plusState d β h : Measure (ConfigSpace (Site d)))
      = (minusState d β h : Measure (ConfigSpace (Site d)))) :
    μ = (minusState d β h : Measure (ConfigSpace (Site d)))
Uses 36
Statement usesConfiguration space of a statistical-mechanics model · DLR state of the Ising model on \(\mathbb{Z}^d\) · Infinite-volume minus state as a subsequential weak limit · Infinite-volume plus state as a subsequential weak limit · Site of the hypercubic lattice
Proof usesCoordinate projection of a configuration · Product σ-algebra on configuration space is generated by the coordinates · Increasing event · Infinite-volume state of a sequence of measures · Stochastic domination on increasing clopen events · Bond variable of an unordered pair · Bonds touching the box · Box \((-n, n)^d\) as a finite set of sites · Increasing clopen events · Existence of infinite-volume states · Box energy with a boundary condition · Finite-volume Gibbs measure on configurations of \(\mathbb{Z}^d\) · Finite-volume Gibbs probability with a boundary condition · Finite-volume Boltzmann weight with a boundary condition · Finite-volume partition function with a boundary condition · Configuration glued from inside spins and a boundary condition · Chosen subsequential weak limit of a sequence of measures · All-minus configuration · Minus-boundary Ising measure in a box · All-plus configuration · Plus-boundary Ising measure in a box · Spin of a configuration at a site · Box \((-n, n)^d\) in the hypercubic lattice · Stochastic domination of measures on configurations · Stochastic domination compares real-valued masses · Weak convergence of probability measures on configuration space · Conditional distribution given the outside of a region · Outside conditional distribution is a version of the conditional probability · Holley inequality for increasing events · σ-algebra of the configuration outside a region · Outside σ-algebra is a sub-σ-algebra of the product σ-algebra

DefinitionSpecification applied to a function#✓fully proved

The specification applied to f: η ↦ ∫ f d(fvMeasure η n B β h).

noncomputable def specApply (n : ℕ) (B : Finset (Sym2 (Site d))) (β h : ℝ)
    (f : ConfigSpace (Site d) → ℝ) (ω : ConfigSpace (Site d)) : ℝ :=
  ∫ y, f y ∂(fvMeasure ω n B β h)
Uses 3 · Used by 3
Statement usesConfiguration space of a statistical-mechanics model · Finite-volume Gibbs measure on configurations of \(\mathbb{Z}^d\) · Site of the hypercubic lattice
Used byConsistency of the plus measures under the specification · The plus state is a Gibbs (DLR) state · Specification applied to a bounded continuous function

DefinitionSpecification applied to a bounded continuous function#✓fully proved

The specification applied to a bounded continuous function, as a bounded continuous function.

noncomputable def specApply_bcf (n : ℕ) (B : Finset (Sym2 (Site d))) (β h : ℝ)
    (f : ConfigSpace (Site d) →ᵇ ℝ) : ConfigSpace (Site d) →ᵇ ℝ :=
  BoundedContinuousFunction.mkOfCompact
    ⟨specApply n B β h (f : ConfigSpace (Site d) → ℝ), specApply_continuous n B β h f.continuous⟩
Uses 13 · Used by 1
Statement usesConfiguration space of a statistical-mechanics model · Bond variable of an unordered pair · Box \((-n, n)^d\) as a finite set of sites · Box energy with a boundary condition · Finite-volume Gibbs measure on configurations of \(\mathbb{Z}^d\) · Finite-volume Gibbs probability with a boundary condition · Finite-volume Boltzmann weight with a boundary condition · Finite-volume partition function with a boundary condition · Configuration glued from inside spins and a boundary condition · Specification applied to a function · Spin of a configuration at a site · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice
Used byThe plus state is a Gibbs (DLR) state

DefinitionConsistency of the plus measures under the specification#✓fully proved

The plus measures in Λ_m are invariant under the specification in every Λ_n ⊆ Λ_m.

def FVConsistency (d : ℕ) (β h : ℝ) : Prop :=
  ∀ (n m : ℕ), n ≤ m → ∀ f : ConfigSpace (Site d) →ᵇ ℝ,
    ∫ ω, specApply n (bondFinsetTouch d n) β h (f : ConfigSpace (Site d) → ℝ) ω
        ∂(plusMeasure d m β h : Measure (ConfigSpace (Site d)))
      = ∫ ω, f ω ∂(plusMeasure d m β h : Measure (ConfigSpace (Site d)))
Uses 5 · Used by 1
Statement usesConfiguration space of a statistical-mechanics model · Bonds touching the box · Plus-boundary Ising measure in a box · Specification applied to a function · Site of the hypercubic lattice
Used byThe plus state is a Gibbs (DLR) state

DefinitionIsing specification as a Markov kernel#✓fully proved

The Ising specification in Λ_n as a Markov kernel on the full σ-algebra.

noncomputable def isingSpecFull (n : ℕ) (B : Finset (Sym2 (Site d))) (β h : ℝ) :
    Kernel (ConfigSpace (Site d)) (ConfigSpace (Site d)) :=
  Kernel.mk (fun η => fvMeasure η n B β h)
    (Measure.measurable_of_measurable_coe _
      (fun _ hs => (meas_fvMeasure_coe n B β h hs).mono (outsideSigma_le (box d n)) le_rfl))
Uses 15 · Used by 1
Statement usesConfiguration space of a statistical-mechanics model · Coordinate projection of a configuration · Bond variable of an unordered pair · Box \((-n, n)^d\) as a finite set of sites · Box energy with a boundary condition · Finite-volume Gibbs measure on configurations of \(\mathbb{Z}^d\) · Finite-volume Gibbs probability with a boundary condition · Finite-volume Boltzmann weight with a boundary condition · Finite-volume partition function with a boundary condition · Configuration glued from inside spins and a boundary condition · Spin of a configuration at a site · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · σ-algebra of the configuration outside a region · Outside σ-algebra is a sub-σ-algebra of the product σ-algebra
Used byThe plus state is a Gibbs (DLR) state

Definition\(\sigma\)-algebra of events determined outside a region#✓fully proved

The σ-algebra of events determined by the spins outside Λ.

@[reducible] def outsideInvariantMS {E : Type*} (Λ : Set E) : MeasurableSpace (ConfigSpace E) where
  MeasurableSet' s := ∀ ω ω' : ConfigSpace E, (∀ x ∉ Λ, ω x = ω' x) → (ω ∈ s ↔ ω' ∈ s)
  measurableSet_empty := by simp
  measurableSet_compl s hs ω ω' h := by simp only [Set.mem_compl_iff]; rw [hs ω ω' h]
  measurableSet_iUnion f hf ω ω' h := by
    simp only [Set.mem_iUnion]; exact exists_congr (fun i => hf i ω ω' h)
Uses 1 · Used by 1
Statement usesConfiguration space of a statistical-mechanics model
Used byThe plus state is a Gibbs (DLR) state

DefinitionOverwriting a configuration on an inner box#✓fully proved

The configuration on Λ_m obtained from σ by overwriting its spins in Λ_n with τ.

noncomputable def ovrBox {n m : ℕ} (_hnm : n ≤ m)
    (σ : {x // x ∈ box d m} → Bool) (τ : {x // x ∈ box d n} → Bool) :
    {x // x ∈ box d m} → Bool :=
  fun x => if hn : (x : Site d) ∈ box d n then τ ⟨x, hn⟩ else σ x
Uses 2 · Used by 6
Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice
Used byThe plus state is a Gibbs (DLR) state · Involution swapping inner-box parts of configuration pairs · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · Mean-field lower bound for the spontaneous magnetization

DefinitionRestriction of a configuration to an inner box#✓fully proved

The restriction of a configuration on Λ_m to Λ_n.

noncomputable def resBox {n m : ℕ} (hnm : n ≤ m)
    (σ : {x // x ∈ box d m} → Bool) : {x // x ∈ box d n} → Bool :=
  fun x => σ ⟨x, box_mono d hnm x.2⟩
Uses 2 · Used by 6
Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice
Used byThe plus state is a Gibbs (DLR) state · Involution swapping inner-box parts of configuration pairs · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · Mean-field lower bound for the spontaneous magnetization

DefinitionInvolution swapping inner-box parts of configuration pairs#✓fully proved

The involution of pairs exchanging the Λ_n parts of a configuration on Λ_m and a configuration on Λ_n.

noncomputable def swapPair {n m : ℕ} (hnm : n ≤ m) :
    (({x // x ∈ box d m} → Bool) × ({x // x ∈ box d n} → Bool))
      → (({x // x ∈ box d m} → Bool) × ({x // x ∈ box d n} → Bool)) :=
  fun p => (ovrBox hnm p.1 p.2, resBox hnm p.1)
Uses 4 · Used by 5
Statement usesOverwriting a configuration on an inner box · Restriction of a configuration to an inner box · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice
Used byThe plus state is a Gibbs (DLR) state · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · Mean-field lower bound for the spontaneous magnetization

TheoremThe plus state is a Gibbs (DLR) state#✓fully proved

For all β, h, the plus state of the Ising model on ℤ^d satisfies the DLR condition.

H.-O. Georgii, Gibbs Measures and Phase Transitions, de Gruyter (1988), Chapter 4.

theorem plusState_isDLR (β h : ℝ) :
    IsDLRState d β h (plusState d β h : Measure (ConfigSpace (Site d)))
Uses 38
Statement usesConfiguration space of a statistical-mechanics model · DLR state of the Ising model on \(\mathbb{Z}^d\) · Infinite-volume plus state as a subsequential weak limit · Site of the hypercubic lattice
Proof usesCoordinate projection of a configuration · Consistency of the plus measures under the specification · Infinite-volume state of a sequence of measures · Bond variable of an unordered pair · Bonds touching the box · Ordered nearest-neighbour pairs touching the box · Box \((-n, n)^d\) as a finite set of sites · Existence of infinite-volume states · Box energy with a boundary condition · Finite-volume Gibbs measure on configurations of \(\mathbb{Z}^d\) · Finite-volume Gibbs probability with a boundary condition · Finite-volume Boltzmann weight with a boundary condition · Finite-volume partition function with a boundary condition · Configuration glued from inside spins and a boundary condition · Ising specification in a box · Ising specification as a Markov kernel · Chosen subsequential weak limit of a sequence of measures · \(\sigma\)-algebra of events determined outside a region · Overwriting a configuration on an inner box · All-plus configuration · Plus-boundary Ising measure in a box · Restriction of a configuration to an inner box · Specification applied to a function · Specification applied to a bounded continuous function · Spin of a configuration at a site · Involution swapping inner-box parts of configuration pairs · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Weak convergence of probability measures on configuration space · Weak convergence implies convergence of integrals · Conditional distribution given the outside of a region · Disintegration in product form for the outside conditional distribution · σ-algebra of the configuration outside a region · Outside σ-algebra is a sub-σ-algebra of the product σ-algebra
42 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.