FKG inequality and monotonicity of random-cluster measures

DefinitionProbability that an edge is open under the random-cluster measure#✓fully proved

The probability φ_{G,p,q}(e open) that the edge e is open.

noncomputable def edgeMarginalOpen (p q : ℝ) (e : Sym2 V) : ℝ :=
  ∑ ω ∈ Finset.univ.filter (fun ω : ConfigSpace (Sym2 V) => ω e = true), fkProb G p q ω

Uses 2 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Probability of an ambient FK configuration

Used byEdge density lies between \(p/(p+q(1-p))\) and \(p\) for \(q \ge 1\)

LemmaEdge density lies between \(p/(p+q(1-p))\) and \(p\) for \(q \ge 1\)#✓fully proved

For q ≥ 1, every edge of G is open with probability between p / (p + q(1 - p)) and p.

lemma edge_density_bounds {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    {e : Sym2 V} (he : e ∈ G.edgeFinset) :
    p / (p + q * (1 - p)) ≤ edgeMarginalOpen G p q e ∧ edgeMarginalOpen G p q e ≤ p

Uses 13

Statement usesProbability that an edge is open under the random-cluster measure

Proof usesConfiguration space of a statistical-mechanics model · Conditional probability that an edge is open given the rest · Bernoulli edge product · Bernoulli product over the edges other than one edge · Probability of an ambient FK configuration · Unnormalized random-cluster weight · Ambient FK normalizer · Number of open clusters · Opening an edge lowers the cluster count by at most one · Opening an edge does not increase the cluster count · Closing a coordinate of a configuration · Opening a coordinate of a configuration

LemmaSupermodularity of the number of connected components#✓fully proved

The number of connected components of simple graphs on a finite vertex set is supermodular: #comp(G₁) + #comp(G₂) ≤ #comp(G₁ ⊔ G₂) + #comp(G₁ ⊓ G₂).

lemma card_connectedComponent_submodular (G₁ G₂ : SimpleGraph V)
    [DecidableRel G₁.Adj] [DecidableRel G₂.Adj] :
    Nat.card G₁.ConnectedComponent + Nat.card G₂.ConnectedComponent
      ≤ Nat.card (G₁ ⊔ G₂).ConnectedComponent + Nat.card (G₁ ⊓ G₂).ConnectedComponent

Used by 1

Used bySupermodularity of the random-cluster cluster count

LemmaSupermodularity of the random-cluster cluster count#✓fully proved

The cluster count of the random-cluster model is supermodular in the configuration.

lemma numClusters_supermodular (a b : ConfigSpace (Sym2 V)) :
    numClusters G a + numClusters G b
      ≤ numClusters G (a ⊔ b) + numClusters G (a ⊓ b)

Uses 4 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Number of open clusters

Proof usesSupermodularity of the number of connected components · Open subgraph of an edge configuration

Used byHolley's cross inequality for FK measures, \(p_1 \le p_2\), \(q \ge 1\) · FKG lattice condition for the random-cluster measure

LemmaFKG lattice condition for the random-cluster measure#✓fully proved

For q ≥ 1 and p ∈ (0, 1), the random-cluster measure satisfies the FKG lattice condition φ(a) φ(b) ≤ φ(a ⊔ b) φ(a ⊓ b).

lemma fkProb_FKGLatticeCondition {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q) :
    FKGLatticeCondition (fun ω => fkProb G p q ω)

Uses 8 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Probability of an ambient FK configuration · FKG lattice condition

Proof usesBernoulli edge product · Unnormalized random-cluster weight · Ambient FK normalizer · Number of open clusters · Supermodularity of the random-cluster cluster count

Used byFKG inequality for the random-cluster model · FKG inequality for increasing random-cluster events

TheoremFKG inequality for the random-cluster model#✓fully proved

For q ≥ 1, increasing functions are positively correlated under φ_{G,p,q}: φ(f) φ(g) ≤ φ(f g). (Fortuin–Kasteleyn–Ginibre, Comm. Math. Phys. 22, 1971; Grimmett, The Random-Cluster Model, 2006, Theorem 3.8.)

theorem fkProb_positively_associated {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    {f g : ConfigSpace (Sym2 V) → ℝ} (hf : Monotone f) (hg : Monotone g) :
    (∑ ω, fkProb G p q ω * f ω) * (∑ ω, fkProb G p q ω * g ω)
      ≤ ∑ ω, fkProb G p q ω * (f ω * g ω)

Uses 8

Statement usesConfiguration space of a statistical-mechanics model · Probability of an ambient FK configuration

Proof usesBernoulli edge product · FKG lattice condition for the random-cluster measure · Unnormalized random-cluster weight · Ambient FK normalizer · Number of open clusters · FKG inequality

LemmaFKG inequality for increasing random-cluster events#✓fully proved

The FKG inequality for increasing events: φ(A) φ(B) ≤ φ(A ∩ B) for q ≥ 1.

lemma fkProb_positively_associated_events {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    {A B : Set (ConfigSpace (Sym2 V))} (hA : IsIncreasing A) (hB : IsIncreasing B) :
    (∑ ω, fkProb G p q ω * A.indicator (fun _ => (1 : ℝ)) ω)
        * (∑ ω, fkProb G p q ω * B.indicator (fun _ => (1 : ℝ)) ω)
      ≤ ∑ ω, fkProb G p q ω * (A ∩ B).indicator (fun _ => (1 : ℝ)) ω

Uses 9 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Probability of an ambient FK configuration · Increasing event

Proof usesBernoulli edge product · FKG lattice condition for the random-cluster measure · Unnormalized random-cluster weight · Ambient FK normalizer · Number of open clusters · FKG inequality for increasing events

Used byFKG inequality for free \(q = 2\) box measures on smaller-box events · FKG inequality for connection events for \(q \ge 1\)

DefinitionKernel of the Laplacian of the open subgraph#✓fully proved

The kernel of the Laplacian of the open subgraph of ω, a subspace of V → ℝ.

noncomputable def kerLap (ω : ConfigSpace (Sym2 V)) : Submodule ℝ (V → ℝ) :=
  LinearMap.ker (Matrix.toLin' ((openSub G ω).lapMatrix ℝ))

Uses 2 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Open subgraph of an edge configuration

Used byComparison inequalities · Number of open clusters equals the dimension of the Laplacian kernel · Opening an edge lowers the cluster count by at most one

LemmaNumber of open clusters equals the dimension of the Laplacian kernel#✓fully proved

The number of open clusters equals the dimension of the kernel of the Laplacian of the open subgraph.

lemma numClusters_eq_finrank (ω : ConfigSpace (Sym2 V)) :
    numClusters G ω = Module.finrank ℝ (kerLap G ω)

Uses 4 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Kernel of the Laplacian of the open subgraph · Number of open clusters

Proof usesOpen subgraph of an edge configuration

Used byComparison inequalities · Opening an edge lowers the cluster count by at most one

LemmaHolley's cross inequality for FK measures, \(p_1 \le p_2\), \(q \ge 1\)#✓fully proved

Holley's cross inequality for two random-cluster measures with p₁ ≤ p₂ and the same q ≥ 1.

lemma fkProb_cross {p1 p2 q : ℝ} (hp1 : 0 < p1) (hp1' : p1 < 1) (hp2 : 0 < p2)
    (hp2' : p2 < 1) (hle : p1 ≤ p2) (hq : 1 ≤ q) (a b : ConfigSpace (Sym2 V)) :
    fkProb G p1 q a * fkProb G p2 q b
      ≤ fkProb G p1 q (a ⊓ b) * fkProb G p2 q (a ⊔ b)

Uses 7 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Probability of an ambient FK configuration

Proof usesBernoulli edge product · Unnormalized random-cluster weight · Ambient FK normalizer · Number of open clusters · Supermodularity of the random-cluster cluster count

Used byMonotonicity in \(p\) of free \(q = 2\) edge marginals on a finite graph · Random-cluster measure increases stochastically in \(p\) when \(q \ge 1\) · Monotonicity of the random-cluster measure in p

TheoremMonotonicity of the random-cluster measure in p#✓fully proved

For q ≥ 1 and p₁ ≤ p₂, φ_{p₁,q}(A) ≤ φ_{p₂,q}(A) for every increasing event A (Grimmett, The Random-Cluster Model, 2006, Theorem 3.21).

theorem fkProb_stochastically_increasing {p1 p2 q : ℝ} (hp1 : 0 < p1) (hp1' : p1 < 1)
    (hp2 : 0 < p2) (hp2' : p2 < 1) (hle : p1 ≤ p2) (hq : 1 ≤ q)
    {A : Set (ConfigSpace (Sym2 V))} (hA : IsIncreasing A) :
    (∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * fkProb G p1 q ω)
      ≤ ∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * fkProb G p2 q ω

Uses 9

Statement usesConfiguration space of a statistical-mechanics model · Probability of an ambient FK configuration · Increasing event

Proof usesBernoulli edge product · Holley's cross inequality for FK measures, \(p_1 \le p_2\), \(q \ge 1\) · Unnormalized random-cluster weight · Ambient FK normalizer · Number of open clusters · Holley inequality for increasing events

DefinitionNumber of open edges of a configuration#✓fully proved

The number of open edges of G in ω. Same as openCount in Tilt.

noncomputable def chOpenCount (ω : ConfigSpace (Sym2 V)) : ℕ :=
  (G.edgeFinset.filter (fun e => ω e = true)).card

Uses 1 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model

Used byFK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition · Comparison inequalities · Cluster count plus open-edge count is monotone

DefinitionEdges closed in one configuration and open in another#✓fully proved

The edges of G closed in b and open in c.

noncomputable def diffSet (b c : ConfigSpace (Sym2 V)) : Finset (Sym2 V) :=
  G.edgeFinset.filter (fun e => b e = false ∧ c e = true)

Uses 1 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model

Used byFK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition · Comparison inequalities · Cluster count plus open-edge count is monotone

LemmaCluster count plus open-edge count is monotone#✓fully proved

For b ≤ c, k(b) + o(b) ≤ k(c) + o(c): opening an edge lowers the cluster count by at most one.

lemma numClusters_add_openCount_mono : ∀ (n : ℕ) (b c : ConfigSpace (Sym2 V)),
    b ≤ c → (diffSet G b c).card = n →
    numClusters G b + chOpenCount G b ≤ numClusters G c + chOpenCount G c

Uses 8 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Number of open edges of a configuration · Edges closed in one configuration and open in another · Number of open clusters

Proof usesOpening an edge lowers the cluster count by at most one · Open subgraph of an edge configuration · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Used byFK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition · Comparison inequalities

DefinitionReduced density \(p/(p + q(1-p))\)#✓fully proved

The reduced density p / (p + q(1 - p)): the Bernoulli parameter dominated by φ_{p,q}.

noncomputable def reducedDensity (p q : ℝ) : ℝ := p / (p + q * (1 - p))

Used by 5

Used byFK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition · Comparison inequalities

LemmaRandom-cluster measure increases stochastically in \(p\) when \(q \ge 1\)#✓fully proved

For q ≥ 1 the random-cluster measure is stochastically increasing in p.

lemma fk_monotone_in_p {p₁ p₂ q : ℝ} (hp₁ : 0 < p₁) (hp₁' : p₁ < 1) (hp₂ : 0 < p₂)
    (hp₂' : p₂ < 1) (hle : p₁ ≤ p₂) (hq : 1 ≤ q) :
    measOfMass (fkProb G p₁ q) ≼ measOfMass (fkProb G p₂ q)

Uses 10

Statement usesProbability of an ambient FK configuration · Finite measure with prescribed point masses · Stochastic domination of measures on configurations

Proof usesConfiguration space of a statistical-mechanics model · Bernoulli edge product · Holley's cross inequality for FK measures, \(p_1 \le p_2\), \(q \ge 1\) · Unnormalized random-cluster weight · Ambient FK normalizer · Holley's inequality · Number of open clusters

TheoremComparison inequalities#✓fully proved

For q ≥ 1, P_{p/(p + q(1 - p))} ≼ φ_{p,q} ≼ P_p, with every law extended uniformly to loops and nonedges. On graph-edge marginals, this gives the usual FK/Bernoulli comparison (Fortuin 1972; Grimmett, The Random-Cluster Model, 2006, Theorem 3.21).

theorem fk_bernoulli_sandwich {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q) :
    measOfMass (fkProb G (reducedDensity p q) 1) ≼ measOfMass (fkProb G p q)
      ∧ measOfMass (fkProb G p q) ≼ measOfMass (fkProb G p 1)

Uses 17

Statement usesProbability of an ambient FK configuration · Finite measure with prescribed point masses · Reduced density \(p/(p + q(1-p))\) · Stochastic domination of measures on configurations

Proof usesConfiguration space of a statistical-mechanics model · Number of open edges of a configuration · Edges closed in one configuration and open in another · Bernoulli edge product · Unnormalized random-cluster weight · At \(q = 1\) the random-cluster weight is the Bernoulli product · Ambient FK normalizer · Holley's inequality · Kernel of the Laplacian of the open subgraph · Number of open clusters · Cluster count plus open-edge count is monotone · Number of open clusters equals the dimension of the Laplacian kernel · Open subgraph of an edge configuration

LemmaMixed supermodularity of free and wired cluster counts#✓fully proved

Mixed supermodularity of cluster counts: k(a) + k¹(b) ≤ k(a ⊓ b) + k¹(a ⊔ b), where k¹ counts clusters with the boundary wired.

lemma mixed_supermodular (a b : ConfigSpace (Sym2 V)) :
    numClusters G a + numClustersWired G bdry b
      ≤ numClusters G (a ⊓ b) + numClustersWired G bdry (a ⊔ b)

Uses 10 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Number of open clusters · Number of open clusters with wired boundary conditions

Proof usesOpen subgraph of an edge configuration · Open edge in a bond configuration · Complete graph on the boundary vertices · Number of open clusters with free boundary conditions · Open subgraph of a bond configuration · Boundary wiring relation · Wired open graph

Used byHolley's condition for free and wired weights when \(q \ge 1\)

LemmaHolley's condition for free and wired weights when \(q \ge 1\)#✓fully proved

Holley's condition for the free and wired weights when q ≥ 1. See also bcWeight_cross, which contains this as the case of boundary wirings ⊥ ≤ clique.

lemma freeWiredWeight_cross {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    (a b : ConfigSpace (Sym2 V)) :
    fkWeight G p q a * wiredFkWeight G bdry p q b
      ≤ fkWeight G p q (a ⊓ b) * wiredFkWeight G bdry p q (a ⊔ b)

Uses 7 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Unnormalized random-cluster weight · Wired random-cluster weight

Proof usesBernoulli edge product · Mixed supermodularity of free and wired cluster counts · Number of open clusters · Number of open clusters with wired boundary conditions

Used byHolley's condition for free and wired probabilities when \(q \ge 1\)

LemmaHolley's condition for free and wired probabilities when \(q \ge 1\)#✓fully proved

Holley's condition for the free and wired probabilities when q ≥ 1.

lemma freeWiredProb_cross {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    (a b : ConfigSpace (Sym2 V)) :
    fkProb G p q a * wiredFkProb G bdry p q b
      ≤ fkProb G p q (a ⊓ b) * wiredFkProb G bdry p q (a ⊔ b)

Uses 11 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Probability of an ambient FK configuration · Wired random-cluster probability of a configuration

Proof usesBernoulli edge product · Unnormalized random-cluster weight · Ambient FK normalizer · Holley's condition for free and wired weights when \(q \ge 1\) · Number of open clusters · Wired random-cluster weight · Wired random-cluster partition function · Number of open clusters with wired boundary conditions

Used byFree–wired domination on a finite graph for \(q \ge 1\)

LemmaFree–wired domination on a finite graph for \(q \ge 1\)#✓fully proved

For q ≥ 1 the free random-cluster measure gives every increasing event at most the probability the wired measure gives it.

lemma fkProb_le_wiredFkProb_increasing {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    {A : Set (ConfigSpace (Sym2 V))} (hA : IsIncreasing A) :
    (∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * fkProb G p q ω)
      ≤ ∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * wiredFkProb G bdry p q ω

Uses 13 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Probability of an ambient FK configuration · Wired random-cluster probability of a configuration · Increasing event

Proof usesBernoulli edge product · Unnormalized random-cluster weight · Ambient FK normalizer · Holley's condition for free and wired probabilities when \(q \ge 1\) · Number of open clusters · Wired random-cluster weight · Wired random-cluster partition function · Number of open clusters with wired boundary conditions · Holley inequality for increasing events

Used byFK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition · Free box measure dominated by the wired one for \(q \ge 1\)

LemmaFree box measure dominated by the wired one for \(q \ge 1\)#✓fully proved

For q ≥ 1 the free box measure is stochastically dominated by the wired box measure on ℤ^d: φ⁰_n ≼ φ¹_n.

lemma freeFiniteMeasure_dominated (d n : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q) :
    (freeFiniteMeasure d n hp hp1 (zero_lt_one.trans_le hq)
        : Measure (ConfigSpace (Sym2 (Site d))))
      ≼ (wiredFiniteMeasure d n hp hp1 (zero_lt_one.trans_le hq)
        : Measure (ConfigSpace (Sym2 (Site d))))

Uses 24 · Used by 9

Statement usesConfiguration space of a statistical-mechanics model · Free random-cluster measure on a box · Wired random-cluster measure on a box · Site of the hypercubic lattice · Stochastic domination of measures on configurations

Proof 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\) · Bernoulli edge product · Extension of a box configuration by closed edges · Ambient random-cluster law as a probability mass function · Probability of an ambient FK configuration · Free–wired domination on a finite graph for \(q \ge 1\) · Unnormalized random-cluster weight · Ambient FK normalizer · Number of open clusters · Wired random-cluster measure as a probability mass function · Wired random-cluster probability of a configuration · Wired random-cluster weight · Wired random-cluster partition function · Increasing event · Box \((-n, n)^d\) in the hypercubic lattice · Number of open clusters with wired boundary conditions

Used byWired \(q = 2\) measure dominates the free one on increasing cylinders · Free limit at most wired limit along a common subsequence, \(q \ge 1\) · Secant bound gives free–wired density agreement off a countable set · Free density is at most each translated wired marginal · Per-box \(q = 2\) uniqueness off a countable set of tilts · Secant bound gives \(q = 2\) edge-event uniqueness off a countable set · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\)

DefinitionNumber of clusters under a boundary wiring#✓fully proved

The number of clusters of ω under the boundary wiring C: connected components of the open subgraph of ω joined with C.

noncomputable def numClustersBC (C : SimpleGraph V) [DecidableRel C.Adj]
    (ω : ConfigSpace (Sym2 V)) : ℕ :=
  Nat.card (openSub G ω ⊔ C).ConnectedComponent

Uses 2 · Used by 32

Statement usesConfiguration space of a statistical-mechanics model · Open subgraph of an edge configuration

Used byEdwards–Sokal one-point identity · Boundary-graph comparison \(\varphi^{C'}(A) \le q^N \varphi^C(A)\) · Empty wiring gives the free random-cluster measure · Boundary clique gives the wired random-cluster measure · Holley's condition for probabilities with nested wirings, \(q \ge 1\) · Disintegration of a boundary-wired measure over conditioning fibres · Random-cluster comparison of boundary conditions for \(q \ge 1\) · Boundary-graph FK measure increases in \(p\) for \(q \ge 1\) · FKG inequality for the random-cluster measure, \(q \ge 1\) · Random-cluster weight with a boundary wiring · Holley's condition for weights with nested wirings, \(q \ge 1\) · Holley's condition for nested-wiring conditional measures, \(q \ge 1\) · Conditional measures increase with the wiring for \(q \ge 1\) · Mixed supermodularity of cluster counts for nested wirings · Domain Markov property for the wired measure on nested boxes · Wired cluster count of a glued configuration splits additively · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Factorization of the wired FK weight of a glued configuration · Glued cluster count is induced-wiring count plus outside-only clusters · Outer wired fibre masses sum to one · Inner wired domination of the restricted outer wired measure · Closed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Free measure is dominated by induced-wiring measures for \(q \ge 1\) · Random-cluster weight of a glued configuration factorizes · Cluster count of a glued configuration splits additively · Domain Markov property for the wired box measure · Masses of the conditioning fibres sum to one · Wired box measures decrease on inner increasing events for \(q \ge 1\) · Per-box uniqueness of the random-cluster measures off a countable set · Free off-centre lower bound by the recentred small-box marginal · Translation invariance of the free \(q = 2\) infinite-volume measure · Ergodicity of the wired random-cluster measure

LemmaMixed supermodularity of cluster counts for nested wirings#✓fully proved

Mixed supermodularity of cluster counts for nested wirings C ≤ C': k_C(a) + k_C'(b) ≤ k_C(a ⊓ b) + k_C'(a ⊔ b).

lemma mixed_supermodular_bc (C C' : SimpleGraph V) [DecidableRel C.Adj]
    [DecidableRel C'.Adj] (hCC' : C ≤ C') (a b : ConfigSpace (Sym2 V)) :
    numClustersBC G C a + numClustersBC G C' b
      ≤ numClustersBC G C (a ⊓ b) + numClustersBC G C' (a ⊔ b)

Uses 3 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Number of clusters under a boundary wiring

Proof usesOpen subgraph of an edge configuration

Used byBoundary-graph FK measure increases in \(p\) for \(q \ge 1\) · Holley's condition for weights with nested wirings, \(q \ge 1\)

DefinitionRandom-cluster weight with a boundary wiring#✓fully proved

The unnormalized random-cluster weight with boundary wiring C: edgeProduct G p ω · q ^ numClustersBC G C ω.

noncomputable def bcWeight (p q : ℝ) (ω : ConfigSpace (Sym2 V)) : ℝ :=
  edgeProduct G p ω * q ^ numClustersBC G C ω

Uses 3 · Used by 40

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli edge product · Number of clusters under a boundary wiring

Used byEdwards–Sokal one-point identity · Boundary-graph comparison \(\varphi^{C'}(A) \le q^N \varphi^C(A)\) · Random-cluster probability with a boundary wiring · Empty wiring gives the free random-cluster measure · Boundary clique gives the wired random-cluster measure · Holley's condition for probabilities with nested wirings, \(q \ge 1\) · Disintegration of a boundary-wired measure over conditioning fibres · Random-cluster comparison of boundary conditions for \(q \ge 1\) · Boundary-graph FK measure increases in \(p\) for \(q \ge 1\) · FKG inequality for the random-cluster measure, \(q \ge 1\) · Holley's condition for weights with nested wirings, \(q \ge 1\) · Partition function with a boundary wiring · Conditional random-cluster measure with a boundary wiring · Holley's condition for nested-wiring conditional measures, \(q \ge 1\) · Conditional measures increase with the wiring for \(q \ge 1\) · Partition function of a conditioning fibre · Domain Markov property for the wired measure on nested boxes · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Law of total probability over outside configurations · Factorization of the wired FK weight of a glued configuration · Conditional outer measure is the induced-wiring FK measure · Conditional outer probability as an induced-wiring probability · Factorization of the conditioned outer partition function · Outer wired fibre masses sum to one · Inner wired domination of the restricted outer wired measure · Closed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Domain Markov property · Free measure is dominated by induced-wiring measures for \(q \ge 1\) · Random-cluster weight of a glued configuration factorizes · Conditional partition function in terms of the induced wiring · Domain Markov property for the wired box measure · Configurations agreeing off \(F\) have equal conditional probabilities · Conditional wired decrease on inner increasing events for \(q \ge 1\) · Masses of the conditioning fibres sum to one · Wired \(\Lambda_{n+1}\) measure decomposed over outer configurations · Wired box measures decrease on inner increasing events for \(q \ge 1\) · Per-box uniqueness of the random-cluster measures off a countable set · Free off-centre lower bound by the recentred small-box marginal · Translation invariance of the free \(q = 2\) infinite-volume measure · Ergodicity of the wired random-cluster measure

DefinitionPartition function with a boundary wiring#✓fully proved

The partition function with boundary wiring C.

noncomputable def bcZ (p q : ℝ) : ℝ :=
  ∑ ω : ConfigSpace (Sym2 V), bcWeight G C p q ω

Uses 2 · Used by 25

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster weight with a boundary wiring

Used byEdwards–Sokal one-point identity · Boundary-graph comparison \(\varphi^{C'}(A) \le q^N \varphi^C(A)\) · Random-cluster probability with a boundary wiring · Empty wiring gives the free random-cluster measure · Boundary clique gives the wired random-cluster measure · Holley's condition for probabilities with nested wirings, \(q \ge 1\) · Disintegration of a boundary-wired measure over conditioning fibres · Random-cluster comparison of boundary conditions for \(q \ge 1\) · Boundary-graph FK measure increases in \(p\) for \(q \ge 1\) · FKG inequality for the random-cluster measure, \(q \ge 1\) · Domain Markov property for the wired measure on nested boxes · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Conditional outer measure is the induced-wiring FK measure · Factorization of the conditioned outer partition function · Outer wired fibre masses sum to one · Inner wired domination of the restricted outer wired measure · Domain Markov property · Free measure is dominated by induced-wiring measures for \(q \ge 1\) · Conditional partition function in terms of the induced wiring · Masses of the conditioning fibres sum to one · Wired box measures decrease on inner increasing events for \(q \ge 1\) · Per-box uniqueness of the random-cluster measures off a countable set · Free off-centre lower bound by the recentred small-box marginal · Translation invariance of the free \(q = 2\) infinite-volume measure · Ergodicity of the wired random-cluster measure

DefinitionRandom-cluster probability with a boundary wiring#✓fully proved

The random-cluster probability with boundary wiring C, bcWeight / bcZ.

noncomputable def bcProb (p q : ℝ) (ω : ConfigSpace (Sym2 V)) : ℝ :=
  bcWeight G C p q ω / bcZ G C p q

Uses 3 · Used by 50

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster weight with a boundary wiring · Partition function with a boundary wiring

Used byFK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Wired \(q = 2\) edge density is monotone in \(t\) · Wired box-boundary connection probability is monotone in \(p\) at \(q = 2\) · Edwards–Sokal one-point identity · Wired random-cluster probability of connecting to the boundary · Event mass under the random-cluster measure with a boundary graph · Boundary-graph comparison \(\varphi^{C'}(A) \le q^N \varphi^C(A)\) · Empty wiring gives the free random-cluster measure · Boundary clique gives the wired random-cluster measure · Holley's condition for probabilities with nested wirings, \(q \ge 1\) · Free–wired sandwich for boundary graphs inside the boundary clique · Sandwich between the free and all-wired boundary conditions · Disintegration of a boundary-wired measure over conditioning fibres · Random-cluster comparison of boundary conditions for \(q \ge 1\) · Boundary-graph FK measure increases in \(p\) for \(q \ge 1\) · FKG inequality for the random-cluster measure, \(q \ge 1\) · Boundary wirings lie between free and wired when \(q \ge 1\) · Wirings with the boundary clique dominate the wired measure, \(q \ge 1\) · Wired box measure dominates the induced-wiring measure for \(q \ge 1\) · Domain Markov property for the wired measure on nested boxes · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Law of total probability over outside configurations · Conditional outer wired probability at most the inner wired one, \(q \ge 1\) · Domination by the inner wired measure under a coarser induced wiring · Conditional outer measure is the induced-wiring FK measure · Conditional outer probability as an induced-wiring probability · Free inner measure is dominated by the conditional outer measure · Free inner measure is dominated by every induced-wiring measure · Inner wired domination for vertex sets of \(\mathbb{Z}^d\) · Outer wired fibre masses sum to one · Inner wired domination of the restricted outer wired measure · FKG lattice condition for the wired measure when \(q \ge 1\) · Domain Markov property · Conditional free measure as an induced-wiring measure · Conditional free measure dominates the smaller free box for \(q \ge 1\) · Free measure is dominated by induced-wiring measures for \(q \ge 1\) · Secant bound gives free–wired density agreement off a countable set · Conditional wired decrease on inner increasing events for \(q \ge 1\) · Masses of the conditioning fibres sum to one · Wired box measures decrease on increasing cylinder events at \(q = 2\) · Wired \(\Lambda_{n+1}\) measure of a \(\Lambda_n\) cylinder event as a sum · Wired \(\Lambda_{n+1}\) measure decomposed over outer configurations · Wired box measures decrease on inner increasing events for \(q \ge 1\) · Secant bound gives \(q = 2\) edge-event uniqueness off a countable set · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Free off-centre lower bound by the recentred small-box marginal · Translation invariance of the free \(q = 2\) infinite-volume measure · Ergodicity of the wired random-cluster measure

LemmaHolley's condition for weights with nested wirings, \(q \ge 1\)#✓fully proved

Holley's condition for the weights with nested wirings C ≤ C' and q ≥ 1.

lemma bcWeight_cross (C' : SimpleGraph V) [DecidableRel C'.Adj] (hCC' : C ≤ C')
    {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q) (a b : ConfigSpace (Sym2 V)) :
    bcWeight G C p q a * bcWeight G C' p q b
      ≤ bcWeight G C p q (a ⊓ b) * bcWeight G C' p q (a ⊔ b)

Uses 5 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster weight with a boundary wiring

Proof usesBernoulli edge product · Mixed supermodularity of cluster counts for nested wirings · Number of clusters under a boundary wiring

Used byHolley's condition for probabilities with nested wirings, \(q \ge 1\) · Holley's condition for nested-wiring conditional measures, \(q \ge 1\)

LemmaHolley's condition for probabilities with nested wirings, \(q \ge 1\)#✓fully proved

Holley's condition for the probabilities with nested wirings C ≤ C' and q ≥ 1.

lemma bcProb_cross (C' : SimpleGraph V) [DecidableRel C'.Adj] (hCC' : C ≤ C')
    {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q) (a b : ConfigSpace (Sym2 V)) :
    bcProb G C p q a * bcProb G C' p q b
      ≤ bcProb G C p q (a ⊓ b) * bcProb G C' p q (a ⊔ b)

Uses 7 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring

Proof usesRandom-cluster weight with a boundary wiring · Holley's condition for weights with nested wirings, \(q \ge 1\) · Partition function with a boundary wiring · Bernoulli edge product · Number of clusters under a boundary wiring

Used byRandom-cluster comparison of boundary conditions for \(q \ge 1\) · FKG inequality for the random-cluster measure, \(q \ge 1\) · FKG lattice condition for the wired measure when \(q \ge 1\)

TheoremFKG inequality for the random-cluster measure, \(q \ge 1\)#✓fully proved

FKG inequality for the random-cluster measure (Fortuin, Kasteleyn and Ginibre, 1971): for q ≥ 1 and any boundary wiring C, increasing functions are positively correlated under φ_C. See Grimmett, The Random-Cluster Model (2006), Chapter 3.

theorem bcProb_positively_associated {p q : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hq : 1 ≤ q) {f g : ConfigSpace (Sym2 V) → ℝ} (hf : Monotone f)
    (hg : Monotone g) :
    (∑ ω, bcProb G C p q ω * f ω) * (∑ ω, bcProb G C p q ω * g ω)
      ≤ ∑ ω, bcProb G C p q ω * (f ω * g ω)

Uses 9

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring

Proof usesHolley's condition for probabilities with nested wirings, \(q \ge 1\) · Random-cluster weight with a boundary wiring · Partition function with a boundary wiring · Bernoulli edge product · Number of clusters under a boundary wiring · FKG lattice condition · FKG inequality

TheoremRandom-cluster comparison of boundary conditions for \(q \ge 1\)#✓fully proved

Comparison of boundary conditions for the random-cluster measure: for q ≥ 1 and wirings C ≤ C', φ_C(A) ≤ φ_C'(A) for every increasing event A. This follows from Holley's inequality (Holley, 1974); see Grimmett, The Random-Cluster Model (2006), Chapter 4.

theorem bcProb_mono_bc (C' : SimpleGraph V) [DecidableRel C'.Adj] (hCC' : C ≤ C')
    {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    {A : Set (ConfigSpace (Sym2 V))} (hA : IsIncreasing A) :
    (∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * bcProb G C p q ω)
      ≤ ∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * bcProb G C' p q ω

Uses 9 · Used by 11

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring · Increasing event

Proof usesHolley's condition for probabilities with nested wirings, \(q \ge 1\) · Random-cluster weight with a boundary wiring · Partition function with a boundary wiring · Bernoulli edge product · Number of clusters under a boundary wiring · Holley inequality for increasing events

Used byFree–wired sandwich for boundary graphs inside the boundary clique · Sandwich between the free and all-wired boundary conditions · Boundary wirings lie between free and wired when \(q \ge 1\) · Wirings with the boundary clique dominate the wired measure, \(q \ge 1\) · Wired box measure dominates the induced-wiring measure for \(q \ge 1\) · Domination by the inner wired measure under a coarser induced wiring · Free inner measure is dominated by every induced-wiring measure · Free measure is dominated by induced-wiring measures for \(q \ge 1\) · Per-box uniqueness of the random-cluster measures off a countable set · Free off-centre lower bound by the recentred small-box marginal · Translation invariance of the free \(q = 2\) infinite-volume measure

LemmaFree–wired sandwich for boundary graphs inside the boundary clique#✓fully proved

For q ≥ 1 and C inside the boundary clique, φ^0(A) ≤ φ^C(A) ≤ φ^1(A) for every increasing event A.

lemma bcProb_dlr_sandwich (C : SimpleGraph V) [DecidableRel C.Adj]
    (hC : C ≤ StatMech.Lattice.boundaryCliqueGraph bdry)
    {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    {A : Set (ConfigSpace (Sym2 V))} (hA : IsIncreasing A) :
    (∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * bcProb G (⊥ : SimpleGraph V) p q ω)
        ≤ ∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * bcProb G C p q ω
    ∧ (∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * bcProb G C p q ω)
        ≤ ∑ ω, A.indicator (fun _ => (1 : ℝ)) ω
            * bcProb G (StatMech.Lattice.boundaryCliqueGraph bdry) p q ω

Uses 6

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring · Increasing event · Complete graph on the boundary vertices · Boundary wiring relation

Proof usesRandom-cluster comparison of boundary conditions for \(q \ge 1\)

LemmaSandwich between the free and all-wired boundary conditions#✓fully proved

The free lower bound together with the bound by the boundary condition ⊤ (all vertices wired).

lemma bcProb_dlr_sandwich_top (C : SimpleGraph V) [DecidableRel C.Adj]
    {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    {A : Set (ConfigSpace (Sym2 V))} (hA : IsIncreasing A) :
    (∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * bcProb G (⊥ : SimpleGraph V) p q ω)
        ≤ ∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * bcProb G C p q ω
    ∧ (∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * bcProb G C p q ω)
        ≤ ∑ ω, A.indicator (fun _ => (1 : ℝ)) ω
            * bcProb G (⊤ : SimpleGraph V) p q ω

Uses 4

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring · Increasing event

Proof usesRandom-cluster comparison of boundary conditions for \(q \ge 1\)

DefinitionEdge marginal of a mass function#✓fully proved

The probability μ(ω(e) = 1) that the coordinate e is open under the mass function μ.

noncomputable def edgeMargProb (μ : ConfigSpace E → ℝ) (e : E) : ℝ :=
  ∑ ω : ConfigSpace E, (if ω e then (1 : ℝ) else 0) * μ ω

Uses 1 · Used by 67

Statement usesConfiguration space of a statistical-mechanics model

Used bySet where coupled measures differ is countable under a convex pressure · Coupled measures agree off a countable set, given a convex pressure · Monotonicity in \(p\) of free \(q = 2\) edge marginals on a finite graph · Continuity in \(t\) of free \(q = 2\) edge marginals on a finite graph · Left-continuity of the free \(q = 2\) edge density in \(t\) · Free \(q = 2\) edge density is monotone in \(p\) on \((0, 1)\) · Continuity in \(t\) of wired \(q = 2\) edge marginals on a finite graph · Right-continuity of the wired \(q = 2\) edge density in \(t\) · Derivative marginals of a convex pressure agree off a countable set · Average wired edge density as the mean of edge marginals · Expected wired open-edge count is the sum of edge marginals · Monotone couplings with equal edge marginals agree on up-sets · Off-centre carrier vanishes by translation covariance · Free density is at most each translated wired marginal · Translated wired marginals converge to the wired density · Equal wired densities from equal translated marginals · Countably many parameters admit a separating increasing event · Per-box \(q = 2\) uniqueness off a countable set of tilts · Wired-marginal difference between a box and its translate · Monotone-coupled laws with equal edge marginals agree on up-sets · Per-box uniqueness of the random-cluster measures off a countable set · Free unit-edge marginal at \(0\) on \(\Lambda_{\lfloor\sqrt n\rfloor}\) · Wired unit-edge marginal at \(0\) on \(\Lambda_{\lfloor\sqrt n\rfloor}\) · Toggle-invariant coordinates are open with probability one half · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Two-sided free \(q = 2\) bulk bounds from the free sandwich · Free \(q = 2\) bulk sandwich from equal free edge densities · Two-sided wired \(q = 2\) bulk bounds from the wired sandwich · Wired \(q = 2\) bulk sandwich from equal wired edge densities · Lower bound on free bulk edge marginals · Free off-centre lower bound by the recentred small-box marginal · Free off-centre sandwich from free rotation residues · Free unit-edge marginals converge to the free density · Wired unit-edge marginals converge to the wired density · Free unit-edge marginal in the square-root box · Wired unit-edge marginal in the square-root box · Upper bound on wired bulk edge marginals · Wired off-centre sandwich from wired rotation residues · Wired off-centre upper bound by the recentred small-box marginal · Parametric agreement on increasing events off a countable set · Average wired \(q = 2\) edge density of a box as a mean of marginals · Wired FK edge marginals are at most one · Nonnegativity of wired FK edge marginals · Free \(q = 2\) edge density lies in \((0, 1)\) · Free uniform bulk deviation at \(q = 2\) · Wired \(q = 2\) edge density lies in \((0, 1)\) · Wired uniform bulk deviation at \(q = 2\) · Graph automorphisms preserve free FK edge marginals · Boundary-preserving automorphisms preserve wired FK edge marginals · Box symmetries preserve the free \(q = 2\) density of box edges · Box symmetries preserve the wired \(q = 2\) density of box edges · Translation covariance of FK edge marginals on boxes · Boundary-matching isomorphisms transport FK edge marginals · Free off-centre sandwich hypothesis · Free \(q = 2\) box edge marginals are at most the free density · Wired off-centre sandwich hypothesis · Wired \(q = 2\) box edge marginals are at least the wired density · Translation invariance of free and wired densities if marginals merge · Constant free density gives an upper bound on expected open edges · Equal free densities from merging free marginals · Translation invariance of the free density given merging marginals · Constant wired density gives a lower bound on expected open edges · Equal wired densities from merging wired marginals · Translation invariance of the wired density given merging marginals · Free box integral of an edge indicator is the free edge marginal · Wired box integral of an edge indicator is the wired edge marginal

DefinitionMass of an event under a mass function#✓fully proved

The mass μ(A) of an event under the mass function μ.

noncomputable def eventMassProb (μ : ConfigSpace E → ℝ) (A : Set (ConfigSpace E)) : ℝ :=
  ∑ ω : ConfigSpace E, A.indicator (fun _ => (1 : ℝ)) ω * μ ω

Uses 1 · Used by 10

Statement usesConfiguration space of a statistical-mechanics model

Used bySet where coupled measures differ is countable under a convex pressure · Coupled measures agree off a countable set, given a convex pressure · Monotone couplings with equal edge marginals agree on up-sets · Countably many parameters admit a separating increasing event · Per-box \(q = 2\) uniqueness off a countable set of tilts · Monotone-coupled laws with equal edge marginals agree on up-sets · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Parametric agreement on increasing events off a countable set

StructureMonotone coupling of two mass functions#✓fully proved

P is a monotone coupling of the mass functions μ and ν: a nonnegative mass function on pairs with marginals μ and ν, supported on pairs (ω, ω') with ω ≤ ω'.

structure IsMonotoneCouplingFun (P : ConfigSpace E × ConfigSpace E → ℝ)
    (μ ν : ConfigSpace E → ℝ) : Prop where
  nonneg : ∀ z, 0 ≤ P z
  supportLE : ∀ z, ¬ z.1 ≤ z.2 → P z = 0
  fst_marginal : ∀ ω, ∑ ω' : ConfigSpace E, P (ω, ω') = μ ω
  snd_marginal : ∀ ω', ∑ ω : ConfigSpace E, P (ω, ω') = ν ω'

Uses 1 · Used by 9

Statement usesConfiguration space of a statistical-mechanics model

Used bySet where coupled measures differ is countable under a convex pressure · Coupled measures agree off a countable set, given a convex pressure · Monotone couplings with equal edge marginals agree on up-sets · Countably many parameters admit a separating increasing event · Monotone-coupled laws with equal edge marginals agree on up-sets · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Parametric agreement on increasing events off a countable set

LemmaMonotone couplings with equal edge marginals agree on up-sets#✓fully proved

Two monotonically coupled measures with the same edge marginals give the same mass to every increasing event.

lemma eventMass_eq_of_edgeMarg_eq {P : ConfigSpace E × ConfigSpace E → ℝ}
    {μ ν : ConfigSpace E → ℝ} (hP : IsMonotoneCouplingFun P μ ν)
    (hmarg : ∀ e : E, edgeMargProb μ e = edgeMargProb ν e)
    {A : Set (ConfigSpace E)} (hA : IsIncreasing A) :
    eventMassProb μ A = eventMassProb ν A

Uses 6 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Monotone coupling of two mass functions · Edge marginal of a mass function · Mass of an event under a mass function · Increasing event

Proof usesIndicator of an increasing event is monotone

Used byMonotone-coupled laws with equal edge marginals agree on up-sets

DefinitionEvent mass under the random-cluster measure with a boundary graph#✓fully proved

The mass φ^C_{G,p,q}(A) of an event under the random-cluster measure with boundary graph C.

noncomputable def bcEventMass (C : SimpleGraph V) [DecidableRel C.Adj] (p q : ℝ)
    (A : Set (ConfigSpace (Sym2 V))) : ℝ :=
  ∑ ω : ConfigSpace (Sym2 V), A.indicator (fun _ => (1 : ℝ)) ω * bcProb G C p q ω

Uses 2 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring

Used byBoundary-graph comparison \(\varphi^{C'}(A) \le q^N \varphi^C(A)\)

LemmaBoundary-graph comparison \(\varphi^{C'}(A) \le q^N \varphi^C(A)\)#✓fully proved

If the cluster counts with boundary graphs C ≤ C' differ by at most N, then φ^C(A) ≤ q^N φ^{C'}(A) for nonnegative event indicators.

lemma bcEventMass_le_qpow (C C' : SimpleGraph V) [DecidableRel C.Adj]
    [DecidableRel C'.Adj] (hCC' : C ≤ C') {p q : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hq : 1 ≤ q) (N : ℕ) (hb : ∀ ω, numClustersBC G C ω ≤ numClustersBC G C' ω + N)
    {A : Set (ConfigSpace (Sym2 V))} (hA0 : ∀ ω, 0 ≤ A.indicator (fun _ => (1 : ℝ)) ω) :
    bcEventMass G C' p q A ≤ q ^ N * bcEventMass G C p q A

Uses 8

Statement usesConfiguration space of a statistical-mechanics model · Event mass under the random-cluster measure with a boundary graph · Number of clusters under a boundary wiring

Proof usesRandom-cluster probability with a boundary wiring · Random-cluster weight with a boundary wiring · Partition function with a boundary wiring · Bernoulli edge product · Open subgraph of an edge configuration

LemmaBoundary-supported wirings lie below the boundary clique#✓fully proved

A wiring whose edges join boundary vertices lies below the boundary clique.

lemma bc_le_boundaryClique (C : SimpleGraph V)
    (hC : ∀ x y, C.Adj x y → bdry x ∧ bdry y) :
    C ≤ StatMech.Lattice.boundaryCliqueGraph bdry

Uses 2 · Used by 1

Statement usesComplete graph on the boundary vertices

Proof usesBoundary wiring relation

Used byBoundary wirings lie between free and wired when \(q \ge 1\)

LemmaEmpty wiring gives the free random-cluster measure#✓fully proved

The empty wiring gives the free random-cluster measure.

lemma bcProb_bot_eq_fkProb (p q : ℝ) (ω : ConfigSpace (Sym2 V)) :
    bcProb G (⊥ : SimpleGraph V) p q ω = fkProb G p q ω

Uses 11 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring · Probability of an ambient FK configuration

Proof usesRandom-cluster weight with a boundary wiring · Partition function with a boundary wiring · Bernoulli edge product · Unnormalized random-cluster weight · Ambient FK normalizer · Number of open clusters · Number of clusters under a boundary wiring · Open subgraph of an edge configuration

Used byBoundary wirings lie between free and wired when \(q \ge 1\) · Free inner measure is dominated by every induced-wiring measure · Per-box uniqueness of the random-cluster measures off a countable set · Free off-centre lower bound by the recentred small-box marginal · Translation invariance of the free \(q = 2\) infinite-volume measure

LemmaBoundary clique gives the wired random-cluster measure#✓fully proved

The boundary clique gives the wired random-cluster measure.

lemma bcProb_clique_eq_wiredFkProb (p q : ℝ) (ω : ConfigSpace (Sym2 V)) :
    bcProb G (StatMech.Lattice.boundaryCliqueGraph bdry) p q ω
      = wiredFkProb G bdry p q ω

Uses 15 · Used by 16

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring · Wired random-cluster probability of a configuration · Complete graph on the boundary vertices · Boundary wiring relation

Proof usesRandom-cluster weight with a boundary wiring · Partition function with a boundary wiring · Bernoulli edge product · Number of clusters under a boundary wiring · Open subgraph of an edge configuration · Wired random-cluster weight · Wired random-cluster partition function · Number of open clusters with wired boundary conditions · Open subgraph of a bond configuration · Wired open graph

Used byFK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Wired \(q = 2\) edge density is monotone in \(t\) · Wired box-boundary connection probability is monotone in \(p\) at \(q = 2\) · Boundary wirings lie between free and wired when \(q \ge 1\) · Wirings with the boundary clique dominate the wired measure, \(q \ge 1\) · Wired box measure dominates the induced-wiring measure for \(q \ge 1\) · Domination by the inner wired measure under a coarser induced wiring · Inner wired domination for vertex sets of \(\mathbb{Z}^d\) · FKG lattice condition for the wired measure when \(q \ge 1\) · Secant bound gives free–wired density agreement off a countable set · Wired \(\Lambda_{n+1}\) measure of a \(\Lambda_n\) cylinder event as a sum · Secant bound gives \(q = 2\) edge-event uniqueness off a countable set · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Ergodicity of the wired random-cluster measure

LemmaBoundary wirings lie between free and wired when \(q \ge 1\)#✓fully proved

For q ≥ 1 and a wiring C supported on the boundary, free ≤ φ_C ≤ wired on every increasing event.

lemma fkProb_le_bcProb_le_wiredFkProb (C : SimpleGraph V) [DecidableRel C.Adj]
    (hC : ∀ x y, C.Adj x y → bdry x ∧ bdry y)
    {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    {A : Set (ConfigSpace (Sym2 V))} (hA : IsIncreasing A) :
    (∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * fkProb G p q ω)
        ≤ (∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * bcProb G C p q ω)
      ∧ (∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * bcProb G C p q ω)
        ≤ ∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * wiredFkProb G bdry p q ω

Uses 11

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring · Probability of an ambient FK configuration · Wired random-cluster probability of a configuration · Increasing event

Proof usesEmpty wiring gives the free random-cluster measure · Boundary clique gives the wired random-cluster measure · Random-cluster comparison of boundary conditions for \(q \ge 1\) · Boundary-supported wirings lie below the boundary clique · Complete graph on the boundary vertices · Boundary wiring relation

LemmaBoundary-graph FK measure increases in \(p\) for \(q \ge 1\)#✓fully proved

For q ≥ 1, the random-cluster measure with boundary graph C is increasing in p on increasing events.

lemma bcProb_monotone_in_p {p1 p2 q : ℝ} (hp1 : 0 < p1) (hp1' : p1 < 1)
    (hp2 : 0 < p2) (hp2' : p2 < 1) (hle : p1 ≤ p2) (hq : 1 ≤ q)
    {A : Set (ConfigSpace (Sym2 V))} (hA : IsIncreasing A) :
    (∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * bcProb G C p1 q ω)
      ≤ ∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * bcProb G C p2 q ω

Uses 9 · Used by 7

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring · Increasing event

Proof usesRandom-cluster weight with a boundary wiring · Partition function with a boundary wiring · Bernoulli edge product · Mixed supermodularity of cluster counts for nested wirings · Number of clusters under a boundary wiring · Holley inequality for increasing events

Used byFK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Wired \(q = 2\) edge density is monotone in \(t\) · Wired box-boundary connection probability is monotone in \(p\) at \(q = 2\) · Secant bound gives free–wired density agreement off a countable set · Secant bound gives \(q = 2\) edge-event uniqueness off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\)

DefinitionPartition function of a conditioning fibre#✓fully proved

The partition function of the fibre of ψ off F: the sum of bcWeight over configurations agreeing with ψ off F.

noncomputable def inducedBcZ (p q : ℝ) (F : Finset (Sym2 V)) (ψ : ConfigSpace (Sym2 V)) : ℝ :=
  ∑ ρ ∈ condFibre F ψ, bcWeight G C p q ρ

Uses 3 · Used by 15

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster weight with a boundary wiring · Fibre of configurations agreeing off an edge set

Used byDisintegration of a boundary-wired measure over conditioning fibres · Conditional random-cluster measure with a boundary wiring · Holley's condition for nested-wiring conditional measures, \(q \ge 1\) · Conditional measures increase with the wiring for \(q \ge 1\) · Domain Markov property for the wired measure on nested boxes · Law of total probability over outside configurations · Conditional outer measure is the induced-wiring FK measure · Conditional outer probability as an induced-wiring probability · Factorization of the conditioned outer partition function · Closed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Domain Markov property for the wired box measure · Configurations agreeing off \(F\) have equal conditional probabilities · Conditional wired decrease on inner increasing events for \(q \ge 1\) · Wired \(\Lambda_{n+1}\) measure decomposed over outer configurations · Ergodicity of the wired random-cluster measure

DefinitionConditional random-cluster measure with a boundary wiring#✓fully proved

The random-cluster measure with wiring C conditioned on agreeing with ψ off the edge set F.

noncomputable def condBcProb (p q : ℝ) (F : Finset (Sym2 V)) (ψ ω : ConfigSpace (Sym2 V)) : ℝ :=
  if AgreesOff F ψ ω then bcWeight G C p q ω / inducedBcZ G C p q F ψ else 0

Uses 4 · Used by 24

Statement usesConfiguration space of a statistical-mechanics model · Agreement of configurations off an edge set · Random-cluster weight with a boundary wiring · Partition function of a conditioning fibre

Used byDisintegration of a boundary-wired measure over conditioning fibres · Holley's condition for nested-wiring conditional measures, \(q \ge 1\) · Conditional measures increase with the wiring for \(q \ge 1\) · Wired measure conditionally dominated by larger wirings, \(q \ge 1\) · Domain Markov property for the wired measure on nested boxes · Law of total probability over outside configurations · Conditional outer wired probability at most the inner wired one, \(q \ge 1\) · Conditional outer measure is the induced-wiring FK measure · Conditional outer probability as an induced-wiring probability · Free inner measure is dominated by the conditional outer measure · Inner wired domination of the restricted outer wired measure · Closed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Domain Markov property for the wired box measure · Configurations agreeing off \(F\) have equal conditional probabilities · Conditional wired decrease on inner increasing events for \(q \ge 1\) · Wired \(\Lambda_{n+1}\) measure decomposed over outer configurations · Wired box measures decrease on inner increasing events for \(q \ge 1\) · Per-box uniqueness of the random-cluster measures off a countable set · Free off-centre lower bound by the recentred small-box marginal · Translation invariance of the free \(q = 2\) infinite-volume measure · Ergodicity of the wired random-cluster measure · Disjoint-box cap hypothesis for multi-open events · Conditional product cap for multi-open events in boxes

LemmaHolley's condition for nested-wiring conditional measures, \(q \ge 1\)#✓fully proved

Holley's condition for the conditional measures with nested wirings C ≤ C' and q ≥ 1.

lemma condBcProb_cross (C' : SimpleGraph V) [DecidableRel C'.Adj] (hCC' : C ≤ C')
    {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    (F : Finset (Sym2 V)) (ψ a b : ConfigSpace (Sym2 V)) :
    condBcProb G C p q F ψ a * condBcProb G C' p q F ψ b
      ≤ condBcProb G C p q F ψ (a ⊓ b) * condBcProb G C' p q F ψ (a ⊔ b)

Uses 9 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Conditional random-cluster measure with a boundary wiring

Proof usesAgreement of configurations off an edge set · Random-cluster weight with a boundary wiring · Holley's condition for weights with nested wirings, \(q \ge 1\) · Fibre of configurations agreeing off an edge set · Bernoulli edge product · Partition function of a conditioning fibre · Number of clusters under a boundary wiring

Used byConditional measures increase with the wiring for \(q \ge 1\)

LemmaConditional measures increase with the wiring for \(q \ge 1\)#✓fully proved

For q ≥ 1 and C ≤ C', the conditional measure with wiring C is dominated by the one with wiring C' on increasing events.

lemma condBcProb_mono_bc (C' : SimpleGraph V) [DecidableRel C'.Adj] (hCC' : C ≤ C')
    {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    (F : Finset (Sym2 V)) (ψ : ConfigSpace (Sym2 V))
    {A : Set (ConfigSpace (Sym2 V))} (hA : IsIncreasing A) :
    (∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * condBcProb G C p q F ψ ω)
      ≤ ∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * condBcProb G C' p q F ψ ω

Uses 11 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Conditional random-cluster measure with a boundary wiring · Increasing event

Proof usesAgreement of configurations off an edge set · Random-cluster weight with a boundary wiring · Holley's condition for nested-wiring conditional measures, \(q \ge 1\) · Fibre of configurations agreeing off an edge set · Bernoulli edge product · Partition function of a conditioning fibre · Number of clusters under a boundary wiring · Holley inequality for increasing events

Used byWired measure conditionally dominated by larger wirings, \(q \ge 1\) · Ergodicity of the wired random-cluster measure

LemmaDisintegration of a boundary-wired measure over conditioning fibres#✓fully proved

Disintegration: φ_C(ω) is the mass of the fibre of ω times the conditional probability of ω in that fibre.

lemma bcProb_eq_fibreMass_mul_condBcProb {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (F : Finset (Sym2 V)) (ω : ConfigSpace (Sym2 V)) :
    bcProb G C p q ω
      = (∑ ρ ∈ condFibre F ω, bcProb G C p q ρ) * condBcProb G C p q F ω ω

Uses 10 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring · Conditional random-cluster measure with a boundary wiring · Fibre of configurations agreeing off an edge set

Proof usesAgreement of configurations off an edge set · Random-cluster weight with a boundary wiring · Partition function with a boundary wiring · Bernoulli edge product · Partition function of a conditioning fibre · Number of clusters under a boundary wiring

Used byLaw of total probability over outside configurations · Wired \(\Lambda_{n+1}\) measure decomposed over outer configurations · Ergodicity of the wired random-cluster measure

LemmaWirings with the boundary clique dominate the wired measure, \(q \ge 1\)#✓fully proved

For q ≥ 1 the wired measure is dominated by φ_C' for any wiring C' containing the boundary clique.

lemma wiredFkProb_inner_dominated (C' : SimpleGraph V) [DecidableRel C'.Adj]
    (hCC' : StatMech.Lattice.boundaryCliqueGraph bdry ≤ C')
    {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    {A : Set (ConfigSpace (Sym2 V))} (hA : IsIncreasing A) :
    (∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * wiredFkProb G bdry p q ω)
      ≤ ∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * bcProb G C' p q ω

Uses 8

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring · Wired random-cluster probability of a configuration · Increasing event · Complete graph on the boundary vertices

Proof usesBoundary clique gives the wired random-cluster measure · Random-cluster comparison of boundary conditions for \(q \ge 1\) · Boundary wiring relation

LemmaWired measure conditionally dominated by larger wirings, \(q \ge 1\)#✓fully proved

Conditional version of wiredFkProb_inner_dominated.

lemma wiredFkProb_inner_dominated_cond (C' : SimpleGraph V) [DecidableRel C'.Adj]
    (hCC' : StatMech.Lattice.boundaryCliqueGraph bdry ≤ C')
    {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    (F : Finset (Sym2 V)) (ψ : ConfigSpace (Sym2 V))
    {A : Set (ConfigSpace (Sym2 V))} (hA : IsIncreasing A) :
    (∑ ω, A.indicator (fun _ => (1 : ℝ)) ω
        * condBcProb G (StatMech.Lattice.boundaryCliqueGraph bdry) p q F ψ ω)
      ≤ ∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * condBcProb G C' p q F ψ ω

Uses 6 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Conditional random-cluster measure with a boundary wiring · Increasing event · Complete graph on the boundary vertices · Boundary wiring relation

Proof usesConditional measures increase with the wiring for \(q \ge 1\)

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

51 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.