Duminil-Copin–Tassion differential inequality

DefinitionEvent of a connection inside a finite set#✓fully proved

The event {o ↔ x inside S}: o and x lie in S and are joined by an open path in S.

def withinConnEvent (d : ℕ) (S : Set (Site d)) (o x : Site d) :
    Set (ConfigSpace (Sym2 (Site d))) :=
  {ω | ∃ (ho : o ∈ S) (hx : x ∈ S), ConnectedWithin d ω S ⟨o, ho⟩ ⟨x, hx⟩}

Uses 3 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Connection by an open path within a set · Site of the hypercubic lattice

Used byDuminil-Copin–Tassion differential inequality · Exponential decay below p̃_c

DefinitionPairs of sites of a finite set#✓fully proved

All unordered pairs of sites of the finite set S.

noncomputable def edgesWithinFinset (S : Finset (Site d)) : Finset (Sym2 (Site d)) :=
  (S ×ˢ S).image (fun p => s(p.1, p.2))

Uses 1 · Used by 5

Statement usesSite of the hypercubic lattice

Used bySupport of the first-exit decomposition events · Pairs of box sites outside a given set · Duminil-Copin–Tassion differential inequality · Box edges with no endpoint in a cluster · Exponential decay below p̃_c

DefinitionPairs of sites of a lattice box#✓fully proved

All unordered pairs of sites of Λ_n (containing the lattice edges of Λ_n).

noncomputable def boxEdgeFinset (d n : ℕ) : Finset (Sym2 (Site d)) :=
  ((boxFinset d n) ×ˢ (boxFinset d n)).image (fun p => s(p.1, p.2))

Uses 2 · Used by 5

Statement usesSite of the hypercubic lattice · Lattice box as a finite set

Used byPairs of box sites outside a given set · Box-crossing probability as a polynomial in the density · Duminil-Copin–Tassion differential inequality · Mean-field lower bound · Sharpness of the phase transition

DefinitionBox-crossing event#✓fully proved

The event that the origin is joined by an open path inside Λ_n to the vertex boundary of Λ_n.

def boxCrossingEvent (d n : ℕ) : Set (ConfigSpace (Sym2 (Site d))) :=
  {ω | ∃ (x : Site d) (hx : x ∈ box d n), x ∈ vertexBoundary d n ∧
       ∃ (h0 : origin d ∈ box d n),
         ConnectedWithin d ω (box d n) ⟨origin d, h0⟩ ⟨x, hx⟩}

Uses 6 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Connection by an open path within a set · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Inner vertex boundary of a box · Origin of the hypercubic lattice

Used byBox-crossing probability · Box-crossing probability as a polynomial in the density · Duminil-Copin–Tassion differential inequality · Mean-field lower bound · Sharpness of the phase transition

DefinitionBox-crossing probability#✓fully proved

The probability of boxCrossingEvent d n.

noncomputable def boxCrossProb (d : ℕ) (p : ℝ≥0) (hp : p ≤ 1) (n : ℕ) : ℝ :=
  (bernoulliProductMeasure (E := Sym2 (Site d)) p hp).real (boxCrossingEvent d n)

Uses 4 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Box-crossing event · Bernoulli product measure on configuration space

Used byDuminil-Copin–Tassion differential inequality · Mean-field lower bound · Sharpness of the phase transition

DefinitionPivotal edge event#✓fully proved

The event that the edge e is pivotal for A (flipping e changes whether A occurs).

def pivotalEvent (e : Sym2 (Site d)) (A : Set (ConfigSpace (Sym2 (Site d)))) :
    Set (ConfigSpace (Sym2 (Site d))) :=
  {ω | IsPivotal e A ω}

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Pivotal coordinate for an event · Site of the hypercubic lattice

Used byDuminil-Copin–Tassion differential inequality

DefinitionConnection of a site to the box boundary#✓fully proved

x ∈ Λ_n is joined by an open path inside Λ_n to a site of the vertex boundary of Λ_n.

def connBdry (d n : ℕ) (ω : ConfigSpace (Sym2 (Site d))) (x : Site d) : Prop :=
  ∃ (hx : x ∈ box d n) (y : Site d) (hy : y ∈ box d n),
    y ∈ vertexBoundary d n ∧ ConnectedWithin d ω (box d n) ⟨x, hx⟩ ⟨y, hy⟩

Uses 5 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Connection by an open path within a set · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Inner vertex boundary of a box

Used byDuminil-Copin–Tassion differential inequality · Set of sites not connected to the box boundary

DefinitionSet of sites not connected to the box boundary#✓fully proved

