The Peierls argument: contour sums and the long-range-order criterion

4 fully proved

A. The Peierls series

DefinitionPeierls series#✓fully proved

The Peierls series ∑_ℓ ℓ (2d)^ℓ e^{-2βℓ}.

noncomputable def peierlsBound (d : ℕ) (β : ℝ) : ℝ :=
  ∑' ℓ : ℕ, (ℓ : ℝ) * (2 * d : ℝ) ^ ℓ * Real.exp (-(2 * β) * ℓ)

Used by 8

Used byPeierls series bound on the cluster-family contour sum · Peierls series bound on the connected-cluster contour sum · Twice the Peierls series · Peierls series bound on the origin-cluster contour sum · Peierls bound on the probability that the origin is minus · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionRatio \(2d e^{-2\beta}\) of the Peierls series#✓fully proved

The ratio 2d e^{-2β} of the Peierls series.

noncomputable def peierlsRatio (d : ℕ) (β : ℝ) : ℝ := (2 * d : ℝ) * Real.exp (-(2 * β))

Used by 3

Used byPlus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

B. The origin spin

DefinitionProbability that the origin spin is minus#✓fully proved

The probability that the origin spin is minus under the box measure with boundary condition η.

noncomputable def probOriginMinus (η : ConfigSpace (Site d)) (n : ℕ)
    (B : Finset (Sym2 (Site d))) (β h : ℝ) : ℝ :=
  ∑ τ : {x // x ∈ box d n} → Bool,
    (if (glue η τ) (origin d) = false then fvProb η n B β h τ else 0)

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

MathlibExt/Probability/Configuration/ConfigSpace.lean:40

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

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

def box (d n : ℕ) : Set (Site d) := {x | ∀ i, (x i).natAbs ≤ n}

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

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

PhyslibExt/CondensedMatter/IsingModel/InfiniteVolume.lean:125

def origin (d : ℕ) : Site d := fun _ => 0

PhyslibExt/CondensedMatter/IsingModel/Peierls.lean:195

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

PhyslibExt/CondensedMatter/IsingModel/InfiniteVolume.lean:177

Uses 6 · Used by 4

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 · Origin of \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byPeierls bound on the probability that the origin is minus · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

C. Long-range order from a contour bound

DefinitionPeierls bound on the probability that the origin is minus#✓fully proved

Under the plus box measure on Λ_n, the origin is minus with probability at most peierlsBound d β.

def PeierlsContourBound (d n : ℕ) (β : ℝ) : Prop :=
  probOriginMinus (plusField d) n (bondFinsetTouch d n) β 0 ≤ peierlsBound d β

noncomputable def probOriginMinus (η : ConfigSpace (Site d)) (n : ℕ)
    (B : Finset (Sym2 (Site d))) (β h : ℝ) : ℝ :=
  ∑ τ : {x // x ∈ box d n} → Bool,
    (if (glue η τ) (origin d) = false then fvProb η n B β h τ else 0)

PhyslibExt/CondensedMatter/IsingModel/PeierlsCriterion.lean:167

def plusField (d : ℕ) : ConfigSpace (Site d) := fun _ => true

PhyslibExt/CondensedMatter/IsingModel/InfiniteVolume.lean:226

noncomputable def bondFinsetTouch (d n : ℕ) : Finset (Sym2 (Site d)) :=
  (bondPairsTouch d n).image (fun p => s(p.1, p.2))

PhyslibExt/CondensedMatter/IsingModel/InfiniteVolume.lean:114

noncomputable def peierlsBound (d : ℕ) (β : ℝ) : ℝ :=
  ∑' ℓ : ℕ, (ℓ : ℝ) * (2 * d : ℝ) ^ ℓ * Real.exp (-(2 * β) * ℓ)

PhyslibExt/CondensedMatter/IsingModel/PeierlsCriterion.lean:71

Uses 4

Statement usesBonds touching the box · Peierls series · All-plus configuration · Probability that the origin spin is minus

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.