Number of infinite clusters

TheoremShift-invariant countably valued functions are a.s. constant under ergodicity#✓fully proved

A measurable function with countable values that is invariant under all shifts is almost surely constant under an ergodic probability measure. See also Mathlib's ErgodicSMul and aeconst_of_forall_preimage_smul_ae_eq, which state ergodicity of a group action through a.e.-invariant sets.

theorem ergodic_ae_const_of_shiftInvariant [IsProbabilityMeasure μ]
    {β : Type*} [Countable β] [MeasurableSpace β] [MeasurableSingletonClass β]
    (herg : IsErgodic (G := G) μ)
    (f : ConfigSpace E → β) (hf : Measurable f)
    (hinv : ∀ (g : G) (ω : ConfigSpace E), f (shift g ω) = f ω) :
    ∃ k : β, μ {ω | f ω = k} = 1

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Ergodic measure on configuration space · Shift of a configuration by a group element

Proof usesTranslation-invariant measure on configuration space

Used byNumber of infinite clusters is almost surely constant

DefinitionTranslation of the open subgraph as a graph homomorphism#✓fully proved

Translation by g as a graph homomorphism between the open subgraphs of ω and of its shift.

def translateHom (g : Multiplicative (Site d)) (ω : ConfigSpace (Sym2 (Site d))) :
    openSubgraph d ω →g openSubgraph d (shift g ω) where
  toFun x := g • x
  map_rel' {x y} h := (openSubgraph_adj_shift g ω x y).mpr h

Uses 5 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Open subgraph of a bond configuration

Used byNumber of infinite clusters is almost surely constant · Exponential decay below p̃_c

DefinitionInverse translation of the open subgraph#✓fully proved

The inverse of translateHom.

def translateHomInv (g : Multiplicative (Site d)) (ω : ConfigSpace (Sym2 (Site d))) :
    openSubgraph d (shift g ω) →g openSubgraph d ω where
  toFun a := g⁻¹ • a
  map_rel' {a b} h := by
    have h' := (openSubgraph_adj_shift g ω (g⁻¹ • a) (g⁻¹ • b)).mp
    simp only [smul_inv_smul] at h'
    exact h' h

Uses 5 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Open subgraph of a bond configuration

Used byNumber of infinite clusters is almost surely constant · Exponential decay below p̃_c

DefinitionSet of infinite open clusters#✓fully proved

The set of infinite open clusters of ω.

def infiniteClusters (d : ℕ) (ω : ConfigSpace (Sym2 (Site d))) : Set (Set (Site d)) :=
  {C | C.Infinite ∧ ∃ x, C = cluster d ω x}

Uses 3 · Used by 3

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

Used byNumber of infinite open clusters · Number of infinite clusters is almost surely constant · Disconnected sites in infinite clusters give two infinite clusters

DefinitionNumber of infinite open clusters#✓fully proved

The number N(ω) ∈ ℕ∞ of infinite open clusters of ω.

noncomputable def numInfiniteClusters (d : ℕ) (ω : ConfigSpace (Sym2 (Site d))) : ℕ∞ :=
  (infiniteClusters d ω).encard

Uses 3 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Set of infinite open clusters

Used byEvent of at least two infinite open clusters · Configurations with \(k\) infinite clusters, two merged by opening \(F\) · Number of infinite clusters is almost surely constant · Zero or one infinite cluster, given ergodicity and \(\mu(N \ge 2) = 0\) · Burton–Keane theorem · Disconnected sites in infinite clusters give two infinite clusters

TheoremMeasurability of the one-arm event#✓fully proved

The one-arm event crossingEvent d n (the origin is connected to a site outside box d (n - 1)) is measurable.

theorem measurableSet_crossingEvent (n : ℕ) : MeasurableSet (crossingEvent d n)

Uses 8 · Used by 7

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · One-arm event from the origin

Proof usesConnection by an open path · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Open subgraph of a bond configuration · Origin of the hypercubic lattice

Used byMean-field lower bound · 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 crossing probabilities converge to the percolation probability · Crossing probabilities converge to the percolation probability

DefinitionRepresentative sites of the infinite clusters#✓fully proved

The set of sites x in an infinite cluster that are the Encodable-least site of their cluster (one representative per infinite cluster).

def repSet (d : ℕ) (ω : ConfigSpace (Sym2 (Site d))) : Set (Site d) :=
  {x | (cluster d ω x).Infinite ∧
        ∀ y, Connected d ω x y → Encodable.encode x ≤ Encodable.encode y}

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Connection by an open path · Site of the hypercubic lattice · Open cluster of a site

Used byNumber of infinite clusters is almost surely constant

TheoremNumber of infinite clusters is almost surely constant#✓fully proved

The number of infinite clusters is almost surely constant (Newman–Schulman 1981) for any translation-ergodic probability measure on bond configurations of ℤ^d.

