The off-centre carrier for wired q = 2 FK marginals

6 fully proved

A. Translated wired marginals

LemmaTranslated wired marginals converge to the wired density#✓fully proved

The wired marginals of the translated edge e + v in v + Λ_{N+k} converge to the wired q = 2 density of e.

lemma occ_translated_tendsto_wiredDensity (N : ℕ) (v : Site d) (eb' : Sym2 (boxVerts d N))
    {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    Tendsto (fun k =>
        edgeMargProb
            (wiredFkProb (fvs_transBoxGraph d (N + k) v) (fvs_transBoxBoundary d (N + k) v) p 2)
            (Sym2.map (fvs_transEquiv d (N + k) v) (innerEdgeLE d (Nat.le_add_right N k) eb')))
      atTop (𝓝 (wiredEdgeDensity d 2 (edgeIncl d N eb') p))

Uses 28

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge marginal of a mass function · Translated box in \(\mathbb{Z}^d\) · Vertex boundary of a translated box · Nearest-neighbour graph on a translated box · Vertex type of a translated box · Translation from the centered box onto a translated box · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Wired infinite-volume edge density · Wired random-cluster probability of a configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesConfiguration space of a statistical-mechanics model · Vertex boundary of a box · Event that a box edge is open · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Restriction of a configuration from \(\Lambda_m\) to \(\Lambda_n\) · Restriction to \(\Lambda_n\) factors through \(\Lambda_m\) · Event that an edge is open · Probability of an ambient FK configuration · Wired infinite-volume measure as limit on increasing cylinder events · Translation covariance of FK edge marginals on boxes · Wired random-cluster measure on a box · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired infinite-volume random-cluster measure · Increasing event

LemmaFree density is at most each translated wired marginal#✓fully proved

The free q = 2 density of e is at most the wired marginal of e + v in v + Λ_{N+k}.

lemma occ_translated_between_iv (N : ℕ) (v : Site d) (eb' : Sym2 (boxVerts d N))
    {p : ℝ} (hp : 0 < p) (hp1 : p < 1) (k : ℕ) :
    freeEdgeDensity d 2 (edgeIncl d N eb') p
        ≤ edgeMargProb
            (wiredFkProb (fvs_transBoxGraph d (N + k) v) (fvs_transBoxBoundary d (N + k) v) p 2)
            (Sym2.map (fvs_transEquiv d (N + k) v) (innerEdgeLE d (Nat.le_add_right N k) eb'))

Uses 37

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge marginal of a mass function · Free infinite-volume edge density · Translated box in \(\mathbb{Z}^d\) · Vertex boundary of a translated box · Nearest-neighbour graph on a translated box · Vertex type of a translated box · Translation from the centered box onto a translated box · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Wired random-cluster probability of a configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesConfiguration space of a statistical-mechanics model · Vertex boundary of a box · Event that a box edge is open · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Restriction of a configuration from \(\Lambda_m\) to \(\Lambda_n\) · Restriction to \(\Lambda_n\) factors through \(\Lambda_m\) · Event that an edge is open · Probability of an ambient FK configuration · Infimum of wired box probabilities of a box event · Wired infinite-volume probability equals the infimum over boxes · Free \(q=2\) box masses of increasing cylinders tend to infinite volume · Wired infinite-volume measure as limit on increasing cylinder events · Free random-cluster measure on a box · Free box measure dominated by the wired one for \(q \ge 1\) · Free infinite-volume random-cluster measure · Translation covariance of FK edge marginals on boxes · Cylinder events of a box are measurable · Wired infinite-volume edge density · Wired random-cluster measure on a box · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired infinite-volume random-cluster measure · Increasing event · Stochastic domination compares real-valued masses

B. Free and wired densities

LemmaSecant bound gives free–wired density agreement off a countable set#✓fully proved

Under the secant comparison wired(p') ≤ free(p) for p' < p, the free and wired densities of a box edge agree for all p ∈ (0, 1) outside a countable set, namely the discontinuities of the monotone wired density.

lemma occ_free_eq_wired_off_countable (N : ℕ) (eb' : Sym2 (boxVerts d N))
    (hsecant : ∀ p ∈ Ioo (0 : ℝ) 1, ∀ p' ∈ Ioo (0 : ℝ) 1, p' < p →
      wiredEdgeDensity d 2 (edgeIncl d N eb') p' ≤ freeEdgeDensity d 2 (edgeIncl d N eb') p) :
    ∃ S : Set ℝ, S.Countable ∧ ∀ p ∈ Ioo (0 : ℝ) 1, p ∉ S →
      freeEdgeDensity d 2 (edgeIncl d N eb') p = wiredEdgeDensity d 2 (edgeIncl d N eb') p

Uses 32

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Free infinite-volume edge density · Wired infinite-volume edge density

Proof usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring · Boundary clique gives the wired random-cluster measure · Boundary-graph FK measure increases in \(p\) for \(q \ge 1\) · Vertex boundary of a box · Event that a box edge is open · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Restriction of a configuration from \(\Lambda_m\) to \(\Lambda_n\) · Restriction to \(\Lambda_n\) factors through \(\Lambda_m\) · Monotonicity of restriction between boxes · Event that an edge is open · Free \(q=2\) box masses of increasing cylinders tend to infinite volume · Wired infinite-volume measure as limit on increasing cylinder events · Free random-cluster measure on a box · Free box measure dominated by the wired one for \(q \ge 1\) · Free infinite-volume random-cluster measure · Cylinder events of a box are measurable · Wired random-cluster measure on a box · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired random-cluster probability of a configuration · Wired infinite-volume random-cluster measure · Increasing event · Site of the hypercubic lattice · Complete graph on the boundary vertices · Box \((-n, n)^d\) in the hypercubic lattice · Boundary wiring relation · Stochastic domination compares real-valued masses

C. The off-centre carrier

LemmaOff-centre carrier vanishes by translation covariance#✓fully proved

The off-centre carrier vanishes for every k, by translation covariance of the wired box measures.

lemma occ_offCentreCarrier_eq_zero (N : ℕ) (v : Site d) (eb' : Sym2 (boxVerts d N))
    (p q : ℝ) (k : ℕ) :
    fbd_offCentreCarrier N v eb' p q k = 0

Uses 16 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Wired-marginal difference between a box and its translate · Site of the hypercubic lattice

Proof usesVertex boundary of a box · Nearest-neighbour graph on a box · Edge marginal of a mass function · Probability of an ambient FK configuration · Translation covariance of FK edge marginals on boxes · Translated box in \(\mathbb{Z}^d\) · Vertex boundary of a translated box · Nearest-neighbour graph on a translated box · Vertex type of a translated box · Translation from the centered box onto a translated box · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Wired random-cluster probability of a configuration · Box \((-n, n)^d\) in the hypercubic lattice

Used byOff-centre carrier tends to zero

LemmaOff-centre carrier tends to zero#✓fully proved

The off-centre carrier tends to zero, for every p.

lemma occ_offCentreCarrier (N : ℕ) (v : Site d) (eb' : Sym2 (boxVerts d N)) (p : ℝ) :
    Tendsto (fbd_offCentreCarrier N v eb' p 2) atTop (𝓝 0)

Uses 4 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Wired-marginal difference between a box and its translate · Site of the hypercubic lattice

Proof usesOff-centre carrier vanishes by translation covariance

Used byEqual wired densities from equal translated marginals

LemmaEqual wired densities from equal translated marginals#✓fully proved

If for every k the wired marginal of e' + v in v + Λ_{N+k} equals the wired marginal of e in Λ_{N+k}, then e and e' have the same wired density.

lemma occ_wired_density_eq_of_translation_cofinal (N : ℕ) (v : Site d)
    (eb eb' : Sym2 (boxVerts d N)) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (htrans : ∀ k,
        edgeMargProb
            (wiredFkProb (fvs_transBoxGraph d (N + k) v) (fvs_transBoxBoundary d (N + k) v) p 2)
            (Sym2.map (fvs_transEquiv d (N + k) v) (innerEdgeLE d (Nat.le_add_right N k) eb'))
          = edgeMargProb (wiredFkProb (boxGraph d (N + k)) (boxBoundary d (N + k)) p 2)
            (innerEdgeLE d (Nat.le_add_right N k) eb)) :
    wiredEdgeDensity d 2 (edgeIncl d N eb) p
      = wiredEdgeDensity d 2 (edgeIncl d N eb') p

Uses 28

Statement usesVertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge marginal of a mass function · Translated box in \(\mathbb{Z}^d\) · Vertex boundary of a translated box · Nearest-neighbour graph on a translated box · Vertex type of a translated box · Translation from the centered box onto a translated box · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Wired infinite-volume edge density · Wired random-cluster probability of a configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesConfiguration space of a statistical-mechanics model · Event that a box edge is open · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Restriction of a configuration from \(\Lambda_m\) to \(\Lambda_n\) · Restriction to \(\Lambda_n\) factors through \(\Lambda_m\) · Wired-marginal difference between a box and its translate · Event that an edge is open · Wired infinite-volume measure as limit on increasing cylinder events · Off-centre carrier tends to zero · Wired random-cluster measure on a box · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired infinite-volume random-cluster measure · Increasing event

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.