Exponential decay below the critical point

DefinitionBernoulli weight of a single edge#✓fully proved

The Bernoulli(p) weight of a single edge state: p for open, 1 - p for closed.

noncomputable def w1 (p : ℝ≥0) (hp : p ≤ 1) (b : Bool) : ℝ := (bernoulliMeasure p hp).real {b}

Uses 1 · Used by 4

Statement usesBernoulli distribution on the Booleans

Used byDuminil-Copin–Tassion differential inequality · Exponential decay below p̃_c · Exploration independence of a cluster inside a set · Product weight of an edge configuration

DefinitionProduct weight of an edge configuration#✓fully proved

The product weight ∏_e w1(ω_e) of a configuration on a finite edge set.

noncomputable def W (p : ℝ≥0) (hp : p ≤ 1) (ω : ConfigSpace E) : ℝ := ∏ e, w1 p hp (ω e)

Uses 2 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli weight of a single edge

Used byDuminil-Copin–Tassion differential inequality · Exponential decay below p̃_c · Exploration independence of a cluster inside a set · Expectation under Bernoulli product weights

DefinitionExpectation under Bernoulli product weights#✓fully proved

The expectation ∑_ω f(ω) W(ω) of f under the Bernoulli(p) product weights on a finite edge set.

noncomputable def wsum (p : ℝ≥0) (hp : p ≤ 1) (f : ConfigSpace E → ℝ) : ℝ :=
  ∑ ω : ConfigSpace E, f ω * W p hp ω

Uses 2 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Product weight of an edge configuration

Used byDuminil-Copin–Tassion differential inequality · Exponential decay below p̃_c · Exploration independence of a cluster inside a set

DefinitionOpen cluster of a site inside a set#✓fully proved

The open cluster C_S(o) of o inside S: sites of S joined to o by an open path in S.

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

Uses 3 · Used by 3

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

Used byEvent that the cluster of the origin inside a set equals a given set · Exponential decay below p̃_c · Exploration independence of a cluster inside a set

DefinitionEdges from a subset into a set#✓fully proved

The set of edges {x, y} with x ∈ K and y ∈ S.

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

Uses 1 · Used by 2

Statement usesSite of the hypercubic lattice

Used byExponential decay below p̃_c · Exploration independence of a cluster inside a set

DefinitionEvent that the cluster of the origin inside a set equals a given set#✓fully proved

The event {C_S(o) = K} that the open cluster of o inside S is exactly K.

def clusterEvent (d : ℕ) (S : Set (Site d)) (o : Site d) (K : Set (Site d)) :
    Set (ConfigSpace (Sym2 (Site d))) :=
  {ω | clusterWithin d ω S o = K}

Uses 3 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Open cluster of a site inside a set

Used byExponential decay below p̃_c · Exploration independence of a cluster inside a set

DefinitionEdges joining a finite set to a region#✓fully proved

The finite set of edges {x, y} with x ∈ K and y ∈ S.

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

Uses 1 · Used by 2

Statement usesSite of the hypercubic lattice

Used byExponential decay below p̃_c · Exploration independence of a cluster inside a set

TheoremExploration independence of a cluster inside a set#✓fully proved

Exploration independence: for K ⊆ S finite and an event B depending only on edges in U, disjoint from the edges between K and S, ℙ_p(C_S(o) = K, B) = ℙ_p(C_S(o) = K) ℙ_p(B).

theorem exploration_decomposition (p : ℝ≥0) (hp : p ≤ 1)
    (S : Finset (Site d)) (o : Site d) (hoS : o ∈ (S : Set (Site d))) (K : Finset (Site d))
    (B : Set (ConfigSpace (Sym2 (Site d)))) (U : Finset (Sym2 (Site d)))
    (hdisj : Disjoint (incidentWithinFinset K S) U)
    (hB : DependsOn (B.indicator (fun _ => (1 : ℝ))) (U : Set (Sym2 (Site d)))) :
    (bernoulliProductMeasure (E := Sym2 (Site d)) p hp).real
        (clusterEvent d (S : Set (Site d)) o (K : Set (Site d)) ∩ B)
      = (bernoulliProductMeasure (E := Sym2 (Site d)) p hp).real
          (clusterEvent d (S : Set (Site d)) o (K : Set (Site d)))
        * (bernoulliProductMeasure (E := Sym2 (Site d)) p hp).real B

Uses 20

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Event that the cluster of the origin inside a set equals a given set · Edges joining a finite set to a region · Bernoulli product measure on configuration space

