Finite susceptibility of the plus state below β̃_c

DefinitionWindow sum of plus-state correlations#✓fully proved

The window sum ∑_{z ∈ L} ⟨σ_0σ_z⟩^+_β.

noncomputable def plusCorrWindowSum (d : ℕ) (beta : ℝ)
    (L : Finset (Site d)) : ℝ :=
  ∑ z ∈ L, plusCorr d beta (Percolation.origin d) z

Uses 3 · Used by 4

Statement usesSite of the hypercubic lattice · Origin of the hypercubic lattice · Plus-state two-point function at zero field

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Supremum of plus-state window sums over windows of at most \(n\) sites · 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\)

DefinitionSupremum of plus-state window sums over windows of at most \(n\) sites#✓fully proved

The supremum of the window sums over windows with at most n sites.

noncomputable def plusCorrWindowSup (d : ℕ) (beta : ℝ) (n : ℕ) : ℝ :=
  sSup {r : ℝ | ∃ L : Finset (Site d), L.card ≤ n ∧
    r = plusCorrWindowSum d beta L}

Uses 2 · Used by 3

Statement usesSite of the hypercubic lattice · Window sum of plus-state correlations

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · 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\)

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.