theorem numInfiniteClusters_ae_const
    (μ : Measure (ConfigSpace (Sym2 (Site d)))) [IsProbabilityMeasure μ]
    (herg : IsErgodic (G := Multiplicative (Site d)) μ) :
    ∃ k : ℕ∞, μ {ω | numInfiniteClusters d ω = k} = 1

Uses 16 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Ergodic measure on configuration space · Site of the hypercubic lattice · Number of infinite open clusters

Proof usesShift-invariant countably valued functions are a.s. constant under ergodicity · Shift of a configuration by a group element · Connection by an open path · Box \((-n, n)^d\) in the hypercubic lattice · Open cluster of a site · Every finite set of sites lies in a box · Hypercubic lattice \(\mathbb{Z}^d\) · Open subgraph of a bond configuration · Set of infinite open clusters · Representative sites of the infinite clusters · Translation of the open subgraph as a graph homomorphism · Inverse translation of the open subgraph

Used byZero or one infinite cluster, given ergodicity and \(\mu(N \ge 2) = 0\)

DefinitionEvent of at least two infinite open clusters#✓fully proved

The event that there are at least two infinite open clusters.

def atLeastTwoInfinite (d : ℕ) : Set (ConfigSpace (Sym2 (Site d))) :=
  {ω | 2 ≤ numInfiniteClusters d ω}

Uses 3 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Number of infinite open clusters

Used byZero or one infinite cluster, given ergodicity and \(\mu(N \ge 2) = 0\) · Joint percolation at most connectivity given no two infinite clusters · Two-point lower bound from FKG, invariance, uniqueness and percolation · Disconnected sites in infinite clusters give two infinite clusters

DefinitionConfiguration with a finite edge set forced open#✓fully proved

The configuration obtained from ω by opening every edge of F.

noncomputable def forceOpenFinset (F : Finset (Sym2 (Site d)))
    (ω : ConfigSpace (Sym2 (Site d))) : ConfigSpace (Sym2 (Site d)) :=
  fun e => if e ∈ F then true else ω e

Uses 2 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice

Used byFinite energy for opening finite edge sets · Configurations with \(k\) infinite clusters, two merged by opening \(F\)

DefinitionEndpoints of a finite edge set#✓fully proved

The endpoints of the edges of F.

def anchorSites (F : Finset (Sym2 (Site d))) : Set (Site d) :=
  {a | ∃ e ∈ F, a ∈ e}

Uses 1

Statement usesSite of the hypercubic lattice

DefinitionConfigurations with \(k\) infinite clusters, two merged by opening \(F\)#✓fully proved

Configurations with exactly k infinite clusters in which opening F connects two distinct infinite clusters.

def MergeWitness (d : ℕ) (F : Finset (Sym2 (Site d))) (k : ℕ∞) :
    Set (ConfigSpace (Sym2 (Site d))) :=
  {ω | numInfiniteClusters d ω = k ∧
    ∃ x y : Site d, (cluster d ω x).Infinite ∧ (cluster d ω y).Infinite ∧
      cluster d ω x ≠ cluster d ω y ∧ Connected d (forceOpenFinset F ω) x y}

Uses 6

Statement usesConfiguration space of a statistical-mechanics model · Connection by an open path · Site of the hypercubic lattice · Open cluster of a site · Configuration with a finite edge set forced open · Number of infinite open clusters

DefinitionFinite energy for opening finite edge sets#✓fully proved

Finite energy for opening edges: for every finite edge set F, the law of forceOpenFinset F ω is absolutely continuous with respect to μ.

def HasFiniteEnergyMerge (μ : Measure (ConfigSpace (Sym2 (Site d)))) : Prop :=
  ∀ F : Finset (Sym2 (Site d)), (μ.map (fun ω => forceOpenFinset F ω)) ≪ μ

Uses 3

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Configuration with a finite edge set forced open

LemmaZero or one infinite cluster, given ergodicity and \(\mu(N \ge 2) = 0\)#✓fully proved

For an ergodic measure with μ(N ≥ 2) = 0, either a.s. N = 0 or a.s. N = 1.

lemma numInfiniteClusters_zero_or_one
    (μ : Measure (ConfigSpace (Sym2 (Site d)))) [IsProbabilityMeasure μ]
    (herg : IsErgodic (G := Multiplicative (Site d)) μ)
    (hmerge : μ (atLeastTwoInfinite d) = 0) :
    μ {ω | numInfiniteClusters d ω = 0} = 1 ∨ μ {ω | numInfiniteClusters d ω = 1} = 1

Uses 6

Statement usesConfiguration space of a statistical-mechanics model · Ergodic measure on configuration space · Site of the hypercubic lattice · Event of at least two infinite open clusters · Number of infinite open clusters

Proof usesNumber of infinite clusters is almost surely constant

14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.