Mean-field lower bound and critical points for Bernoulli percolation

3 fully proved

B. The mean-field lower bound

LemmaMean-field lower bound for \(\theta(p)\) from a differential inequality#✓fully proved

The mean-field lower bound θ(p) ≥ (p - p₀)/(p(1 - p₀)) from the differential inequality for crossing probabilities. 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 item1_meanfield_lower_bound (p : ℝ≥0) (hp : p ≤ 1)
    (p₀ : ℝ) (hp₀ : 0 < p₀) (hp₀1 : p₀ < 1)
    (f : ℕ → ℝ → ℝ)
    (hfval : ∀ n, f n (p : ℝ) = crossProb d p hp n)
    (hdiff : ∀ n, ∀ q ∈ Ico p₀ 1, DifferentiableAt ℝ (f n) q)
    (hineq : ∀ n, ∀ q ∈ Ioo p₀ 1, (1 / (q * (1 - q))) * (1 - f n q) ≤ deriv (f n) q)
    (hf0 : ∀ n, 0 ≤ f n p₀)
    (hpp₀ : p₀ ≤ (p : ℝ)) (hp1 : (p : ℝ) < 1)
    (htends : Tendsto (fun n => crossProb d p hp n) atTop (𝓝 (theta d p hp))) :
    ((p : ℝ) - p₀) / ((p : ℝ) * (1 - p₀)) ≤ theta d p hp

Uses 2

Statement usesOne-arm probability · Percolation probability of bond percolation

C. Critical points

Lemma\(p_c \le \tilde p_c\) if \(\theta > 0\) above \(\tilde p_c\)#✓fully proved

p_c ≤ p̃_c when θ is positive above p̃_c. See also Percolation.pc_le_tildePc (MathlibExt), stated with hypotheses on θ(1) and on (p̃_c, 1).

lemma pc_le_tildePc
    (hpos : ∀ t : ℝ≥0, tildePc d < t → ∀ ht : t ≤ 1, 0 < theta d t ht) :
    pc d ≤ tildePc d

Uses 4

Statement usesCritical probability of bond percolation on the hypercubic lattice · Percolation probability of bond percolation · Duminil-Copin–Tassion threshold

Proof usesSet of densities with no percolation

Lemma\(\tilde p_c \le p_c\) if \(\theta = 0\) on the set defining \(\tilde p_c\)#✓fully proved

p̃_c ≤ p_c when θ vanishes on the set defining p̃_c. See also Percolation.tildePc_le_pc (MathlibExt), stated with exponential decay of crossing probabilities.

lemma tildePc_le_pc
    (hzero : ∀ t ∈ tildePcSet d, ∀ ht : t ≤ 1, theta d t ht = 0) :
    tildePc d ≤ pc d

Uses 8

Statement usesCritical 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 usesSite of the hypercubic lattice · Origin of the hypercubic lattice · Duminil-Copin–Tassion quantity · Set of densities with no percolation

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.