Skip to content

The Duminil-Copin–Tassion point for the Ising model

10 fully proved

A. The percolation version

DefinitionBond parameter \(1 - e^{-\beta}\)#✓fully proved

The bond parameter 1 - exp(-β) as an element of ℝ≥0.

noncomputable def bondParam (β : ℝ) : ℝ≥0 := Real.toNNReal (1 - Real.exp (-β))
Used by 1
Used byPercolation quantity \(\varphi_p(S)\) at \(p = 1 - e^{-\beta}\)

DefinitionPercolation quantity \(\varphi_p(S)\) at \(p = 1 - e^{-\beta}\)#✓fully proved

The percolation quantity φ_p(S) at p = 1 - exp(-β).

noncomputable def phiBeta (d : ℕ) (β : ℝ) (S : Finset (Site d)) : ℝ :=
  Percolation.phi d (bondParam β) (bondParam_le_one β) S
Uses 3 · Used by 1
Statement usesSite of the hypercubic lattice · Duminil-Copin–Tassion quantity · Bond parameter \(1 - e^{-\beta}\)
Used byInverse temperatures with a percolation witness \(\varphi(S) < 1\)

DefinitionInverse temperatures with a percolation witness \(\varphi(S) < 1\)#✓fully proved

Inverse temperatures β ≥ 0 with a finite S ∋ 0 such that φ_{1-e^{-β}}(S) < 1.

def tildeBetaCPercoSet (d : ℕ) : Set ℝ :=
  {β : ℝ | 0 ≤ β ∧ ∃ S : Finset (Site d), origin d ∈ S ∧ phiBeta d β S < 1}
Uses 3 · Used by 1
Statement usesSite of the hypercubic lattice · Origin of the hypercubic lattice · Percolation quantity \(\varphi_p(S)\) at \(p = 1 - e^{-\beta}\)
Used byPercolation auxiliary critical point on the \(\beta\) scale

DefinitionPercolation auxiliary critical point on the \(\beta\) scale#✓fully proved

The percolation auxiliary critical point on the β scale, the supremum of tildeBetaCPercoSet.

noncomputable def tildeBetaCPerco (d : ℕ) : ℝ :=
  sSup (tildeBetaCPercoSet d)
Uses 1
Statement usesInverse temperatures with a percolation witness \(\varphi(S) < 1\)

B. Free-boundary correlations in a finite set

DefinitionInduced subgraph of \(\mathbb{Z}^d\) on a finite set#✓fully proved

The subgraph of ℤ^d induced by a finite set S, on the vertex type S.

noncomputable def graphS (d : ℕ) (S : Finset (Site d)) : SimpleGraph {v // v ∈ S} :=
  (hypercubicLattice d).comap (fun v : {v // v ∈ S} => (v : Site d))
Uses 2 · Used by 7
Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)
Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Finite-volume mean-field inequality for the Ising model · 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\) · Free-boundary zero-field two-point function in a finite set · Simon–Lieb inequality in the infinite-volume plus state

DefinitionFree-boundary zero-field two-point function in a finite set#✓fully proved

The free-boundary zero-field two-point function ⟨σ_aσ_b⟩_S in the induced graph on S (equal to 1 when a = b).

noncomputable def freeCorr (d : ℕ) (β : ℝ) (S : Finset (Site d))
    (a b : {v // v ∈ S}) : ℝ :=
  if a = b then 1 else
    isingExpectation (graphS d S) β 0 (spinProd {a, b})
Uses 5 · Used by 7
Statement usesFinite-volume Ising expectation · Spin product over a vertex set · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Induced subgraph of \(\mathbb{Z}^d\) on a finite set
Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Finite-volume mean-field inequality for the Ising model · 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\) · Free origin correlation in a set, extended by zero · Simon–Lieb inequality in the infinite-volume plus state

DefinitionFree origin correlation in a set, extended by zero#✓fully proved

The function x ↦ ⟨σ_0σ_x⟩_S, extended by 0 outside S (and identically 0 if 0 ∉ S).

noncomputable def corrOriginInner (d : ℕ) (β : ℝ) (S : Finset (Site d))
    (x : Site d) : ℝ := by
  classical
  exact
    if h0 : origin d ∈ S then
      if hx : x ∈ S then
        freeCorr d β S ⟨origin d, h0⟩ ⟨x, hx⟩
      else 0
    else 0
Uses 3 · Used by 12
Statement usesSite of the hypercubic lattice · Origin of the hypercubic lattice · Free-boundary zero-field two-point function in a finite set
Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Boundary correlation of an edge crossing a cut · External boundary correlation of a cut, over edges leaving the box · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Oriented cut mass over cuts \(T \ni 0, x\) with \(y \notin T\) · 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\) · Duminil-Copin–Tassion quantity \(\varphi_\beta(S)\) for the Ising model · Simon–Lieb inequality in the infinite-volume plus state · Simon–Lieb boundary sum against a measure · Simon–Lieb boundary sum in the plus state

C. The Ising version of φ and β̃_c

DefinitionDuminil-Copin–Tassion quantity \(\varphi_\beta(S)\) for the Ising model#✓fully proved

The Duminil-Copin–Tassion quantity φ_β(S) = tanh β ∑_{(x,y) ∈ ∂S} ⟨σ_0σ_x⟩_S.

noncomputable def phiIsing (d : ℕ) (β : ℝ) (S : Finset (Site d)) : ℝ :=
  Real.tanh β * ∑ e ∈ Percolation.boundaryEdges d S, corrOriginInner d β S e.1
Uses 3 · Used by 6
Statement usesSite of the hypercubic lattice · Oriented edge boundary of a finite lattice set · Free origin correlation in a set, extended by zero
Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Finite-volume mean-field inequality for the Ising model · 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\) · Inverse temperatures with an Ising witness \(\varphi_\beta(S) < 1\)

DefinitionInverse temperatures with an Ising witness \(\varphi_\beta(S) < 1\)#✓fully proved

Inverse temperatures β ≥ 0 with a finite S ∋ 0 such that φ_β(S) < 1.

def tildeBetaCIsingSet (d : ℕ) : Set ℝ :=
  {β : ℝ | 0 ≤ β ∧ ∃ S : Finset (Site d), origin d ∈ S ∧ phiIsing d β S < 1}
Uses 3 · Used by 4
Statement usesSite of the hypercubic lattice · Origin of the hypercubic lattice · Duminil-Copin–Tassion quantity \(\varphi_\beta(S)\) for the Ising model
Used byMean-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\) · Auxiliary critical point \(\tilde\beta_c\) of the Ising model

DefinitionAuxiliary critical point \(\tilde\beta_c\) of the Ising model#✓fully proved

The auxiliary critical point β̃_c(d) = sup {β ≥ 0 | ∃ S ∋ 0, φ_β(S) < 1}.

noncomputable def tildeBetaCIsing (d : ℕ) : ℝ :=
  sSup (tildeBetaCIsingSet d)
Uses 1 · Used by 3
Statement usesInverse temperatures with an Ising witness \(\varphi_\beta(S) < 1\)
Used byMean-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\)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.