Positive association, translates of crossing events, and the box-crossing property

DefinitionOpen cluster of the origin#✓fully proved

The open cluster of the origin of ℤ^d.

def originCluster (d : ℕ) (ω : ConfigSpace (Sym2 (Site d))) : Set (Site d) :=
  cluster d ω (0 : Site d)

Uses 3 · Used by 1

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

Used byEvent that the origin's cluster is infinite

DefinitionEvent that the origin's cluster is infinite#✓fully proved

The event {0 ↔ ∞} that the open cluster of the origin is infinite.

def percolationEvent (d : ℕ) : Set (ConfigSpace (Sym2 (Site d))) :=
  {ω | (originCluster d ω).Infinite}

Uses 3 · Used by 2

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

Used byAgreement of the two percolation events · Percolation probability as an extended real

DefinitionPercolation probability as an extended real#✓fully proved

The percolation probability θ_d(p) = ℙ_p(0 ↔ ∞), as an extended nonnegative real.

noncomputable def percolationProbability (d : ℕ) (p : ℝ≥0) (hp : p ≤ 1) : ℝ≥0∞ :=
  bernoulliProductMeasure (E := Sym2 (Site d)) p hp (percolationEvent d)

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Event that the origin's cluster is infinite · Bernoulli product measure on configuration space

Used byReal densities with no percolation

DefinitionReal densities with no percolation#✓fully proved

The set of real densities p ∈ [0, 1] with θ_d(p) = 0.

def subcriticalDensities (d : ℕ) : Set ℝ :=
  {p : ℝ | ∃ (hp0 : 0 ≤ p) (hp1 : p ≤ 1),
      percolationProbability d ⟨p, hp0⟩ (by exact_mod_cast hp1) = 0}

Uses 1 · Used by 2

Statement usesPercolation probability as an extended real

Used byCritical probability as a real number · Agreement of the two critical probabilities

DefinitionCritical probability as a real number#✓fully proved

The critical probability p_c(d) = sup {p ∈ [0, 1] : θ_d(p) = 0} as a real number (see criticalProbability_eq_pc).

noncomputable def criticalProbability (d : ℕ) : ℝ :=
  sSup (subcriticalDensities d)

Uses 1 · Used by 1

Statement usesReal densities with no percolation

Used byAgreement of the two critical probabilities

TheoremAgreement of the two percolation events#✓fully proved

percolationEvent is StatMech.Percolation.percolationEvent.

theorem percolationEvent_eq : percolationEvent d = Percolation.percolationEvent d

Uses 4

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Percolation event for the origin · Event that the origin's cluster is infinite

TheoremAgreement of the two critical probabilities#✓fully proved

criticalProbability is the real-valued form of StatMech.Percolation.pc.

theorem criticalProbability_eq_pc : criticalProbability d = (Percolation.pc d : ℝ)

Uses 10

Statement usesCritical probability of bond percolation on the hypercubic lattice · Critical probability as a real number

Proof usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Percolation event for the origin · Set of densities with no percolation · Percolation probability of bond percolation · Real densities with no percolation · Bernoulli distribution on the Booleans · Bernoulli product measure on configuration space

DefinitionPositively associated measure#✓fully proved

A finite measure on configurations is positively associated if μ(A) μ(B) ≤ μ(A ∩ B) μ(univ) for all measurable increasing events A, B. The total-mass factor makes the Harris--FKG inequality invariant under finite scaling.

def PositivelyAssociated {E : Type*} (μ : Measure (ConfigSpace E))
    [IsFiniteMeasure μ] : Prop :=
  ∀ A B : Set (ConfigSpace E), MeasurableSet A → MeasurableSet B →
    IsIncreasing A → IsIncreasing B →
    μ.real A * μ.real B ≤ μ.real (A ∩ B) * μ.real Set.univ

Uses 2 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Increasing event

Used byPositive association for probability measures is the Harris–FKG inequality · Harris–FKG inequality for a positively associated probability measure · Square-root trick · RSW gluing from side separation

TheoremPositive association for probability measures is the Harris–FKG inequality#✓fully proved

For a probability measure, normalized positive association is the usual Harris--FKG inequality.

theorem positivelyAssociated_iff_of_isProbabilityMeasure {E : Type*}
    (μ : Measure (ConfigSpace E)) [IsProbabilityMeasure μ] :
    PositivelyAssociated μ ↔
      ∀ A B : Set (ConfigSpace E), MeasurableSet A → MeasurableSet B →
        IsIncreasing A → IsIncreasing B → μ.real A * μ.real B ≤ μ.real (A ∩ B)

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Positively associated measure