The random set 𝒮(ω) of sites of Λ_n not joined inside Λ_n to the vertex boundary.

noncomputable def surfaceSet (d n : ℕ) (ω : ConfigSpace (Sym2 (Site d))) : Finset (Site d) := by
  classical
  exact (boxFinset d n).filter (fun x => ¬ connBdry d n ω x)

Uses 4 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Lattice box as a finite set · Connection of a site to the box boundary

Used byDuminil-Copin–Tassion differential inequality · Event that the unconnected set equals a given set

DefinitionEvent that the unconnected set equals a given set#✓fully proved

The event {𝒮 = S}.

def surfaceEvent (d n : ℕ) (S : Finset (Site d)) : Set (ConfigSpace (Sym2 (Site d))) :=
  {ω | surfaceSet d n ω = S}

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Set of sites not connected to the box boundary

Used byDuminil-Copin–Tassion differential inequality

DefinitionPairs of box sites outside a given set#✓fully proved

The pairs of sites of Λ_n that are not pairs of sites of S.

noncomputable def boxEdgesOutside (d n : ℕ) (S : Finset (Site d)) : Finset (Sym2 (Site d)) :=
  (boxEdgeFinset d n) \ (edgesWithinFinset S)

Uses 3 · Used by 1

Statement usesSite of the hypercubic lattice · Pairs of sites of a lattice box · Pairs of sites of a finite set

Used byDuminil-Copin–Tassion differential inequality

TheoremDuminil-Copin–Tassion differential inequality#✓fully proved

The Duminil-Copin–Tassion differential inequality: if φ_p(S) ≥ m for every finite S ∋ 0, then d/dp ℙ_p(A_n) ≥ (p(1 - p))⁻¹ m (1 - ℙ_p(A_n)) for 0 < p < 1 and n ≥ 1 (Duminil-Copin–Tassion 2016).

theorem dct_differential_inequality (p : ℝ≥0) (hp : p ≤ 1) (n : ℕ) (hn : 1 ≤ n)
    (hp0 : 0 < (p : ℝ)) (hp1 : (p : ℝ) < 1) (m : ℝ)
    (hm : ∀ S : Finset (Site d), origin d ∈ S → m ≤ phi d p hp S) :
    deriv (fun q => prob q ((boxEdgeFinset d n).restrict '' (boxCrossingEvent d n))) (p : ℝ)
      ≥ (1 / ((p : ℝ) * (1 - (p : ℝ)))) * m * (1 - boxCrossProb d p hp n)

Uses 49 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Box-crossing probability · Box-crossing event · Pairs of sites of a lattice box · Origin of the hypercubic lattice · Duminil-Copin–Tassion quantity · Bernoulli weight of an event

Proof usesIncreasing event · Pivotal coordinate for an event · Connection by an open path within a set · Open lattice edge of a bond configuration · Box \((-n, n)^d\) in the hypercubic lattice · Open connection within a set is monotone in the set · Hypercubic lattice \(\mathbb{Z}^d\) · Open subgraph of a bond configuration · Open subgraph induced on a set of sites · Inner vertex boundary of a box · Product weight of an edge configuration · Oriented edge boundary of a finite lattice set · Pairs of box sites outside a given set · Lattice box as a finite set · Connection of a site to the box boundary · Probability of connection inside a set · Shift of a lattice site in one coordinate · Pairs of sites of a finite set · Pivotal edge event · Sign of a unit lattice step · Event that the unconnected set equals a given set · Set of sites not connected to the box boundary · Bernoulli weight of a single edge · Event of a connection inside a finite set · Expectation under Bernoulli product weights · Bernoulli distribution on the Booleans · Bernoulli product measure on configuration space · Probability of an event as a sum of configuration masses · Mass of a configuration under a finite Bernoulli product measure, real form · Bernoulli product weight of a configuration · Russo's formula · Events depending on finitely many coordinates are cylinders · Configuration patched from one configuration on a finite set and another off it · Pivotality depends only on the other coordinates · Pivotal coordinates of an increasing event · Weight of the event that a coordinate is pivotal · Bernoulli product measure of a cylinder event, real-valued form · Probability of a finitely dependent event as a polynomial in \(p\) · Probability of a finitely dependent event as a finite weight · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Used byMean-field lower bound · Sharpness of the phase transition

DefinitionBox-crossing probability as a polynomial in the density#✓fully proved

The polynomial t ↦ ℙ_t(A_{n+1}) (the box-crossing probability as a polynomial in the density), defined for all real t.