Proof usesConnection by an open path within a set · Open lattice edge of a bond configuration · Hypercubic lattice \(\mathbb{Z}^d\) · Open subgraph induced on a set of sites · Product weight of an edge configuration · Open cluster of a site inside a set · Edges from a subset into a set · Bernoulli weight of a single edge · Expectation under Bernoulli product weights · Bernoulli distribution on the Booleans · Probability of an event as a sum of configuration masses · Mass of a configuration under a finite Bernoulli product measure, real form · Events depending on finitely many coordinates are cylinders · Configuration patched from one configuration on a finite set and another off it · Bernoulli product measure of a cylinder event, real-valued form

DefinitionCrossing to the box exterior that avoids a cluster#✓fully proved

y ∉ C is joined by an open path avoiding C to a site outside Λ_{n-1}.

def offClusterCrossing (d : ℕ) (C : Set (Site d)) (y : Site d) (n : ℕ)
    (ω : ConfigSpace (Sym2 (Site d))) : Prop :=
  ∃ v, v ∉ box d (n - 1) ∧ ∃ (hy : y ∉ C) (hv : v ∉ C),
    ConnectedWithin d ω {z | z ∉ C} ⟨y, hy⟩ ⟨v, hv⟩

Uses 4

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

DefinitionOpen boundary edge of a cluster#✓fully proved

The edge {x, y} is open, with x ∈ C and y ∉ C.

def boundaryOpen (d : ℕ) (C : Set (Site d)) (x y : Site d)
    (ω : ConfigSpace (Sym2 (Site d))) : Prop :=
  x ∈ C ∧ y ∉ C ∧ IsOpenEdge d ω x y

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Open lattice edge of a bond configuration · Site of the hypercubic lattice

Used byExponential decay below p̃_c

DefinitionCrossing inside the box that avoids a cluster#✓fully proved

y ∈ Λ_n \ C is joined by an open path inside Λ_n \ C to a site outside Λ_{n-1}.

def offClusterBoxCrossing (d : ℕ) (C : Set (Site d)) (y : Site d) (n : ℕ)
    (ω : ConfigSpace (Sym2 (Site d))) : Prop :=
  ∃ z, z ∉ box d (n - 1) ∧ ∃ (hy : y ∈ box d n \ C) (hz : z ∈ box d n \ C),
    ConnectedWithin d ω (box d n \ C) ⟨y, hy⟩ ⟨z, hz⟩

Uses 4 · Used by 1

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

Used byExponential decay below p̃_c

DefinitionBox edges with no endpoint in a cluster#✓fully proved

The edges of Λ_n with no endpoint in C.

noncomputable def boxOffCEdges (d : ℕ) (C : Set (Site d)) (n : ℕ) :
    Finset (Sym2 (Site d)) := by
  classical
  exact (edgesWithinFinset (boxFinset d n)).filter (fun e => ∀ z ∈ e, z ∉ C)

Uses 3 · Used by 1

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

Used byExponential decay below p̃_c

DefinitionOne-arm event from the origin#✓fully proved

The event {0 ↔ ℤ^d \ Λ_{n-1}} that the origin is joined by an open path to a site outside Λ_{n-1}.

def crossingEvent (d n : ℕ) : Set (ConfigSpace (Sym2 (Site d))) :=
  {ω | ∃ v, Connected d ω (origin d) v ∧ v ∉ box d (n - 1)}

Uses 5 · Used by 17

Statement 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 · Origin of the hypercubic lattice

Used byMeasurability of the one-arm event · Mean-field lower bound · One-arm probability · Exponential decay below p̃_c · Exponential decay from a one-step recursion · Sharpness of the phase transition, conditional form · Equality of the Duminil-Copin–Tassion threshold and \(p_c\) · Sharpness of the phase transition · Measurability of the percolation event · Wired probability that the origin connects to the outside of a box · Wired crossing probabilities converge to the percolation probability · Crossing events intersect to the percolation event · Box-boundary connection probability tends to percolation probability · Crossing probabilities converge to the percolation probability · Boundary connection inside \(\Lambda_n\) reaches outside \(\Lambda_{n-1}\) · Leaving \(\Lambda_n\) implies connecting to \(\partial\Lambda_n\) · Wired infinite-volume boundary connection tends to \(\theta^1(p, q)\)

DefinitionOne-arm probability#✓fully proved

The one-arm probability ℙ_p(0 ↔ ℤ^d \ Λ_{n-1}).

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

Uses 4 · Used by 9

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · One-arm event from the origin · Bernoulli product measure on configuration space

