Sharpness of the phase transition, assuming its two analytic inputs

DefinitionOne-arm probability as a function of a real density#✓fully proved

The one-arm probability crossProb d t n as a function of a real density t (0 outside [0, 1]).

noncomputable def crossProbReal (d n : ℕ) (t : ℝ) : ℝ :=
  if ht : 0 ≤ t ∧ t ≤ 1 then crossProb d t.toNNReal (Real.toNNReal_le_one.mpr ht.2) n else 0

Uses 1 · Used by 3

Statement usesOne-arm probability

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

TheoremEquality of the Duminil-Copin–Tassion threshold and \(p_c\)#✓fully proved

p̃_c = p_c, assuming exponential decay on tildePcSet, θ(1) ≠ 0, and θ(q) > 0 for p̃_c < q < 1.

theorem tildePc_eq_pc
    (htheta_one : ∀ h1 : (1 : ℝ≥0) ≤ 1, theta d 1 h1 ≠ 0)
    (hsub : ∀ p ∈ tildePcSet d, ∀ hp : p ≤ 1,
        ∃ c > 0, ∃ C > 0, ∀ n, crossProb d p hp n ≤ C * Real.exp (-c * n))
    (hmf : ∀ q : ℝ≥0, ∀ hq : q ≤ 1, tildePc d < q → (q : ℝ) < 1 → 0 < theta d q hq) :
    tildePc d = pc d

Uses 19 · Used by 1

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 · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Open cluster of a site · Every finite set of sites lies in a box · One-arm event from the origin · Measurability of the one-arm event · Origin of the hypercubic lattice · Percolation event for the origin · Duminil-Copin–Tassion quantity · Set of densities with no percolation · Bernoulli distribution on the Booleans · Bernoulli product measure on configuration space

Used bySharpness of the phase transition, conditional form

TheoremSharpness of the phase transition, conditional form#✓fully proved

Sharpness of the phase transition, conditional form: from p̃_c > 0, θ(1) ≠ 0, exponential decay of the one-arm probability on tildePcSet, and the Duminil-Copin–Tassion differential inequality on (p̃_c, q) (with continuity and derivative hypotheses), conclude p̃_c = p_c, exponential decay on tildePcSet, and θ(q) ≥ (q - p̃_c)/(q(1 - p̃_c)) for p̃_c < q < 1. The hypotheses are discharged in sharp_phase_transition.

StatMech.Percolation.sharpness · 17 lines

theorem sharpness (htildePc_pos : 0 < (tildePc d : ℝ))
    (htheta_one : ∀ h1 : (1 : ℝ≥0) ≤ 1, theta d 1 h1 ≠ 0)
    (hsub : ∀ p ∈ tildePcSet d, ∀ hp : p ≤ 1,
        ∃ c > 0, ∃ C > 0, ∀ n, crossProb d p hp n ≤ C * Real.exp (-c * n))
    (F' : ℕ → ℝ≥0 → ℝ → ℝ)
    (hcont : ∀ q : ℝ≥0, tildePc d < q → (q : ℝ) < 1 → ∀ n,
        ContinuousOn (crossProbReal d (n + 1)) (Icc (tildePc d : ℝ) (q : ℝ)))
    (hderiv : ∀ q : ℝ≥0, tildePc d < q → (q : ℝ) < 1 → ∀ n,
        ∀ t ∈ Ioo (tildePc d : ℝ) (q : ℝ), HasDerivAt (crossProbReal d (n + 1)) (F' n q t) t)
    (hdiffineq : ∀ q : ℝ≥0, tildePc d < q → (q : ℝ) < 1 → ∀ n,
        ∀ t ∈ Ioo (tildePc d : ℝ) (q : ℝ),
        F' n q t ≥ (1 / (t * (1 - t))) * (1 - crossProbReal d (n + 1) t)) :
    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 19 · Used by 1

Statement usesOne-arm probability · One-arm probability as a function of a real density · 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 · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Open cluster of a site · Every finite set of sites lies in a box · One-arm event from the origin · Measurability of the one-arm event · Origin of the hypercubic lattice · Percolation event for the origin · Equality of the Duminil-Copin–Tassion threshold and \(p_c\) · Bernoulli distribution on the Booleans · Bernoulli product measure on configuration space

Used bySharpness of the phase transition

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.