noncomputable def crossPoly (d n : ℕ) (t : ℝ) : ℝ :=
  prob t ((boxEdgeFinset d (n + 1)).restrict '' (boxCrossingEvent d (n + 1)))

Uses 5 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Box-crossing event · Pairs of sites of a lattice box · Bernoulli weight of an event

Used byMean-field lower bound · Sharpness of the phase transition

TheoremMean-field lower bound#✓fully proved

Mean-field lower bound (Duminil-Copin–Tassion 2016): for p̃_c < q < 1 (with p̃_c > 0), θ(q) ≥ (q - p̃_c) / (q(1 - p̃_c)).

theorem theta_ge_meanField_of_tildePc_lt (q : ℝ≥0) (hq : q ≤ 1)
    (htpc0 : 0 < (tildePc d : ℝ)) (hgt : tildePc d < q) (hq1 : (q : ℝ) < 1) :
    theta d q hq ≥ ((q : ℝ) - (tildePc d : ℝ)) / ((q : ℝ) * (1 - (tildePc d : ℝ)))

Uses 34

Statement usesPercolation probability of bond percolation · Duminil-Copin–Tassion threshold

Proof usesConfiguration space of a statistical-mechanics model · Connection by an open path · Connection by an open path within a set · Open lattice edge of a bond configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Open cluster of a site · Open connection within a set is monotone in the set · Every finite set of sites lies in a box · Hypercubic lattice \(\mathbb{Z}^d\) · Open subgraph of a bond configuration · Open subgraph induced on a set of sites · Inner vertex boundary of a box · Box-crossing probability · Box-crossing event · Pairs of sites of a lattice box · Lattice box as a finite set · Box-crossing probability as a polynomial in the density · One-arm probability · One-arm probability as a function of a real density · One-arm event from the origin · Duminil-Copin–Tassion differential inequality · Measurability of the one-arm event · Origin of the hypercubic lattice · Percolation event for the origin · Duminil-Copin–Tassion quantity · Densities with a finite set of small Duminil-Copin–Tassion quantity · Bernoulli distribution on the Booleans · Bernoulli product measure on configuration space · Differentiability in \(p\) of the probability of a cylinder event · Bernoulli weight of an event · Probability of a finitely dependent event as a finite weight

DefinitionEdges of \(\mathbb{Z}^d\) inside a set#✓fully proved

The edges of ℤ^d with both endpoints in S.

def internalEdges (S : Set (Site d)) : Set (Sym2 (Site d)) :=
  {e | ∃ x ∈ S, ∃ y ∈ S, e = s(x, y)}

Uses 1

Statement usesSite of the hypercubic lattice

DefinitionEvent that a vertex is connected to a target set#✓fully proved

The event that o is connected to B.

def mpiCrossingEvent (o : V) (B : Set V) : Set (ConfigSpace (Sym2 V)) :=
  connEvent G Set.univ o B

Uses 2 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Connection event inside a set

Used byMean-field differential inequality for inhomogeneous percolation

DefinitionVertices not connected to a target set#✓fully proved

The set of vertices not connected to B in ω.

noncomputable def mpiBlockedSet (B : Set V) (omega : ConfigSpace (Sym2 V)) : Finset V :=
  by
    classical
    exact Finset.univ.filter fun x => ¬ ConnToSet G omega Set.univ x B

Uses 2 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Open connection inside a set to a target set

Used byAizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Mean-field differential inequality for inhomogeneous percolation · Event that the set of vertices not connected to \(B\) is \(S\)

DefinitionEvent that the set of vertices not connected to \(B\) is \(S\)#✓fully proved

The event that the set of vertices not connected to B is exactly S.

def mpiSurfaceEvent (B : Set V) (S : Finset V) : Set (ConfigSpace (Sym2 V)) :=
  {omega | mpiBlockedSet G B omega = S}

Uses 2 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Vertices not connected to a target set

Used byAizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Mean-field differential inequality for inhomogeneous percolation

DefinitionEdges with both endpoints in a vertex set#✓fully proved

The edges with both endpoints in S.

def mpiInternalEdges (S : Set V) : Set (Sym2 V) :=
  {e | ∃ x ∈ S, ∃ y ∈ S, e = s(x, y)}

Used by 3

Used byAizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Mean-field differential inequality for inhomogeneous percolation

DefinitionInhomogeneous Duminil-Copin–Tassion quantity \(\varphi(S)\)#✓fully proved

The inhomogeneous Duminil-Copin–Tassion quantity φ(S) = ∑_{(x,y) ∈ ∂S} (1 - e^{-βJ_{xy}}) P(o ↔ x in S).

