One-step comparison of wired boundary-connection probabilities

3 fully proved

B. Boundary-connection events

DefinitionOrigin-to-\(\partial\Lambda_n\) event as an event on \(\Lambda_{n+1}\)#✓fully proved

The event on Λ_(n+1) that the origin is connected to ∂Λ_n by open edges of Λ_n.

def innerBdryFinEvent (d n : ℕ) : Set (ConfigSpace (Sym2 (boxVerts d (n + 1)))) :=
  innerRestrict d n ⁻¹'
    {ω : ConfigSpace (Sym2 (boxVerts d n)) |
      ConnToBdry (boxGraph d n) (boxBoundary d n) ω (IsingFK.boxOrigin d n)}

Uses 7 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Vertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Restriction of a next-box configuration to the inner edges · Open connection of a vertex to the boundary · Origin as a vertex of the box graph

Used byClosed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\)

D. The conditional comparison

LemmaClosed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law#✓fully proved

With all annulus edges closed and a wiring made of the inner-boundary clique and an annulus wiring D, the conditional measure on Λ_(n+1) equals the wired measure on Λ_n, on any event pulled back by crossExt.

lemma condBcProb_add_sum_eq_smallerBox (d n : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq0 : 0 < q)
    {D : SimpleGraph (boxVerts d (n + 1))} [DecidableRel D.Adj] (hD : IsAnnulusWiring d n D)
    (B : Set (ConfigSpace (Sym2 (boxVerts d (n + 1))))) :
    (∑ ρ, B.indicator (fun _ => (1 : ℝ)) ρ *
        condBcProb (boxGraph d (n + 1))
          (StatMech.Lattice.boundaryCliqueGraph (innerBdry d n) ⊔ D) p q
          (innerEdgeFinset d n) (fun _ => false) ρ)
      = ∑ ω : ConfigSpace (Sym2 (boxVerts d n)),
          (crossExt d n ⁻¹' B).indicator (fun _ => (1 : ℝ)) ω
            * wiredFkProb (boxGraph d n) (boxBoundary d n) p q ω

Uses 40 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Wiring with every edge inside the annulus · Vertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Conditional random-cluster measure with a boundary wiring · Extension of a configuration closing the annulus edges · Vertex on the boundary of the inner box · Edges of the next box coming from the inner box · Wired random-cluster probability of a configuration · Site of the hypercubic lattice · Complete graph on the boundary vertices · Box \((-n, n)^d\) in the hypercubic lattice · Boundary wiring relation

Proof usesAgreement of configurations off an edge set · Vertices of the annulus between consecutive boxes · Vertex of the next box lying in the inner box · Restriction of a wiring to the annulus vertices · Random-cluster weight with a boundary wiring · Inclusion of box vertices into the next box · Fibre of configurations agreeing off an edge set · Extra-wired components as inner plus annulus-wiring components · Annulus constant counting the components of an extra wiring · Extended open graph with the inner box boundary wired · Extended wired graph with an extra wiring added · Bernoulli edge product · Partition function of a conditioning fibre · Inclusion of box edges into the next box · Restriction of a next-box configuration to the inner edges · Open graph of a box configuration with the box boundary wired · Number of next-box edges not coming from the inner box · Number of clusters under a boundary wiring · Open subgraph of an edge configuration · Wired random-cluster weight · Wired random-cluster partition function · Open edge in a bond configuration · Hypercubic lattice \(\mathbb{Z}^d\) · Number of open clusters with wired boundary conditions · Open subgraph of a bond configuration · Wired open graph

Used byClosed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\)

LemmaClosed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\)#✓fully proved

At q = 2, the wired measure on Λ_(n+1) conditioned on all annulus edges closed gives {0 ↔ ∂Λ_n} at most φ¹_n(0 ↔ ∂Λ_n).

lemma condWiredSucc_le_smallerBox (d n : ℕ) {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    (∑ ρ, (innerBdryFinEvent d n).indicator (fun _ => (1 : ℝ)) ρ *
        condBcProb (boxGraph d (n + 1))
          (StatMech.Lattice.boundaryCliqueGraph (boxBoundary d (n + 1))) p 2
          (innerEdgeFinset d n) (fun _ => false) ρ)
      ≤ (wiredFiniteMeasure d n hp hp1 (by norm_num : (0 : ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real (boxBdryConnEvent d n)

Uses 40

Statement usesConfiguration space of a statistical-mechanics model · Event that the box origin connects to the box boundary · Vertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Conditional random-cluster measure with a boundary wiring · Origin-to-\(\partial\Lambda_n\) event as an event on \(\Lambda_{n+1}\) · Edges of the next box coming from the inner box · Wired random-cluster measure on a box · Site of the hypercubic lattice · Complete graph on the boundary vertices · Box \((-n, n)^d\) in the hypercubic lattice · Boundary wiring relation

Proof usesOpen connection between two vertices · Wiring with every edge inside the annulus · Vertex of the next box lying in the inner box · Event that two sites are joined by open edges inside a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Inclusion of box vertices into the next box · Closed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Event that two vertices are joined by open edges · Extension of a configuration closing the annulus edges · Inclusion of box edges into \(\mathbb{Z}^d\) · Bernoulli edge product · Extension of a box configuration by closed edges · Vertex on the boundary of the inner box · Inclusion of box edges into the next box · Restriction of a next-box configuration to the inner edges · Open subgraph of an edge configuration · Monotonicity of the open subgraph in the configuration · Wired random-cluster measure as a probability mass function · Wired random-cluster probability of a configuration · Wired measure conditionally dominated by larger wirings, \(q \ge 1\) · Wired random-cluster weight · Wired random-cluster partition function · Increasing event · Open connection of a vertex to the boundary · Origin as a vertex of the box graph · Number of open clusters with wired boundary conditions · Inner vertex boundary of a box

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.