Used byHarris–FKG inequality for a positively associated probability measure

TheoremHarris–FKG inequality for a positively associated probability measure#✓fully proved

The usual unnormalized Harris--FKG inequality for a positively associated probability measure.

theorem PositivelyAssociated.probability {E : Type*} {μ : Measure (ConfigSpace E)}
    [IsProbabilityMeasure μ] (h : PositivelyAssociated μ)
    (A B : Set (ConfigSpace E)) (hAm : MeasurableSet A) (hBm : MeasurableSet B)
    (hA : IsIncreasing A) (hB : IsIncreasing B) :
    μ.real A * μ.real B ≤ μ.real (A ∩ B)

Uses 4 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Positively associated measure

Proof usesPositive association for probability measures is the Harris–FKG inequality

Used bySquare-root trick · RSW gluing from side separation

DefinitionTranslate of a bond configuration#✓fully proved

The configuration ω translated by -v: the state of e is the state of e + v in ω.

def translateConfig (v : Site 2) (ω : ConfigSpace (Sym2 (Site 2))) :
    ConfigSpace (Sym2 (Site 2)) :=
  fun e => ω (e.map (· + v))

Uses 2 · Used by 2

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

Used byLeft–right crossing event of a translated rectangle · Bottom–top crossing event of a translated rectangle

DefinitionLeft–right crossing event of a translated rectangle#✓fully proved

The event that the rectangle v + [0, a] × [0, b] has an open left–right crossing.

def translatedHorizontalCrossingEvent (v : Site 2) (a b : ℤ) :
    Set (ConfigSpace (Sym2 (Site 2))) :=
  (translateConfig v) ⁻¹' (horizontalCrossingEvent a b)

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Left–right crossing event of a rectangle at the origin · Translate of a bond configuration

Used bySet of long-direction box-crossing probabilities

DefinitionBottom–top crossing event of a translated rectangle#✓fully proved

The event that the rectangle v + [0, a] × [0, b] has an open bottom–top crossing.

def translatedVerticalCrossingEvent (v : Site 2) (a b : ℤ) :
    Set (ConfigSpace (Sym2 (Site 2))) :=
  (translateConfig v) ⁻¹' (verticalCrossingEvent a b)

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Bottom–top crossing event of a rectangle at the origin · Translate of a bond configuration

Used bySet of long-direction box-crossing probabilities

DefinitionSet of long-direction box-crossing probabilities#✓fully proved

The set of crossing probabilities, for n ≥ n₀ and all translates, of the long direction of ⌊ρn⌋ × n and n × ⌊ρn⌋ rectangles.

noncomputable def boxCrossingProbabilities (μ : Measure (ConfigSpace (Sym2 (Site 2))))
    (ρ : ℝ) (n0 : ℕ) : Set ℝ :=
  {x : ℝ | ∃ (n : ℕ) (τ : Site 2), n0 ≤ n ∧
      (x = μ.real (translatedHorizontalCrossingEvent τ ⌊ρ * (n : ℝ)⌋ (n : ℤ))
        ∨ x = μ.real (translatedVerticalCrossingEvent τ (n : ℤ) ⌊ρ * (n : ℝ)⌋))}

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Left–right crossing event of a translated rectangle · Bottom–top crossing event of a translated rectangle

Used byInfimum of the box-crossing probabilities

DefinitionInfimum of the box-crossing probabilities#✓fully proved

The infimum of boxCrossingProbabilities μ ρ n₀.

noncomputable def boxCrossingInf (μ : Measure (ConfigSpace (Sym2 (Site 2))))
    (ρ : ℝ) (n0 : ℕ) : ℝ :=
  sInf (boxCrossingProbabilities μ ρ n0)

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Set of long-direction box-crossing probabilities

Used byBox-crossing property with a given aspect ratio

DefinitionBox-crossing property with a given aspect ratio#✓fully proved

The box-crossing property with aspect ratio ρ > 1: for some n₀, the probabilities of crossing all translates of ⌊ρn⌋ × n rectangles in the long direction, n ≥ n₀, are bounded below by a positive constant.

def BoxCrossingProperty (μ : Measure (ConfigSpace (Sym2 (Site 2)))) (ρ : ℝ) : Prop :=
  1 < ρ ∧ ∃ n0 : ℕ, 0 < boxCrossingInf μ ρ n0

Uses 3

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Infimum of the box-crossing probabilities

16 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.