noncomputable def mpiPhi (beta : ℝ) (J : Sym2 V → ℝ)
    (o : V) (S : Finset V) : ℝ :=
  ∑ q ∈ shk_boundaryPairs G S,
    (1 - Real.exp (-beta * J s(q.1, q.2))) *
      wprob (shk_edgeLaw beta J) (connEvent G (S : Set V) o {q.1})

Uses 4 · Used by 1

Statement usesConnection event inside a set · Ordered boundary pairs of a set · Edge law of inhomogeneous bond percolation · Weighted probability of an event

Used byMean-field differential inequality for inhomogeneous percolation

DefinitionEvent that an edge is closed and pivotal#✓fully proved

The event that e is closed and pivotal for A.

def mpiPivotalClosed (e : Sym2 V) (A : Set (ConfigSpace (Sym2 V))) :
    Set (ConfigSpace (Sym2 V)) :=
  {omega | IsPivotal e A omega ∧ omega e = false}

Uses 2 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Pivotal coordinate for an event

Used byMean-field differential inequality for inhomogeneous percolation

DefinitionProduct of the edge laws over all other edges#✓fully proved

The product of the edge laws over all edges other than e.

noncomputable def mpiWeightOff (beta : ℝ) (J : Sym2 V → ℝ)
    (e : Sym2 V) (omega : ConfigSpace (Sym2 V)) : ℝ :=
  ∏ j ∈ Finset.univ.erase e, shk_edgeLaw beta J j (omega j)

Uses 2 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Edge law of inhomogeneous bond percolation

Used byMean-field differential inequality for inhomogeneous percolation

LemmaMean-field differential inequality for inhomogeneous percolation#✓fully proved

The mean-field differential inequality for inhomogeneous percolation: Russo's formula ∂_β P(o ↔ B) = ∑_e J_e P(e closed pivotal) and, if φ(S) ≥ m for all S ∋ o, (m/β)(1 - P(o ↔ B)) ≤ ∂_β P(o ↔ B). Reference: H. Duminil-Copin, V. Tassion, "A new proof of the sharpness of the phase transition for Bernoulli percolation and the Ising model", Comm. Math. Phys. 343 (2016) 725–745.

lemma mpi_meanfield_perco (beta : ℝ) (J : Sym2 V → ℝ)
    (hbeta : 0 < beta) (hJ : ∀ e, 0 ≤ J e)
    (o : V) (B : Set V) (m : ℝ)
    (hm : ∀ S : Finset V, o ∈ S → m ≤ mpiPhi G beta J o S) :
    HasDerivAt
        (fun b => wprob (shk_edgeLaw b J) (mpiCrossingEvent G o B))
        (∑ e, J e * wprob (shk_edgeLaw beta J)
          (mpiPivotalClosed e (mpiCrossingEvent G o B))) beta ∧
      (1 / beta) * m *
          (1 - wprob (shk_edgeLaw beta J) (mpiCrossingEvent G o B)) ≤
        ∑ e, J e * wprob (shk_edgeLaw beta J)
          (mpiPivotalClosed e (mpiCrossingEvent G o B))

Uses 36

Statement usesEvent that a vertex is connected to a target set · Inhomogeneous Duminil-Copin–Tassion quantity \(\varphi(S)\) · Event that an edge is closed and pivotal · Edge law of inhomogeneous bond percolation · Weighted probability of an event

Proof usesConfiguration space of a statistical-mechanics model · Event determined by a set of coordinates · Edge parameters \(p_e(\beta) = 1 - e^{-\beta J_e}\) · Derivative in \(\beta\) of the edge parameter \(1 - e^{-\beta J}\) · Increasing event · Pivotal coordinate for an event · Occurrence of an event on a coordinate set · Open connection inside a set to a target set · Open connection between two vertices inside a set · Connection event inside a set · Event that an edge is open · Vertices not connected to a target set · Edges with both endpoints in a vertex set · Event that the set of vertices not connected to \(B\) is \(S\) · Product of the edge laws over all other edges · Open subgraph of a configuration · Ordered boundary pairs of a set · Agreement of configurations on a set · Agreement on a set restricts to subsets · Transitivity of agreement on a set · Disjoint occurrence of events · Disjoint occurrence lies in the intersection · Pivotality depends only on the other coordinates · Pivotal coordinates of an increasing event · Product weight of a configuration · Nonnegativity of the product weight · Closing a coordinate of a configuration · Opening a coordinate of a configuration · Product probability weight has total mass one · Independence of events determined by disjoint coordinate sets · Monotonicity of the weighted probability

22 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.