The square-root trick and gluing crossings through an overlap

TheoremSquare-root trick#✓fully proved

The square-root trick: for a positively associated probability measure and increasing measurable A, B, 1 - √(1 - μ(A ∪ B)) ≤ max(μ(A), μ(B)).

theorem rsw_sqrt_trick {E : Type*} (μ : Measure (ConfigSpace E))
    [IsProbabilityMeasure μ] (hpa : PositivelyAssociated μ)
    {A B : Set (ConfigSpace E)} (hA : IsIncreasing A) (hB : IsIncreasing B)
    (hAm : MeasurableSet A) (hBm : MeasurableSet B) :
    1 - Real.sqrt (1 - μ.real (A ∪ B)) ≤ max (μ.real A) (μ.real B)

Uses 7

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

Proof usesDecreasing event · Complement of a decreasing event is increasing · Complement of an increasing event is decreasing · Harris–FKG inequality for a positively associated probability measure

DefinitionOpen connection inside an overlap rectangle#✓fully proved

An open path inside the overlap rect m m' c d from p to q.

def OverlapConnection (ω : ConfigSpace (Sym2 (Site 2))) (m m' c d : ℤ)
    (p q : Site 2) (hp : p ∈ rect m m' c d) (hq : q ∈ rect m m' c d) : Prop :=
  ConnectedWithin 2 ω (rect m m' c d) ⟨p, hp⟩ ⟨q, hq⟩

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 · Integer rectangle in the plane lattice

Used byConnection event inside an overlap rectangle

DefinitionConnection event inside an overlap rectangle#✓fully proved

The event OverlapConnection.

def overlapConnectionEvent (m m' c d : ℤ) (p q : Site 2)
    (hp : p ∈ rect m m' c d) (hq : q ∈ rect m m' c d) :
    Set (ConfigSpace (Sym2 (Site 2))) :=
  {ω | OverlapConnection ω m m' c d p q hp hq}

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Integer rectangle in the plane lattice · Open connection inside an overlap rectangle

Used byMeasurability of the overlap connection event

TheoremMeasurability of the overlap connection event#✓fully proved

A connection event inside a rectangular overlap is measurable.

theorem measurableSet_overlapConnectionEvent (m m' c d : ℤ) (p q : Site 2)
    (hp : p ∈ rect m m' c d) (hq : q ∈ rect m m' c d) :
    MeasurableSet (overlapConnectionEvent m m' c d p q hp hq)

Uses 5

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Integer rectangle in the plane lattice · Connection event inside an overlap rectangle

Proof usesMeasurability of connection inside a set

DefinitionGluing horizontal crossings through a vertical overlap crossing#✓fully proved

For the configuration ω: horizontal crossings of [a, m'] × [c, d] and of [m, b] × [c, d] together with a vertical crossing of the overlap [m, m'] × [c, d] imply a horizontal crossing of [a, b] × [c, d].

def HVIntersectionProperty (ω : ConfigSpace (Sym2 (Site 2))) (a m m' b c d : ℤ) : Prop :=
  HorizontalCrossing ω a m' c d → VerticalCrossing ω m m' c d →
    HorizontalCrossing ω m b c d → HorizontalCrossing ω a b c d

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Open left–right crossing of a general rectangle · Open bottom–top crossing of a general rectangle

Used byRSW gluing from side separation

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.