Exponential decay of the plus-state two-point function below β̃_c

3 fully proved

B. Distances and the Simon radius

DefinitionSimon radius of a finite set#✓fully proved

One more than the largest ℓ¹ distance from the origin of a point of T or of the outer endpoint of a boundary edge of T.

noncomputable def isingSimonRadius (d : ℕ) (T : Finset (Site d)) : ℕ :=
  max (T.sup (fun x ↦ l1dist d (origin d) x))
    ((boundaryEdges d T).sup (fun e ↦ l1dist d (origin d) e.2)) + 1

Uses 4 · Used by 1

Statement usesSite of the hypercubic lattice · \(\ell^1\) distance on \(\mathbb{Z}^d\) · Oriented edge boundary of a finite lattice set · Origin of the hypercubic lattice

Used bySharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\)

C. The tail supremum and its recursion

DefinitionTail set of plus-state correlations#✓fully proved

The set of values ⟨σ_0σ_z⟩^+_β with ‖z‖₁ ≥ n, together with 0.

def plusCorrTailSet (d : ℕ) (beta : ℝ) (n : ℕ) : Set ℝ :=
  insert 0 {r | ∃ z : Site d, n ≤ l1dist d (origin d) z ∧
    r = plusCorr d beta (origin d) z}

Uses 4 · Used by 2

Statement usesSite of the hypercubic lattice · \(\ell^1\) distance on \(\mathbb{Z}^d\) · Origin of the hypercubic lattice · Plus-state two-point function at zero field

Used byTail supremum of plus-state correlations · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\)

DefinitionTail supremum of plus-state correlations#✓fully proved

The tail supremum sup {⟨σ_0σ_z⟩^+_β | ‖z‖₁ ≥ n} (and 0).

noncomputable def plusCorrTailSup (d : ℕ) (beta : ℝ) (n : ℕ) : ℝ :=
  sSup (plusCorrTailSet d beta n)

Uses 1 · Used by 1

Statement usesTail set of plus-state correlations

Used bySharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.