Sharpness of the phase transition for Bernoulli bond percolation on ℤ^d

TheoremPositivity of the Duminil-Copin–Tassion threshold#✓fully proved

p̃_c(d) > 0 for d ≥ 1: at p = 1/(4d + 1), φ_p({0}) ≤ 2dp < 1.

theorem tildePc_pos (hd : 0 < d) : 0 < (tildePc d : ℝ)

Uses 12 · Used by 1

Statement usesDuminil-Copin–Tassion threshold

Proof usesConfiguration space of a statistical-mechanics model · Connection by an open path within a set · Site of the hypercubic lattice · Oriented edge boundary of a finite lattice set · Size bound for the edge boundary · Probability of connection inside a set · Origin of the hypercubic lattice · 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

Used bySharpness of the phase transition

DefinitionStraight path along the first coordinate axis#✓fully proved

The direction sequence of the straight path from the origin along the first coordinate axis.

noncomputable def lineWord (hd : 0 < d) : ℕ → Fin d × Bool := fun _ => (⟨0, hd⟩, true)

Used by 1

Used bySharpness of the phase transition

TheoremExponential decay of the one-arm probability below the threshold#✓fully proved

Exponential decay of the one-arm probability for every p ∈ tildePcSet d, i.e. every p admitting a finite S ∋ 0 with φ_p(S) < 1.

theorem crossProb_exp_decay_of_mem_tildePcSet :
    ∀ p ∈ tildePcSet d, ∀ hp : p ≤ 1,
      ∃ c > 0, ∃ C > 0, ∀ n, crossProb d p hp n ≤ C * Real.exp (-c * n)

Uses 8 · Used by 1

Statement usesOne-arm probability · Densities with a finite set of small Duminil-Copin–Tassion quantity

Proof usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Every finite set of sites lies in a box · Exponential decay below p̃_c · Origin of the hypercubic lattice · Duminil-Copin–Tassion quantity

Used bySharpness of the phase transition

TheoremSharpness of the phase transition#✓fully proved

Sharpness of the phase transition for Bernoulli bond percolation on ℤ^d, d ≥ 1 (Duminil-Copin–Tassion 2016; Aizenman–Barsky 1987; Menshikov 1986):

1. p̃_c = p_c;
2. for every p ∈ tildePcSet d (a finite S ∋ 0 has φ_p(S) < 1), ℙ_p(0 ↔ ℤ^d \ Λ_{n-1}) ≤ C e^{-cn} for some c, C > 0;
3. θ(q) ≥ (q - p̃_c)/(q(1 - p̃_c)) for p̃_c < q < 1.

Scope of the items: * Item 2 is stated on tildePcSet d, not on [0, p_c): passing from p < p̃_c to p ∈ tildePcSet d needs monotonicity of p ↦ φ_p(S), and passing from p < p_c to θ(p) = 0 needs monotonicity of θ; neither is proved in MathlibExt (θ monotonicity is theta_mono_parameter in PhyslibExt RandomCluster/PcUpperViaFK). * Item 3 is informative only when p̃_c < 1. This file does not prove that for any d; at d = 1 it fails (p̃_c = p_c = 1) and item 3 is vacuous. For d = 2, p_c < 1 is proved in PhyslibExt (StatMech.Percolation.pc_two_lt_one_via_fk), which with item 1 makes item 3 non-vacuous there.

theorem sharp_phase_transition (hd : 0 < d) :
    tildePc d = pc d ∧
      (∀ p ∈ tildePcSet d, ∀ hp : p ≤ 1,
        ∃ c > 0, ∃ C > 0, ∀ n, crossProb d p hp n ≤ C * Real.exp (-c * n)) ∧
      (∀ q : ℝ≥0, ∀ hq : q ≤ 1, tildePc d < q → (q : ℝ) < 1 →
        theta d q hq ≥ ((q : ℝ) - (tildePc d : ℝ)) / ((q : ℝ) * (1 - (tildePc d : ℝ))))

Uses 44

Statement usesOne-arm probability · Critical probability of bond percolation on the hypercubic lattice · Percolation probability of bond percolation · Duminil-Copin–Tassion threshold · Densities with a finite set of small Duminil-Copin–Tassion quantity

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 · Shift of a lattice site in one coordinate · Box-crossing probability as a polynomial in the density · One-arm probability as a function of a real density · Exponential decay of the one-arm probability below the threshold · One-arm event from the origin · Duminil-Copin–Tassion differential inequality · Edges of a lattice path encoded by a step sequence · Straight path along the first coordinate axis · Measurability of the one-arm event · Origin of the hypercubic lattice · Percolation event for the origin · Duminil-Copin–Tassion quantity · Sharpness of the phase transition, conditional form · Sign of a unit lattice step · Positivity of the Duminil-Copin–Tassion threshold · Vertices of a lattice path encoded by a step sequence · Event that an encoded lattice path is open · 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

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.