The Duminil-Copin–Tassion quantity φ_p(S) and the threshold p̃_c

DefinitionShift of a lattice site in one coordinate#✓fully proved

The site x + δ e_i obtained by moving x by δ in coordinate i.

def coordShift (x : Site d) (i : Fin d) (δ : ℤ) : Site d :=
  Function.update x i (x i + δ)

Uses 1 · Used by 13

Statement usesSite of the hypercubic lattice

Used byStep directions of an open walk from the origin · Positivity of the critical probability (Hammersley's bound) · Vertices of a lattice path encoded by a step sequence · Duminil-Copin–Tassion differential inequality · Exponential decay below p̃_c · Sharpness of the phase transition · Oriented edge boundary of a finite lattice set · Size bound for the edge boundary · Open self-avoiding walk in a box gives \(m\) distinct open box edges · Percolation gives open self-avoiding walks of every length · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Simon–Lieb inequality in the infinite-volume plus state

DefinitionSign of a unit lattice step#✓fully proved

The unit step +1 (for true) or -1 (for false).

def stepSign (b : Bool) : ℤ := if b then 1 else -1

Used by 13

Used byStep directions of an open walk from the origin · Positivity of the critical probability (Hammersley's bound) · Vertices of a lattice path encoded by a step sequence · Duminil-Copin–Tassion differential inequality · Exponential decay below p̃_c · Sharpness of the phase transition · Oriented edge boundary of a finite lattice set · Size bound for the edge boundary · Open self-avoiding walk in a box gives \(m\) distinct open box edges · Percolation gives open self-avoiding walks of every length · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Simon–Lieb inequality in the infinite-volume plus state

DefinitionOriented edge boundary of a finite lattice set#✓fully proved

The oriented edge boundary ∂S = {(x, x ± e_i) : x ∈ S, x ± e_i ∉ S} of a finite set S ⊆ ℤ^d, as ordered pairs (inner endpoint first).

noncomputable def boundaryEdges (d : ℕ) (S : Finset (Site d)) :
    Finset (Site d × Site d) := by
  classical
  exact
    ((S ×ˢ (Finset.univ : Finset (Fin d)) ×ˢ (Finset.univ : Finset Bool)).filter
        (fun t => coordShift t.1 t.2.1 (stepSign t.2.2) ∉ S)).image
      (fun t => (t.1, coordShift t.1 t.2.1 (stepSign t.2.2)))

Uses 3 · Used by 17

Statement usesSite of the hypercubic lattice · Shift of a lattice site in one coordinate · Sign of a unit lattice step

Used bySupport of the first-exit decomposition events · Duminil-Copin–Tassion differential inequality · Exponential decay below p̃_c · Positivity of the Duminil-Copin–Tassion threshold · Size bound for the edge boundary · Duminil-Copin–Tassion quantity · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · 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 · Simon radius of a finite set · 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

TheoremSize bound for the edge boundary#✓fully proved

The edge boundary of S has at most 2d |S| elements.

theorem card_boundaryEdges_le (S : Finset (Site d)) :
    (boundaryEdges d S).card ≤ S.card * (2 * d)

Uses 4 · Used by 2

Statement usesSite of the hypercubic lattice · Oriented edge boundary of a finite lattice set

Proof usesShift of a lattice site in one coordinate · Sign of a unit lattice step

Used byPositivity of the Duminil-Copin–Tassion threshold · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\)

DefinitionProbability of connection inside a set#✓fully proved

The probability ℙ_p(0 ↔ x inside S) that the origin and x are joined by an open path using only vertices of S; it is 0 if 0 ∉ S or x ∉ S.

noncomputable def connWithinProb (d : ℕ) (p : ℝ≥0) (hp : p ≤ 1) (S : Finset (Site d))
    (x : Site d) : ℝ := by
  classical
  exact
    if h0 : origin d ∈ S then
      if hx : x ∈ S then
        (bernoulliProductMeasure (E := Sym2 (Site d)) p hp).real
          {ω | ConnectedWithin d ω (S : Set (Site d)) ⟨origin d, h0⟩ ⟨x, hx⟩}
      else 0
    else 0

Uses 5 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Connection by an open path within a set · Site of the hypercubic lattice · Origin of the hypercubic lattice · Bernoulli product measure on configuration space

Used byDuminil-Copin–Tassion differential inequality · Exponential decay below p̃_c · Positivity of the Duminil-Copin–Tassion threshold · Duminil-Copin–Tassion quantity

DefinitionDuminil-Copin–Tassion quantity#✓fully proved

The Duminil-Copin–Tassion quantity φ_p(S) = p ∑_{(x, y) ∈ ∂S} ℙ_p(0 ↔ x inside S).

noncomputable def phi (d : ℕ) (p : ℝ≥0) (hp : p ≤ 1) (S : Finset (Site d)) : ℝ :=
  (p : ℝ) * ∑ e ∈ boundaryEdges d S, connWithinProb d p hp S e.1

Uses 3 · Used by 11

Statement usesSite of the hypercubic lattice · Oriented edge boundary of a finite lattice set · Probability of connection inside a set

Used byDuminil-Copin–Tassion differential inequality · Mean-field lower bound · Exponential decay below p̃_c · Exponential decay from a one-step recursion · \(\tilde p_c \le p_c\) if \(\theta = 0\) on the set defining \(\tilde p_c\) · Equality of the Duminil-Copin–Tassion threshold and \(p_c\) · Exponential decay of the one-arm probability below the threshold · Sharpness of the phase transition · Positivity of the Duminil-Copin–Tassion threshold · Densities with a finite set of small Duminil-Copin–Tassion quantity · Percolation quantity \(\varphi_p(S)\) at \(p = 1 - e^{-\beta}\)

DefinitionDensities with a finite set of small Duminil-Copin–Tassion quantity#✓fully proved

The set of densities p ∈ [0, 1] for which some finite S ∋ 0 has φ_p(S) < 1.

def tildePcSet (d : ℕ) : Set ℝ≥0 :=
  {p : ℝ≥0 | ∃ hp : p ≤ 1, ∃ S : Finset (Site d), origin d ∈ S ∧ phi d p hp S < 1}

Uses 3 · Used by 8

Statement usesSite of the hypercubic lattice · Origin of the hypercubic lattice · Duminil-Copin–Tassion quantity

Used byMean-field lower bound · \(\tilde p_c \le p_c\) if \(\theta = 0\) on the set defining \(\tilde p_c\) · Sharpness of the phase transition, conditional form · Equality of the Duminil-Copin–Tassion threshold and \(p_c\) · Exponential decay of the one-arm probability below the threshold · Sharpness of the phase transition · Positivity of the Duminil-Copin–Tassion threshold · Duminil-Copin–Tassion threshold

DefinitionDuminil-Copin–Tassion threshold#✓fully proved

The Duminil-Copin–Tassion threshold p̃_c(d) = sup {p : ∃ S ∋ 0 finite, φ_p(S) < 1}.

noncomputable def tildePc (d : ℕ) : ℝ≥0 :=
  sSup (tildePcSet d)

Uses 1 · Used by 8

Statement usesDensities with a finite set of small Duminil-Copin–Tassion quantity

Used byAuxiliary critical inverse temperature from \(\tilde p_c\) · Mean-field lower bound · \(p_c \le \tilde p_c\) if \(\theta > 0\) above \(\tilde p_c\) · \(\tilde p_c \le p_c\) if \(\theta = 0\) on the set defining \(\tilde p_c\) · Sharpness of the phase transition, conditional form · Equality of the Duminil-Copin–Tassion threshold and \(p_c\) · Sharpness of the phase transition · Positivity of the Duminil-Copin–Tassion threshold

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.