Bounds on the critical probability

DefinitionVertices of a lattice path encoded by a step sequence#✓fully proved

The k-th vertex of the lattice path from the origin that takes step ±e_i given by g j at time j.

def vertOf (g : ℕ → Fin d × Bool) : ℕ → Site d
  | 0 => origin d
  | (k + 1) => coordShift (vertOf g k) (g k).1 (stepSign (g k).2)

Uses 4 · Used by 6

Statement usesSite of the hypercubic lattice · Shift of a lattice site in one coordinate · Origin of the hypercubic lattice · Sign of a unit lattice step

Used byEdges of a lattice path encoded by a step sequence · Self-avoiding initial segment of an encoded lattice path · Positivity of the critical probability (Hammersley's bound) · Sharpness of the phase transition · Open self-avoiding walk in a box gives \(m\) distinct open box edges · Percolation gives open self-avoiding walks of every length

DefinitionEdges of a lattice path encoded by a step sequence#✓fully proved

The k-th edge {vertOf g k, vertOf g (k + 1)} of the path encoded by g.

def edgeOf (g : ℕ → Fin d × Bool) (k : ℕ) : Sym2 (Site d) :=
  s(vertOf g k, vertOf g (k + 1))

Uses 2 · Used by 8

Statement usesSite of the hypercubic lattice · Vertices of a lattice path encoded by a step sequence

Used byPositivity of the critical probability (Hammersley's bound) · Event that an encoded lattice path is open · Sharpness of the phase transition · Open self-avoiding walk in a box gives \(m\) distinct open box edges · Event that a given walk is open is clopen · Event that a given walk is open is increasing · Bernoulli bound \(p^m\) for a fixed self-avoiding walk in the box · Percolation gives open self-avoiding walks of every length

DefinitionEvent that an encoded lattice path is open#✓fully proved

The event that the first n edges of the path encoded by g are open.

def wordEvent (g : ℕ → Fin d × Bool) (n : ℕ) : Set (ConfigSpace (Sym2 (Site d))) :=
  {ω | ∀ k ∈ Finset.range n, ω (edgeOf g k) = true}

Uses 3 · Used by 11

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Edges of a lattice path encoded by a step sequence

Used byPositivity of the critical probability (Hammersley's bound) · Sharpness of the phase transition · Open self-avoiding walk in a box gives \(m\) distinct open box edges · Event of an open self-avoiding walk of \(m\) steps · Event of some open self-avoiding walk is clopen · Event that a given walk is open is clopen · Event of some open self-avoiding walk is increasing · Event that a given walk is open is increasing · Bernoulli bound \(p^m\) for a fixed self-avoiding walk in the box · Percolation gives open self-avoiding walks of every length · Wired box bound \((2dp)^m\) on the open-walk event for \(q \ge 1\)

DefinitionSelf-avoiding initial segment of an encoded lattice path#✓fully proved

The first n + 1 vertices of the path encoded by g are distinct.

def goodWord (g : ℕ → Fin d × Bool) (n : ℕ) : Prop :=
  Set.InjOn (vertOf g) (Finset.range (n + 1))

Uses 2 · Used by 8

Statement usesSite of the hypercubic lattice · Vertices of a lattice path encoded by a step sequence

Used byPositivity of the critical probability (Hammersley's bound) · Open self-avoiding walk in a box gives \(m\) distinct open box edges · Event of an open self-avoiding walk of \(m\) steps · Event of some open self-avoiding walk is clopen · Event of some open self-avoiding walk is increasing · Bernoulli bound \(p^m\) for a fixed self-avoiding walk in the box · Percolation gives open self-avoiding walks of every length · Wired box bound \((2dp)^m\) on the open-walk event for \(q \ge 1\)

DefinitionStep directions of an open walk from the origin#✓fully proved

The direction (i, ±) of the k-th step of an open walk from the origin (arbitrary past its end).

noncomputable def dirOf (hd : 0 < d) {ω : ConfigSpace (Sym2 (Site d))} {v : Site d}
    (q : (openSubgraph d ω).Walk (origin d) v) (k : ℕ) : Fin d × Bool := by
  classical
  exact if hk : k < q.length then
      ((adj_exists_dir (openSubgraph_le ω (q.adj_getVert_succ hk))).choose,
       (adj_exists_dir (openSubgraph_le ω (q.adj_getVert_succ hk))).choose_spec.choose)
    else (⟨0, hd⟩, false)

Uses 7 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Open subgraph of a bond configuration · Shift of a lattice site in one coordinate · Origin of the hypercubic lattice · Sign of a unit lattice step

Used byPositivity of the critical probability (Hammersley's bound) · Percolation gives open self-avoiding walks of every length

TheoremPositivity of the critical probability (Hammersley's bound)#✓fully proved

p_c(d) > 0 for bond percolation on ℤ^d, d ≥ 1 (Hammersley 1957, by counting paths: p_c(d) ≥ 1/(2d)).

theorem pc_pos (hd : 0 < d) : 0 < pc d

Uses 21 · Used by 2

Statement usesCritical probability of bond percolation on the hypercubic lattice

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 · Hypercubic lattice \(\mathbb{Z}^d\) · Open subgraph of a bond configuration · Shift of a lattice site in one coordinate · Step directions of an open walk from the origin · Edges of a lattice path encoded by a step sequence · Self-avoiding initial segment of an encoded lattice path · Origin of the hypercubic lattice · Percolation event for the origin · Sign of a unit lattice step · Set of densities with no percolation · Percolation probability of bond percolation · 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

Used byNon-triviality of the percolation critical probability · Nontrivial Bernoulli critical probability on \(\mathbb{Z}^2\)

DefinitionPeierls series bounding closed dual circuits#✓fully proved

The Peierls series ∑_ℓ ℓ 4^ℓ (1 - p)^ℓ bounding the probability of a closed dual circuit around the origin.

noncomputable def pcUpperBound (p : ℝ) : ℝ :=
  ∑' ℓ : ℕ, (ℓ : ℝ) * (4 : ℝ) ^ ℓ * (1 - p) ^ ℓ

Used by 4

Used byPeierls contour bound on the percolation probability · \(p_c(2) < 1\) from the Peierls contour bound · \(p_c(2) < 1\) from anchored dual-circuit enclosure · Peierls series for \(d = 2\) equals the Bernoulli Peierls series

DefinitionGeometric ratio of the Peierls series#✓fully proved

The ratio 4(1 - p) of the geometric part of pcUpperBound.

noncomputable def pcRatio (p : ℝ) : ℝ := 4 * (1 - p)

Used by 2

Used by\(p_c(2) < 1\) from the Peierls contour bound · \(p_c(2) < 1\) from anchored dual-circuit enclosure

DefinitionPeierls contour bound on the percolation probability#✓fully proved

The Peierls contour bound 1 - θ_2(p) ≤ pcUpperBound p at density p.

def PcContourBound (p : ℝ≥0) (hp : p ≤ 1) : Prop :=
  1 - theta 2 p hp ≤ pcUpperBound (p : ℝ)

Uses 2 · Used by 1

Statement usesPeierls series bounding closed dual circuits · Percolation probability of bond percolation

Used by\(p_c(2) < 1\) from the Peierls contour bound

Theorem\(p_c(2) < 1\) from the Peierls contour bound#✓fully proved

p_c(2) < 1, assuming the Peierls contour bound PcContourBound for all p above some p₀ < 1.

theorem pc_lt_one
    (hGeom : ∃ p₀ : ℝ, p₀ < 1 ∧
      ∀ (p : ℝ≥0) (hp : p ≤ 1), (p₀ : ℝ) < (p : ℝ) → PcContourBound p hp) :
    pc 2 < 1

Uses 6

Statement usesPeierls contour bound on the percolation probability · Critical probability of bond percolation on the hypercubic lattice

Proof usesGeometric ratio of the Peierls series · Peierls series bounding closed dual circuits · Set of densities with no percolation · Percolation probability of bond percolation

DefinitionPrimal edges crossed by a dual walk#✓fully proved

The set of primal edges crossed by the darts of a walk c in the dual (face) lattice.

noncomputable def primalEdgeFinset {u v : Site 2} (c : (hypercubicLattice 2).Walk u v) :
    Finset (Sym2 (Site 2)) :=
  (c.darts.map (fun D => sharedPrimalEdge D.fst D.snd)).toFinset

Uses 3 · Used by 1

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Primal edge shared by adjacent faces

Used by\(p_c(2) < 1\) from anchored dual-circuit enclosure

DefinitionEvent that a dual circuit is closed#✓fully proved

The event that every primal edge crossed by the dual walk c is closed.

def closedCircuitEvent {u v : Site 2} (c : (hypercubicLattice 2).Walk u v) :
    Set (ConfigSpace (Sym2 (Site 2))) :=
  {ω | ∀ D ∈ c.darts, ω (sharedPrimalEdge D.fst D.snd) = false}

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Primal edge shared by adjacent faces

Used by\(p_c(2) < 1\) from anchored dual-circuit enclosure

DefinitionAnchor sites for dual circuits#✓fully proved

The 2ℓ anchor sites (j, 0) and (j, -1), 0 ≤ j < ℓ.

noncomputable def anchorFinset (ℓ : ℕ) : Finset (Site 2) :=
  ((Finset.range ℓ).image (fun j : ℕ => (![ (j : ℤ), 0] : Site 2))) ∪
  ((Finset.range ℓ).image (fun j : ℕ => (![ (j : ℤ), -1] : Site 2)))

Uses 1 · Used by 11

Statement usesSite of the hypercubic lattice

Used byAnchored dual cycles of a given length · Anchored dual-circuit enclosure property · \(p_c(2) < 1\) from anchored dual-circuit enclosure · Anchored dual cycles give the anchored enclosure property · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle · \(p_c(\mathbb{Z}^2) < 1\) via boundary connectivity, assuming linked exits · Outer contour map: clusters as interiors of boundary circuits · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionAnchored dual cycles of a given length#✓fully proved

The finite set of dual cycles of length ℓ based at an anchor site of anchorFinset ℓ.

noncomputable def cyclesAtLen (ℓ : ℕ) :
    Finset (Σ u : Site 2, (hypercubicLattice 2).Walk u u) :=
  (anchorFinset ℓ).sigma
    (fun u => ((hypercubicLattice 2).finsetWalkLength ℓ u u).filter (·.IsCycle))

Uses 7 · Used by 2

Statement usesNearest neighbours in \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Nearest neighbours of a lattice site · Neighbour of a site in a coordinate direction · Hypercubic lattice \(\mathbb{Z}^d\) · Shift of a site along a coordinate · Anchor sites for dual circuits

Used by\(p_c(2) < 1\) from anchored dual-circuit enclosure · Cycles of length less than \(M\) based near the origin

DefinitionSummand of the anchored Peierls series#✓fully proved

The summand 2ℓ · 4^ℓ · (1 - p)^ℓ.

noncomputable def pcSummandTwo (p : ℝ) (ℓ : ℕ) : ℝ := (2 * ℓ * 4 ^ ℓ : ℕ) * ((1 - p) ^ ℓ)

Used by 1

Used by\(p_c(2) < 1\) from anchored dual-circuit enclosure

DefinitionAnchored dual-circuit enclosure property#✓fully proved

Every finite cluster of the origin is enclosed by a cycle of its face-boundary graph based at an anchor site of anchorFinset ℓ, where ℓ is the cycle length.

def PcAnchoredEnclosure : Prop :=
  ∀ ω : ConfigSpace (Sym2 (Site 2)), (cluster 2 ω (origin 2)).Finite →
    ∃ (u : Site 2) (c : (faceBoundaryGraph (cluster 2 ω (origin 2))).Walk u u),
      c.IsCycle ∧ u ∈ anchorFinset c.length

Uses 6 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Open cluster of a site · Face-boundary graph of a set · Anchor sites for dual circuits · Origin of the hypercubic lattice

Used by\(p_c(2) < 1\) from anchored dual-circuit enclosure · Anchored dual cycles give the anchored enclosure property · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle · \(p_c(\mathbb{Z}^2) < 1\) via boundary connectivity, assuming linked exits

Theorem\(p_c(2) < 1\) from anchored dual-circuit enclosure#✓fully proved

p_c(2) < 1, assuming the anchored enclosure property PcAnchoredEnclosure.

theorem pc_lt_one_of_enclosure (henc : PcAnchoredEnclosure) : pc 2 < 1

Uses 34 · Used by 4

Statement usesAnchored dual-circuit enclosure property · Critical probability of bond percolation on the hypercubic lattice

Proof usesConfiguration space of a statistical-mechanics model · Connection by an open path · Open lattice edge of a bond configuration · Nearest neighbours in \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Boundary edge of a set · Nearest neighbours of a lattice site · Neighbour of a site in a coordinate direction · Open cluster of a site · Edge boundary of a set of sites · Face-boundary graph of a set · Lower left corner of the unit face at \((a, b)\) · Upper left corner of the unit face at \((a, b)\) · Lower right corner of the unit face at \((a, b)\) · Upper right corner of the unit face at \((a, b)\) · Hypercubic lattice \(\mathbb{Z}^d\) · Open subgraph of a bond configuration · Primal edge shared by adjacent faces · Shift of a site along a coordinate · Anchor sites for dual circuits · Event that a dual circuit is closed · Anchored dual cycles of a given length · Origin of the hypercubic lattice · Geometric ratio of the Peierls series · Summand of the anchored Peierls series · Peierls series bounding closed dual circuits · Percolation event for the origin · Primal edges crossed by a dual walk · Set of densities with no percolation · Percolation probability of bond percolation · Bernoulli distribution on the Booleans · Bernoulli product measure on configuration space

Used by\(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle · \(p_c(\mathbb{Z}^2) < 1\) via boundary connectivity, assuming linked exits · \(p_c(\mathbb{Z}^2) < 1\) via the canonical contour, assuming anchored cycles

LemmaBernoulli product pulled back along an injection is Bernoulli#✓fully proved

Pulling a Bernoulli product configuration back along an injective map f : I → E gives the Bernoulli product measure on I. See also MeasureTheory.Measure.infinitePi_map_restrict' for the case of a subset.

lemma bernoulliProduct_map_injective_restrict
    {I E : Type*} [Countable I] [Countable E]
    (p : ℝ≥0) (hp : p ≤ 1) (f : I → E) (hf : Function.Injective f) :
    Measure.map (fun (omega : ConfigSpace E) (i : I) => omega (f i))
        (bernoulliProductMeasure (E := E) p hp) =
      bernoulliProductMeasure (E := I) p hp

Uses 4 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product measure on configuration space

Proof usesIndependence of coordinates under the Bernoulli product measure · Bernoulli distribution on the Booleans

Used byBernoulli percolation restricted to a box is Bernoulli on the box · Bernoulli percolation restricted to the plane is planar Bernoulli

Lemma\(q = 1\) probability of an edge pattern is its Bernoulli weight#✓fully proved

The q = 1 random-cluster probability of a given pattern on the graph edges is its Bernoulli weight.

lemma fkProbOne_pattern (p : ℝ) (eta : ConfigSpace ↥G.edgeFinset) :
    ∑ omega : ConfigSpace (Sym2 V),
        (if G.edgeFinset.restrict omega = eta then (1 : ℝ) else 0) *
          fkProb G p 1 omega = configWeight p eta

Uses 9 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Probability of an ambient FK configuration · Bernoulli product weight of a configuration

Proof usesBernoulli edge product · Unnormalized random-cluster weight · At \(q = 1\) the random-cluster weight is the Bernoulli product · Ambient FK normalizer · Boolean-configuration sum of a coordinatewise product factorizes · Bernoulli weight of a single coordinate

Used by\(q = 1\) measure equals Bernoulli percolation on graph-edge events

Lemma\(q = 1\) measure equals Bernoulli percolation on graph-edge events#✓fully proved

The q = 1 random-cluster measure on a finite graph agrees with Bernoulli percolation on events that depend only on the graph edges.

lemma fkProbOne_event_eq_bernoulli {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (A : Set (ConfigSpace (Sym2 V)))
    (hA : _root_.DependsOn (A.indicator (fun _ => (1 : ℝ)))
      (G.edgeFinset : Set (Sym2 V))) :
    ∑ omega : ConfigSpace (Sym2 V),
        A.indicator (fun _ => (1 : ℝ)) omega * fkProb G p 1 omega =
      (bernoulliProductMeasure (E := Sym2 V) ⟨p, hp.le⟩
        (by exact_mod_cast hp1.le)).real A

Uses 7 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Probability of an ambient FK configuration · Bernoulli product measure on configuration space

Proof uses\(q = 1\) probability of an edge pattern is its Bernoulli weight · Bernoulli product weight of a configuration · Events depending on finitely many coordinates are cylinders · Probability of a finitely dependent event as a polynomial in \(p\)

Used byWired \(q = 2\) origin-to-boundary probability at most Bernoulli · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition

LemmaConnection to the boundary depends only on graph edges#✓fully proved

The event that x is connected to the boundary depends only on the graph edges.

lemma connToBdryEvent_dependsOn (G : SimpleGraph V) [DecidableRel G.Adj]
    (bdry : V → Prop) (x : V) :
    _root_.DependsOn
      ({omega : ConfigSpace (Sym2 V) |
        IsingFK.ConnToBdry G bdry omega x}.indicator (fun _ => (1 : ℝ)))
      (G.edgeFinset : Set (Sym2 V))

Uses 4 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Open connection of a vertex to the boundary

Proof usesOpen connection between two vertices · Open subgraph of an edge configuration

Used byWired \(q = 2\) origin-to-boundary probability at most Bernoulli · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition

LemmaBernoulli percolation restricted to a box is Bernoulli on the box#✓fully proved

Restricting Bernoulli percolation on ℤ^d to the box gives Bernoulli percolation on the box.

lemma bernoulliProduct_map_boxRestrict (p : ℝ≥0) (hp : p ≤ 1) (n : ℕ) :
    Measure.map (boxRestrict d n)
        (bernoulliProductMeasure (E := Sym2 (Site d)) p hp) =
      bernoulliProductMeasure (E := Sym2 (boxVerts d n)) p hp

Uses 8 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Site of the hypercubic lattice · Bernoulli product measure on configuration space

Proof usesBernoulli product pulled back along an injection is Bernoulli · Inclusion of box edges into \(\mathbb{Z}^d\) · Box \((-n, n)^d\) in the hypercubic lattice

Used byBernoulli box cylinder probability equals its probability on the box

LemmaBernoulli box cylinder probability equals its probability on the box#✓fully proved

The Bernoulli probability of a box cylinder event equals its probability on the box.

lemma bernoulliProduct_boxRestrict_preimage (p : ℝ≥0) (hp : p ≤ 1)
    (n : ℕ) (A : Set (ConfigSpace (Sym2 (boxVerts d n)))) :
    (bernoulliProductMeasure (E := Sym2 (Site d)) p hp).real
        (boxRestrict d n ⁻¹' A) =
      (bernoulliProductMeasure (E := Sym2 (boxVerts d n)) p hp).real A

Uses 8 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Site of the hypercubic lattice · Bernoulli product measure on configuration space

Proof usesBernoulli percolation restricted to a box is Bernoulli on the box · Inclusion of box edges into \(\mathbb{Z}^d\) · Box \((-n, n)^d\) in the hypercubic lattice

Used byMonotonicity in \(p\) of the Bernoulli percolation probability · Wired \(q = 2\) origin-to-boundary probability at most Bernoulli · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition

LemmaWired \(q = 2\) origin-to-boundary probability at most Bernoulli#✓fully proved

The wired q = 2 box measure of "the origin is connected to the box boundary" is at most its Bernoulli probability.

lemma wiredFinite_boxBdryConnEvent_le_bernoulli
    (p : ℝ≥0) (hp0 : 0 < p) (hp1 : p < 1) (n : ℕ) :
    (wiredFiniteMeasure d n (p := (p : ℝ)) (by exact_mod_cast hp0) (by exact_mod_cast hp1)
        (by norm_num : (0 : ℝ) < 2) :
      Measure (ConfigSpace (Sym2 (Site d)))).real (boxBdryConnEvent d n) ≤
      (bernoulliProductMeasure (E := Sym2 (Site d)) p hp1.le).real
        (boxBdryConnEvent d n)

Uses 22 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Event that the box origin connects to the box boundary · Wired random-cluster measure on a box · Site of the hypercubic lattice · Bernoulli product measure on configuration space

Proof usesBernoulli box cylinder probability equals its probability on the box · Vertex boundary of a box · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Connection to the boundary depends only on graph edges · Inclusion of box edges into \(\mathbb{Z}^d\) · Probability of an ambient FK configuration · \(q = 1\) measure equals Bernoulli percolation on graph-edge events · Origin-to-boundary connection is an increasing event · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired random-cluster probability of a configuration · Wired law at most the \(q = 1\) law on increasing events, \(q \ge 1\) · Increasing event · Open connection of a vertex to the boundary · Origin as a vertex of the box graph · Box \((-n, n)^d\) in the hypercubic lattice

Used byWired \(q = 2\) percolation probability at most the Bernoulli one

LemmaWired \(q = 2\) percolation probability at most the Bernoulli one#✓fully proved

The wired q = 2 percolation probability is at most the Bernoulli one: θ¹(p, 2) ≤ θ(p).

lemma fkTheta_two_le_bernoulliTheta
    (p : ℝ≥0) (hp0 : 0 < p) (hp1 : p < 1) :
    fkTheta d (p := (p : ℝ)) (by exact_mod_cast hp0) (by exact_mod_cast hp1)
        (by norm_num : (0 : ℝ) < 2) (q := 2) ≤
      Percolation.theta d p hp1.le

Uses 12 · Used by 5

Statement usesWired random-cluster percolation probability \(\theta(p, q)\) · Percolation probability of bond percolation

Proof usesConfiguration space of a statistical-mechanics model · Event that the box origin connects to the box boundary · Wired \(q = 2\) percolation probability as the limit of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_n\) · Box-boundary connection probability tends to percolation probability · Wired random-cluster measure on a box · Wired \(q = 2\) origin-to-boundary probability at most Bernoulli · Site of the hypercubic lattice · Percolation event for the origin · Bernoulli distribution on the Booleans · Bernoulli product measure on configuration space

Used byPositive planar percolation at some \(p < 1\) via the Ising model · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition

DefinitionPlane embedding of \(\mathbb{Z}^2\) into \(\mathbb{Z}^{2+k}\)#✓fully proved

The embedding of ℤ² into ℤ^{2+k} as the plane of the first two coordinates.

def pcv_siteEmbed (k : ℕ) (x : Site 2) : Site (2 + k) :=
  Fin.addCases x (fun _ => 0)

Uses 1 · Used by 9

Statement usesSite of the hypercubic lattice

Used byPlane open connections are open connections in \(\mathbb{Z}^{2+k}\) · Plane embedding on edges · Injectivity of the plane embedding on edges · Percolation in the plane implies percolation in \(\mathbb{Z}^{2+k}\) · Plane embedding preserves and reflects adjacency · First two coordinates of an embedded site are the original ones · Injectivity of the plane embedding · Last \(k\) coordinates of an embedded site vanish · Plane embedding fixes the origin

LemmaFirst two coordinates of an embedded site are the original ones#✓fully proved

The first two coordinates of an embedded site.

@[simp] lemma pcv_siteEmbed_castAdd (k : ℕ) (x : Site 2) (i : Fin 2) :
    pcv_siteEmbed k x (Fin.castAdd k i) = x i

Uses 2 · Used by 3

Statement usesSite of the hypercubic lattice · Plane embedding of \(\mathbb{Z}^2\) into \(\mathbb{Z}^{2+k}\)

Used byPlane embedding preserves and reflects adjacency · Injectivity of the plane embedding · Plane embedding fixes the origin

LemmaLast \(k\) coordinates of an embedded site vanish#✓fully proved

The last k coordinates of an embedded site vanish.

@[simp] lemma pcv_siteEmbed_natAdd (k : ℕ) (x : Site 2) (i : Fin k) :
    pcv_siteEmbed k x (Fin.natAdd 2 i) = 0

Uses 2 · Used by 2

Statement usesSite of the hypercubic lattice · Plane embedding of \(\mathbb{Z}^2\) into \(\mathbb{Z}^{2+k}\)

Used byPlane embedding preserves and reflects adjacency · Plane embedding fixes the origin

LemmaInjectivity of the plane embedding#✓fully proved

The plane embedding is injective.

lemma pcv_siteEmbed_injective (k : ℕ) : Function.Injective (pcv_siteEmbed k)

Uses 3 · Used by 2

Statement usesSite of the hypercubic lattice · Plane embedding of \(\mathbb{Z}^2\) into \(\mathbb{Z}^{2+k}\)

Proof usesFirst two coordinates of an embedded site are the original ones

Used byInjectivity of the plane embedding on edges · Percolation in the plane implies percolation in \(\mathbb{Z}^{2+k}\)

LemmaPlane embedding preserves and reflects adjacency#✓fully proved

The plane embedding preserves and reflects lattice adjacency.

lemma pcv_siteEmbed_adj_iff (k : ℕ) (x y : Site 2) :
    (hypercubicLattice (2 + k)).Adj (pcv_siteEmbed k x) (pcv_siteEmbed k y) ↔
      (hypercubicLattice 2).Adj x y

Uses 5 · Used by 1

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Plane embedding of \(\mathbb{Z}^2\) into \(\mathbb{Z}^{2+k}\)

Proof usesFirst two coordinates of an embedded site are the original ones · Last \(k\) coordinates of an embedded site vanish

Used byPlane open connections are open connections in \(\mathbb{Z}^{2+k}\)

DefinitionPlane embedding on edges#✓fully proved

The plane embedding on edges.

def pcv_edgeEmbed (k : ℕ) : Sym2 (Site 2) → Sym2 (Site (2 + k)) :=
  Sym2.map (pcv_siteEmbed k)

Uses 2 · Used by 4

Statement usesSite of the hypercubic lattice · Plane embedding of \(\mathbb{Z}^2\) into \(\mathbb{Z}^{2+k}\)

Used byBernoulli percolation restricted to the plane is planar Bernoulli · Injectivity of the plane embedding on edges · Restriction of a configuration to the embedded plane · \(\theta_2(p) \le \theta_{2+k}(p)\) for Bernoulli percolation

LemmaInjectivity of the plane embedding on edges#✓fully proved

The plane embedding on edges is injective.

lemma pcv_edgeEmbed_injective (k : ℕ) : Function.Injective (pcv_edgeEmbed k)

Uses 4 · Used by 1

Statement usesSite of the hypercubic lattice · Plane embedding on edges

Proof usesPlane embedding of \(\mathbb{Z}^2\) into \(\mathbb{Z}^{2+k}\) · Injectivity of the plane embedding

Used byBernoulli percolation restricted to the plane is planar Bernoulli

DefinitionRestriction of a configuration to the embedded plane#✓fully proved

Restrict a configuration on ℤ^{2+k} to the embedded plane.

def pcv_planeRestrict (k : ℕ)
    (omega : ConfigSpace (Sym2 (Site (2 + k)))) : ConfigSpace (Sym2 (Site 2)) :=
  fun e => omega (pcv_edgeEmbed k e)

Uses 3 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Plane embedding on edges

Used byBernoulli percolation restricted to the plane is planar Bernoulli · Plane open connections are open connections in \(\mathbb{Z}^{2+k}\) · Percolation in the plane implies percolation in \(\mathbb{Z}^{2+k}\) · \(\theta_2(p) \le \theta_{2+k}(p)\) for Bernoulli percolation

LemmaBernoulli percolation restricted to the plane is planar Bernoulli#✓fully proved

Restricting Bernoulli percolation on ℤ^{2+k} to the plane gives Bernoulli percolation on ℤ².

lemma bernoulliProduct_map_planeRestrict (k : ℕ) (p : ℝ≥0) (hp : p ≤ 1) :
    Measure.map (pcv_planeRestrict k)
        (bernoulliProductMeasure (E := Sym2 (Site (2 + k))) p hp) =
      bernoulliProductMeasure (E := Sym2 (Site 2)) p hp

Uses 7 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Restriction of a configuration to the embedded plane · Bernoulli product measure on configuration space

Proof usesBernoulli product pulled back along an injection is Bernoulli · Plane embedding on edges · Injectivity of the plane embedding on edges

Used by\(\theta_2(p) \le \theta_{2+k}(p)\) for Bernoulli percolation

LemmaPlane embedding fixes the origin#✓fully proved

The plane embedding sends the origin to the origin.

@[simp] lemma pcv_siteEmbed_origin (k : ℕ) :
    pcv_siteEmbed k (origin 2) = origin (2 + k)

Uses 5 · Used by 1

Statement usesSite of the hypercubic lattice · Origin of the hypercubic lattice · Plane embedding of \(\mathbb{Z}^2\) into \(\mathbb{Z}^{2+k}\)

Proof usesFirst two coordinates of an embedded site are the original ones · Last \(k\) coordinates of an embedded site vanish

Used byPercolation in the plane implies percolation in \(\mathbb{Z}^{2+k}\)

LemmaPlane open connections are open connections in \(\mathbb{Z}^{2+k}\)#✓fully proved

Open connections in the restricted plane configuration are open connections in ℤ^{2+k}.

lemma pcv_connected_of_planeRestrict (k : ℕ)
    (omega : ConfigSpace (Sym2 (Site (2 + k)))) {x y : Site 2}
    (h : Lattice.Connected 2 (pcv_planeRestrict k omega) x y) :
    Lattice.Connected (2 + k) omega (pcv_siteEmbed k x) (pcv_siteEmbed k y)

Uses 8 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Connection by an open path · Site of the hypercubic lattice · Restriction of a configuration to the embedded plane · Plane embedding of \(\mathbb{Z}^2\) into \(\mathbb{Z}^{2+k}\)

Proof usesHypercubic lattice \(\mathbb{Z}^d\) · Open subgraph of a bond configuration · Plane embedding preserves and reflects adjacency

Used byPercolation in the plane implies percolation in \(\mathbb{Z}^{2+k}\)

LemmaPercolation in the plane implies percolation in \(\mathbb{Z}^{2+k}\)#✓fully proved

Percolation in the plane implies percolation in ℤ^{2+k}.

lemma pcv_plane_percolation_subset (k : ℕ) :
    pcv_planeRestrict k ⁻¹' percolationEvent 2 ⊆ percolationEvent (2 + k)

Uses 11 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Restriction of a configuration to the embedded plane · Percolation event for the origin

Proof usesConnection by an open path · Open cluster of a site · Origin of the hypercubic lattice · Plane open connections are open connections in \(\mathbb{Z}^{2+k}\) · Plane embedding of \(\mathbb{Z}^2\) into \(\mathbb{Z}^{2+k}\) · Injectivity of the plane embedding · Plane embedding fixes the origin

Used by\(\theta_2(p) \le \theta_{2+k}(p)\) for Bernoulli percolation

Lemma\(\theta_2(p) \le \theta_{2+k}(p)\) for Bernoulli percolation#✓fully proved

The Bernoulli percolation probability does not decrease with the dimension: θ_2(p) ≤ θ_{2+k}(p).

lemma theta_two_le_theta_add (k : ℕ) (p : ℝ≥0) (hp : p ≤ 1) :
    theta 2 p hp ≤ theta (2 + k) p hp

Uses 11 · Used by 5

Statement usesPercolation probability of bond percolation

Proof usesConfiguration space of a statistical-mechanics model · Measurability of the percolation event · Site of the hypercubic lattice · Bernoulli percolation restricted to the plane is planar Bernoulli · Plane embedding on edges · Restriction of a configuration to the embedded plane · Percolation in the plane implies percolation in \(\mathbb{Z}^{2+k}\) · Percolation event for the origin · Bernoulli distribution on the Booleans · Bernoulli product measure on configuration space

Used byBernoulli critical probability below one for \(d \ge 2\) · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition

LemmaMonotonicity in \(p\) of the Bernoulli percolation probability#✓fully proved

The Bernoulli percolation probability θ_d(p) is monotone in p.

lemma theta_mono_parameter {p q : ℝ≥0} (hp : p ≤ 1) (hq : q ≤ 1)
    (hpq : p ≤ q) : theta d p hp ≤ theta d q hq

Uses 20 · Used by 1

Statement usesPercolation probability of bond percolation

Proof usesConfiguration space of a statistical-mechanics model · Event depending only on a set of coordinates · Bernoulli box cylinder probability equals its probability on the box · Event that the box origin connects to the box boundary · Box-boundary connection probability tends to percolation probability · Vertex boundary of a box · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Origin-to-boundary connection is an increasing event · Open connection of a vertex to the boundary · Origin as a vertex of the box graph · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Percolation event for the origin · Agreement of configurations on a set · Bernoulli distribution on the Booleans · Bernoulli product measure on configuration space · Increasing-event probabilities are monotone in the parameter

Used byPositive percolation at \(p\) gives \(p_c(d) \le p\)

LemmaPositive percolation at \(p\) gives \(p_c(d) \le p\)#✓fully proved

Positive percolation probability at p gives p_c(d) ≤ p.

lemma pc_le_of_theta_pos (p : ℝ≥0) (hp : p ≤ 1)
    (hpos : 0 < theta d p hp) : pc d ≤ p

Uses 4 · Used by 2

Statement usesCritical probability of bond percolation on the hypercubic lattice · Percolation probability of bond percolation

Proof usesSet of densities with no percolation · Monotonicity in \(p\) of the Bernoulli percolation probability

Used byBernoulli critical probability below one for \(d \ge 2\) · Bernoulli critical probability on \(\mathbb{Z}^2\) is below one

LemmaPositive planar percolation at some \(p < 1\) via the Ising model#✓fully proved

There is p < 1 with θ_2(p) > 0, from spontaneous magnetization of the two-dimensional Ising model.

lemma exists_theta_two_pos_below_one :
    ∃ (p : ℝ≥0) (hp1 : p < 1), 0 < theta 2 p hp1.le

Uses 65 · Used by 2

Statement usesPercolation probability of bond percolation

Proof usesConfiguration space of a statistical-mechanics model · Vertex boundary of a box · Ising FK box-boundary connection profile tends to \(\theta^1(p, 2)\) · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Normalizing constant relating the bond sum to the Potts weight · Edwards–Sokal joint weight · Edwards–Sokal bond sum is a multiple of the Potts weight · Wired random-cluster percolation probability \(\theta(p, q)\) · Wired \(q = 2\) percolation probability at most the Bernoulli one · Ising spin value of a two-state color · Infinite-volume state of a sequence of measures · Bond variable of an unordered pair · Bonds touching the box · Ordered nearest-neighbour pairs touching the box · Box \((-n, n)^d\) as a finite set of sites · Existence of infinite-volume states · Box energy with a boundary condition · Finite-volume Gibbs measure on configurations of \(\mathbb{Z}^d\) · Finite-volume Gibbs probability with a boundary condition · Finite-volume Gibbs measure as a probability measure · Finite-volume Boltzmann weight with a boundary condition · Finite-volume partition function with a boundary condition · Configuration glued from inside spins and a boundary condition · Integrability of the spin at a site under finite measures · Chosen subsequential weak limit of a sequence of measures · Spontaneous magnetization of the Ising model · Origin of \(\mathbb{Z}^d\) · All-plus configuration · Plus-boundary Ising measure in a box · Infinite-volume plus state as a subsequential weak limit · Spin of a configuration at a site · Spin at a site as a bounded continuous function · Coloring fixed to a color on the boundary · Two-state color of a Boolean spin · Wired probability that the origin reaches the box boundary · Origin as a vertex of the box graph · Edwards–Sokal weight with fixed boundary color · Wired Edwards–Sokal one-point function · Edwards–Sokal one-point identity · Total wired Edwards–Sokal weight · Finite-volume plus-boundary magnetization at the origin · Box configurations as box-graph colorings with boundary color \(0\) · Ising bond variable of a two-state coloring · Plus-boundary Ising one-point function on a graph · Ising weight of a coloring with plus boundary · Plus-boundary Ising partition function on a graph · Box configuration as a coloring of the next larger box · FK edge parameter of an Ising inverse temperature · Potts weight with fixed boundary color · Potts partition function with fixed boundary color · Peierls' theorem · Wired random-cluster probability of connecting to the boundary · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Inner vertex boundary of a box · Origin of the hypercubic lattice · Agreement count of a spin configuration · Monochromatic-edge indicator · Potts Boltzmann weight · Weak convergence of probability measures on configuration space · Weak convergence implies convergence of integrals

Used byBernoulli critical probability below one for \(d \ge 2\) · Bernoulli critical probability on \(\mathbb{Z}^2\) is below one

LemmaBernoulli critical probability on \(\mathbb{Z}^2\) is below one#✓fully proved

The Bernoulli critical probability on ℤ² is below 1.

lemma pc_two_lt_one_via_fk : pc 2 < 1

Uses 4 · Used by 1

Statement usesCritical probability of bond percolation on the hypercubic lattice

Proof usesPositive planar percolation at some \(p < 1\) via the Ising model · Positive percolation at \(p\) gives \(p_c(d) \le p\) · Percolation probability of bond percolation

Used byNontrivial Bernoulli critical probability on \(\mathbb{Z}^2\)

LemmaNontrivial Bernoulli critical probability on \(\mathbb{Z}^2\)#✓fully proved

0 < p_c(2) < 1.

lemma pc_two_nontrivial : 0 < pc 2 ∧ pc 2 < 1

Uses 3

Statement usesCritical probability of bond percolation on the hypercubic lattice

Proof usesPositivity of the critical probability (Hammersley's bound) · Bernoulli critical probability on \(\mathbb{Z}^2\) is below one

LemmaBernoulli critical probability below one for \(d \ge 2\)#✓fully proved

The Bernoulli critical probability on ℤ^d is below 1 for d ≥ 2.

lemma pc_lt_one_of_two_le_via_fk {d : ℕ} (hd : 2 ≤ d) : pc d < 1

Uses 5 · Used by 1

Statement usesCritical probability of bond percolation on the hypercubic lattice

Proof usesPositive planar percolation at some \(p < 1\) via the Ising model · Positive percolation at \(p\) gives \(p_c(d) \le p\) · Percolation probability of bond percolation · \(\theta_2(p) \le \theta_{2+k}(p)\) for Bernoulli percolation

Used byNon-triviality of the percolation critical probability

TheoremNon-triviality of the percolation critical probability#✓fully proved

For Bernoulli bond percolation on ℤ^d with d ≥ 2, 0 < p_c(d) < 1.

Reference: S. R. Broadbent and J. M. Hammersley, Percolation processes I, Proc. Cambridge Philos. Soc. 53 (1957); G. Grimmett, Percolation, 2nd ed. (1999), Theorem 1.10.

theorem pc_nontrivial_of_two_le {d : ℕ} (hd : 2 ≤ d) :
    0 < pc d ∧ pc d < 1

Uses 3

Statement usesCritical probability of bond percolation on the hypercubic lattice

Proof usesBernoulli critical probability below one for \(d \ge 2\) · Positivity of the critical probability (Hammersley's bound)

45 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.