The contour-count bound over all clusters fails

DefinitionOrigin cluster family: finite site sets in the box through the origin#✓fully proved

The finite sets of sites in Λ_n containing the origin.

noncomputable def originClusterFamily (n : ℕ) : Finset (Finset (Site d)) :=
  (clusterFamily (d := d) n).filter (fun K => origin d ∈ K)

Uses 3 · Used by 1

Statement usesCluster family: all subsets of the box · Origin of \(\mathbb{Z}^d\) · Site of the hypercubic lattice

Used byPeierls series bound on the origin-cluster contour sum

DefinitionSite \(j e_c\) on the \(c\)-th coordinate axis#✓fully proved

The site j e_c on the c-th coordinate axis.

def pcc_rayS (c : Fin d) (j : ℕ) : Site d := fun i => if i = c then (j : ℤ) else 0

Uses 1 · Used by 1

Statement usesSite of the hypercubic lattice

Used byOrigin-only minus configuration satisfies the filled-cluster data

DefinitionPeierls series bound on the origin-cluster contour sum#✓fully proved

The sum of e^{-2β |∂K|} over the origin cluster family is at most the Peierls series.

def OriginContourCountBound (d n : ℕ) (β : ℝ) : Prop :=
  ∑ K ∈ originClusterFamily (d := d) n,
      Real.exp (-(2 * β) * (contourLen (↑K) (bondFinsetTouch d n) : ℝ))
    ≤ peierlsBound d β

Uses 5

Statement usesBonds touching the box · Contour length of a set · Origin cluster family: finite site sets in the box through the origin · Peierls series · Site of the hypercubic lattice

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.