Used byMean-field lower bound · Exponential decay below p̃_c · Exponential decay from a one-step recursion · Mean-field lower bound for \(\theta(p)\) from a differential inequality · One-arm probability as a function of a real density · 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

TheoremExponential decay from a one-step recursion#✓fully proved

If φ_p(S) < 1 and crossProb((k + 1)L) ≤ φ_p(S) · crossProb(kL) for all k, then crossProb d p n ≤ C e^{-cn} for some c, C > 0.

theorem subcritical_decay (p : ℝ≥0) (hp : p ≤ 1) (S : Finset (Site d))
    (_hS0 : origin d ∈ S) (hphi : phi d p hp S < 1)
    (L : ℕ) (hL : 1 ≤ L)
    (hstep : ∀ k, crossProb d p hp ((k + 1) * L) ≤ phi d p hp S * crossProb d p hp (k * L)) :
    ∃ c > 0, ∃ C > 0, ∀ n, crossProb d p hp n ≤ C * Real.exp (-c * n)

Uses 10

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

Proof usesConfiguration space of a statistical-mechanics model · Connection by an open path · Box \((-n, n)^d\) in the hypercubic lattice · One-arm event from the origin · Bernoulli distribution on the Booleans · Bernoulli product measure on configuration space

TheoremTranslation invariance of the Bernoulli product measure#✓fully proved

The Bernoulli product measure on {0, 1}^E is invariant under the shift action of G.

theorem bernoulli_translationInvariant (p : ℝ≥0) (hp : p ≤ 1) [Countable E] :
    IsTranslationInvariant (G := G) (bernoulliProductMeasure (E := E) p hp)

Uses 5 · Used by 3

Statement usesTranslation-invariant measure on configuration space · Bernoulli product measure on configuration space

Proof usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Bernoulli distribution on the Booleans

Used byExponential decay below p̃_c · Bernoulli zero-one law for infinite groups acting finite-to-one · Ergodicity of Bernoulli measures under free infinite-group actions

DefinitionOne-arm event from a shifted origin#✓fully proved

The event that y is joined by an open path to a site outside Λ_{n-1}.

def crossingEventFrom (d : ℕ) (y : Site d) (n : ℕ) : Set (ConfigSpace (Sym2 (Site d))) :=
  {ω | ∃ v, Connected d ω y v ∧ v ∉ box d (n - 1)}

Uses 4 · Used by 1

Statement 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

Used byExponential decay below p̃_c

TheoremExponential decay below p̃_c#✓fully proved

Exponential decay below p̃_c (Duminil-Copin–Tassion 2016): if φ_p(S) < 1 for some finite S ∋ 0, then ℙ_p(0 ↔ ℤ^d \ Λ_{n-1}) ≤ C e^{-cn} for some c, C > 0.

theorem crossProb_exp_decay_of_phi_lt_one (p : ℝ≥0) (hp : p ≤ 1) (S : Finset (Site d))
    (hoS : origin d ∈ (S : Set (Site d))) (hphi : phi d p hp S < 1)
    (L : ℕ) (hL : 1 ≤ L) (hSbox : (S : Set (Site d)) ⊆ box d (L - 1)) :
    ∃ c > 0, ∃ C > 0, ∀ n, crossProb d p hp n ≤ C * Real.exp (-c * n)

Uses 43 · Used by 1

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · One-arm probability · Origin of the hypercubic lattice · Duminil-Copin–Tassion quantity

Proof usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Connection by an open path · Connection by an open path within a set · Open lattice edge of a bond configuration · Hypercubic lattice \(\mathbb{Z}^d\) · Open subgraph of a bond configuration · Open subgraph induced on a set of sites · Product weight of an edge configuration · Translation invariance of the Bernoulli product measure · Oriented edge boundary of a finite lattice set · Open boundary edge of a cluster · Lattice box as a finite set · Box edges with no endpoint in a cluster · Event that the cluster of the origin inside a set equals a given set · Open cluster of a site inside a set · Probability of connection inside a set · Shift of a lattice site in one coordinate · One-arm event from the origin · One-arm event from a shifted origin · Pairs of sites of a finite set · Edges from a subset into a set · Edges joining a finite set to a region · Crossing inside the box that avoids a cluster · Sign of a unit lattice step · Translation of the open subgraph as a graph homomorphism · Inverse translation of the open subgraph · 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 · Events depending on finitely many coordinates are cylinders · Configuration patched from one configuration on a finite set and another off it · Bernoulli product measure of a cylinder event, real-valued form · Probability of a finitely dependent event as a polynomial in \(p\)

Used byExponential decay of the one-arm probability below the threshold

18 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.