Convexity of the free energy and edge densities

DefinitionSurface count of a box#✓fully proved

The surface count 2d (2n + 1)^{d - 1} of the box Λ_n.

noncomputable def boxSecantSurface (d n : ℕ) : ℝ := (2 * d) * (2 * n + 1) ^ (d - 1)

DefinitionEdge-volume count of a box#✓fully proved

The edge-volume count d (2n + 1)^d of the box Λ_n.

noncomputable def boxSecantVolume (d n : ℕ) : ℝ := (d : ℝ) * (2 * n + 1) ^ d

LemmaAdding edges within a vertex set drops components by at most its size#✓fully proved

Adding edges with both endpoints in {v | p v} lowers the number of connected components by at most |{v | p v}|. See also card_connectedComponent_le_sup_fromEdgeSet (EdgeMarginal) for the bound by the number of added edges.

lemma connectedComponent_card_le_add_of_sup {V : Type*} [Fintype V]
    {G K : SimpleGraph V} {p : V → Prop} (hK : ∀ {x y}, K.Adj x y → p x ∧ p y) :
    Nat.card G.ConnectedComponent
      ≤ Nat.card (G ⊔ K).ConnectedComponent + Nat.card {v // p v}

Used by 1

Used byWired and free FK weights within a factor \(q^{|\partial|}\), \(q \ge 1\)

DefinitionRight derivative of the pressure#✓fully proved

The right derivative g'₊(x) = derivWithin g (Ioi x) x, the form used by Mathlib's ConvexOn.monotoneOn_rightDeriv.

noncomputable def pressureRightDeriv (g : ℝ → ℝ) (x : ℝ) : ℝ := derivWithin g (Ioi x) x

Used by 18

Used byPointwise limits of convex maps are convex with one-sided derivatives · Convex function has equal one-sided derivatives off a countable set · Set where coupled measures differ is countable under a convex pressure · Wired edge densities on a box as right derivatives · Wired edge densities on a box bounded by right derivatives · Coupled measures agree off a countable set, given a convex pressure · Infinite-volume edge densities as one-sided derivatives · Convex free-energy hypothesis for a box edge at \(q = 2\) · Softplus is convex with both one-sided derivatives logistic · Convex free energy gives wired density at \(p'\) at most free at \(p > p'\) · Derivative marginals of a convex pressure agree off a countable set · Left derivative of a convex function is at most the right one · Per-box \(q = 2\) uniqueness off a countable set of tilts · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Wired densities of genuine box edges as right derivatives · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Homogeneous free-energy data on a box at \(q = 2\)

DefinitionLeft derivative of the pressure#✓fully proved

The left derivative g'₋(x) = derivWithin g (Iio x) x.

noncomputable def pressureLeftDeriv (g : ℝ → ℝ) (x : ℝ) : ℝ := derivWithin g (Iio x) x

Used by 15

Used byPointwise limits of convex maps are convex with one-sided derivatives · Convex function has equal one-sided derivatives off a countable set · Free edge densities on a box as left derivatives · Infinite-volume edge densities as one-sided derivatives · Convex free-energy hypothesis for a box edge at \(q = 2\) · Softplus is convex with both one-sided derivatives logistic · Convex free energy gives wired density at \(p'\) at most free at \(p > p'\) · Derivative marginals of a convex pressure agree off a countable set · Left derivative of a convex function is at most the right one · Per-box \(q = 2\) uniqueness off a countable set of tilts · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free densities of genuine box edges as left derivatives · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Homogeneous free-energy data on a box at \(q = 2\)

LemmaLeft derivative of a convex function is at most the right one#✓fully proved

g'₋(x) ≤ g'₊(x); Mathlib's ConvexOn.leftDeriv_le_rightDeriv_of_mem_interior on univ.

lemma pressureLeftDeriv_le_rightDeriv (hg : ConvexOn ℝ univ g) (x : ℝ) :
    pressureLeftDeriv g x ≤ pressureRightDeriv g x

Uses 2 · Used by 4

Statement usesLeft derivative of the pressure · Right derivative of the pressure

Used byPointwise limits of convex maps are convex with one-sided derivatives · Convex function has equal one-sided derivatives 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\)

LemmaConvex function has equal one-sided derivatives off a countable set#✓fully proved

A convex function on ℝ has equal left and right derivatives off a countable set.

lemma countable_leftDeriv_ne_rightDeriv (hg : ConvexOn ℝ univ g) :
    {x : ℝ | pressureLeftDeriv g x ≠ pressureRightDeriv g x}.Countable

Uses 3 · Used by 3

Statement usesLeft derivative of the pressure · Right derivative of the pressure

Proof usesLeft derivative of a convex function is at most the right one

Used byPointwise limits of convex maps are convex with one-sided derivatives · Derivative marginals of a convex pressure agree off a countable set · Per-box uniqueness of the random-cluster measures off a countable set

LemmaDerivative marginals of a convex pressure agree off a countable set#✓fully proved

If two families of edge marginals are the left and right derivatives of a convex g, they differ only on a countable set of parameters.

lemma pressure_convex_countable_density_ne
    (g : ℝ → ℝ) (hg : ConvexOn ℝ univ g)
    (μ ν : ℝ → ConfigSpace E → ℝ) (e : E)
    (ha_eq : ∀ p, edgeMargProb (μ p) e = pressureLeftDeriv g p)
    (hb_eq : ∀ p, edgeMargProb (ν p) e = pressureRightDeriv g p) :
    {p : ℝ | edgeMargProb (μ p) e ≠ edgeMargProb (ν p) e}.Countable

Uses 5

Statement usesConfiguration space of a statistical-mechanics model · Edge marginal of a mass function · Left derivative of the pressure · Right derivative of the pressure

Proof usesConvex function has equal one-sided derivatives off a countable set

LemmaCoupled measures agree off a countable set, given a convex pressure#✓fully proved

If μ p and ν p are monotonically coupled, the edge density of ν p at e is the right derivative of a convex g, and all edge marginals agree wherever that density is continuous in p, then μ p and ν p agree on every increasing event for p off a countable set.

lemma fk_uniqueness_of_pressure_convex
    (g : ℝ → ℝ) (hg : ConvexOn ℝ univ g)
    (μ ν : ℝ → ConfigSpace E → ℝ) (e : E)
    (P : ℝ → ConfigSpace E × ConfigSpace E → ℝ)
    (hcoup : ∀ p, IsMonotoneCouplingFun (P p) (μ p) (ν p))
    (hb_eq : ∀ p, edgeMargProb (ν p) e = pressureRightDeriv g p)
    (heq_at_cont : ∀ p : ℝ, ContinuousAt (fun p => edgeMargProb (ν p) e) p →
      ∀ e' : E, edgeMargProb (μ p) e' = edgeMargProb (ν p) e') :
    ∃ S : Set ℝ, S.Countable ∧
      ∀ p ∉ S, ∀ {A : Set (ConfigSpace E)}, IsIncreasing A →
        eventMassProb (μ p) A = eventMassProb (ν p) A

Uses 7

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 · Right derivative of the pressure · Increasing event

Proof usesParametric agreement on increasing events off a countable set

LemmaSet where coupled measures differ is countable under a convex pressure#✓fully proved

The set of parameters at which μ p and ν p differ on some increasing event is countable, under the hypotheses of fk_uniqueness_of_pressure_convex.

lemma countable_phi_ne_of_pressure_convex
    (g : ℝ → ℝ) (hg : ConvexOn ℝ univ g)
    (μ ν : ℝ → ConfigSpace E → ℝ) (e : E)
    (P : ℝ → ConfigSpace E × ConfigSpace E → ℝ)
    (hcoup : ∀ p, IsMonotoneCouplingFun (P p) (μ p) (ν p))
    (hb_eq : ∀ p, edgeMargProb (ν p) e = pressureRightDeriv g p)
    (heq_at_cont : ∀ p : ℝ, ContinuousAt (fun p => edgeMargProb (ν p) e) p →
      ∀ e' : E, edgeMargProb (μ p) e' = edgeMargProb (ν p) e') :
    {p : ℝ | ∃ A : Set (ConfigSpace E), IsIncreasing A ∧
        eventMassProb (μ p) A ≠ eventMassProb (ν p) A}.Countable

Uses 7

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 · Right derivative of the pressure · Increasing event

Proof usesCountably many parameters admit a separating increasing event

DefinitionLogistic function \(e^t/(1+e^t)\)#✓fully proved

The logistic map t ↦ eᵗ / (1 + eᵗ), equal to Mathlib's Real.sigmoid (fsc_logistic_eq_sigmoid).

noncomputable def fsc_logistic (t : ℝ) : ℝ := Real.exp t / (1 + Real.exp t)

Used by 93

Used byFree edge densities on a box as left derivatives · Wired edge densities on a box as right derivatives · Wired edge densities on a box bounded by right derivatives · Average edge density of the \(q = 2\) random-cluster measure · Collapse of average edge densities to the free density · Infinite-volume edge densities as one-sided derivatives · Convex free-energy hypothesis for a box edge at \(q = 2\) · Softplus is convex with both one-sided derivatives logistic · Logistic function equals the sigmoid · Convex free energy gives wired density at \(p'\) at most free at \(p > p'\) · Ambient tilted log normalizer of a finite graph · Convexity of the ambient tilted log normalizer · 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 \(t\) · Continuity of the logistic map · Continuity in \(t\) of wired \(q = 2\) edge marginals on a finite graph · Wired \(q = 2\) edge density is monotone in \(t\) · Right-continuity of the wired \(q = 2\) edge density in \(t\) · Free-wired log-normalizer gap \(\le |\partial|\log q/|E|\) for \(q \ge 1\) · Average wired edge density · Average wired density collapse at \(q = 2\) · Average wired edge density as the mean of edge marginals · Wired per-edge ambient tilted log normalizer · Wired tilted log normalizer as a cumulant generating function · Wired tilted log normalizer has derivative the mean open fraction · Tilted mean of open edges equals the wired FK expectation · Wired partition function at logistic \(p\) as a tilted sum · Additive doubling bound along the scales \(K_j\) · Negative log ambient normalizer of a box · Negative log ambient normalizer of the box \(\Lambda_n\) · Doubling bound at the dyadic scales \(2^j\) · Doubling-bound property of the box free energy along \(K_j\) · Box free-energy doubling bound along \(K_j\) holds for \(d, q \ge 1\) · Doubling bound for the box free energy when \(q \ge 1\) · Van Hove subadditivity of the box free energy for \(q \ge 1\) · Per-edge free energy converges along \(K_j\) for \(d, q \ge 1\) · Edge-normalized box free energy of the random-cluster model · Limit of the van Hove upper bound for a fixed box side · Van Hove limit · Uniform upper bound on the box free energy for \(d, n, q \ge 1\) · Box free energy \(-\log Z^E\) of the random-cluster model · Additive doubling bound for \(-\log Z\) of the free \(q = 2\) FK model · Doubling inequality for \(-\log Z\) of the free \(q = 2\) FK model · Additive doubling bound for the edge partition function · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Van Hove tiling bound for the edge partition function · Per-box \(q = 2\) uniqueness off a countable set of tilts · Upper envelope for the per-edge free energy · Per-edge free energy of boxes converges for \(d \ge 1\) · Negative log edge partition function of a box · Average edge density of a random-cluster measure · Convex limit of centered tilt free energies of boxes for \(d, q \ge 1\) · Per-box uniqueness of the random-cluster measures off a countable set · Total deviation of free unit-edge marginals from a free density · Free infinite-volume mass function on a box for \(q \ge 1\) · Free unit-edge marginal at \(0\) on \(\Lambda_{\lfloor\sqrt n\rfloor}\) · Wired unit-edge marginal at \(0\) on \(\Lambda_{\lfloor\sqrt n\rfloor}\) · Total deviation of wired unit-edge marginals from a wired density · Wired infinite-volume mass function on a box for \(q \ge 1\) · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free average edge density collapse on boxes · Free densities of genuine box edges as left derivatives · Wired average edge density collapse on boxes · Wired densities of genuine box edges as right derivatives · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Free \(q = 2\) infinite-volume mass function on a box · Homogeneous free-energy data on a box at \(q = 2\) · Wired \(q = 2\) infinite-volume mass function on a box · 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 · Total deviation of free unit-edge marginals from the density · Free off-centre sandwich from free rotation residues · Free rotation residue for a box pair · 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 · Total deviation of wired unit-edge marginals from the density · Wired off-centre sandwich from wired rotation residues · Wired rotation residue for a box pair · All box edges have the same free \(q = 2\) density · All box edges have the same wired \(q = 2\) density · Average wired \(q = 2\) edge density of a box as a mean of marginals · Free \(q = 2\) edge density lies in \((0, 1)\) · Free growing-box collapse at \(q = 2\) · Free uniform bulk deviation at \(q = 2\) · Wired \(q = 2\) edge density lies in \((0, 1)\) · Wired uniform bulk deviation at \(q = 2\) · Free off-centre sandwich hypothesis · Wired off-centre sandwich hypothesis

DefinitionLogit function \(\log(p/(1-p))\)#✓fully proved

The logit p ↦ log (p / (1 - p)), inverse to fsc_logistic on (0, 1).

noncomputable def fsc_logit (p : ℝ) : ℝ := Real.log (p / (1 - p))

Used by 1

Used byConvex free energy gives wired density at \(p'\) at most free at \(p > p'\)

LemmaLogistic function equals the sigmoid#✓fully proved

The logistic map is Mathlib's Real.sigmoid.

lemma fsc_logistic_eq_sigmoid : fsc_logistic = Real.sigmoid

Uses 1

Statement usesLogistic function \(e^t/(1+e^t)\)

DefinitionConvex free-energy hypothesis for a box edge at \(q = 2\)#✓fully proved

The convex free-energy hypothesis for the box edge eb at q = 2: some convex g has right derivative t ↦ θ^w(fsc_logistic t) and left derivative t ↦ θ^f(fsc_logistic t), the wired and free infinite-volume densities of the edge.

def fsc_FreeEnergyData (d N : ℕ) (eb : Sym2 (boxVerts d N)) : Prop :=
  ∃ g : ℝ → ℝ, ConvexOn ℝ univ g
    ∧ (∀ t, wiredEdgeDensity d 2 (edgeIncl d N eb) (fsc_logistic t) = pressureRightDeriv g t)
    ∧ (∀ t, freeEdgeDensity d 2 (edgeIncl d N eb) (fsc_logistic t) = pressureLeftDeriv g t)

Uses 7 · Used by 2

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Free infinite-volume edge density · Logistic function \(e^t/(1+e^t)\) · Left derivative of the pressure · Right derivative of the pressure · Wired infinite-volume edge density

Used byEdge-marginal uniqueness off a countable set from convex free energy · Convex free energy gives wired density at \(p'\) at most free at \(p > p'\)

LemmaConvex free energy gives wired density at \(p'\) at most free at \(p > p'\)#✓fully proved

Under fsc_FreeEnergyData, the wired edge density at p' is at most the free edge density at p whenever p' < p.

lemma fsc_secant (d N : ℕ) (eb : Sym2 (boxVerts d N))
    (hdata : fsc_FreeEnergyData d N eb) :
    ∀ 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

Uses 9 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Free infinite-volume edge density · Convex free-energy hypothesis for a box edge at \(q = 2\) · Wired infinite-volume edge density

Proof usesLogistic function \(e^t/(1+e^t)\) · Logit function \(\log(p/(1-p))\) · Left derivative of the pressure · Right derivative of the pressure

Used byEdge-marginal uniqueness off a countable set from convex free energy

DefinitionSoftplus function \(\log(1+e^t)\)#✓fully proved

The softplus function t ↦ log (1 + eᵗ).

noncomputable def fsc_softplus (t : ℝ) : ℝ := Real.log (1 + Real.exp t)

Used by 1

Used bySoftplus is convex with both one-sided derivatives logistic

LemmaSoftplus is convex with both one-sided derivatives logistic#✓fully proved

Softplus is a convex function whose one-sided derivatives are both fsc_logistic, so the derivative conditions in fsc_FreeEnergyData can hold for some convex function.

lemma fsc_freeEnergyData_satisfiable :
    ∃ g : ℝ → ℝ, ConvexOn ℝ univ g
      ∧ (∀ t, fsc_logistic t = pressureRightDeriv g t)
      ∧ (∀ t, fsc_logistic t = pressureLeftDeriv g t)

Uses 4

Statement usesLogistic function \(e^t/(1+e^t)\) · Left derivative of the pressure · Right derivative of the pressure

Proof usesSoftplus function \(\log(1+e^t)\)

LemmaEdge-marginal uniqueness off a countable set from convex free energy#✓fully proved

Under fsc_FreeEnergyData, at q = 2 there is a countable set S of parameters off which every measure φ whose box-edge marginal lies between the free and wired ones has the same marginal as both.

StatMech.FK.fk_uniqueness_q2_secant_from_freeEnergyData · 17 lines

lemma fk_uniqueness_q2_secant_from_freeEnergyData (d N : ℕ) (eb : Sym2 (boxVerts d N))
    (hdata : fsc_FreeEnergyData d N eb) :
    ∃ S : Set ℝ, S.Countable ∧
      ∀ p ∉ S, ∀ (hp : 0 < p) (hp1 : p < 1)
        (phi : Measure (ConfigSpace (Sym2 (Site d)))),
        ((freeInfiniteVolume d hp hp1 (by norm_num : (0:ℝ) < 2) : Measure _).real
            (boxRestrict d N ⁻¹' (boxEdgeOpenEvent d N eb)) ≤ phi.real
              (boxRestrict d N ⁻¹' (boxEdgeOpenEvent d N eb))
          ∧ phi.real (boxRestrict d N ⁻¹' (boxEdgeOpenEvent d N eb))
              ≤ (wiredInfiniteVolume d hp hp1 (by norm_num : (0:ℝ) < 2) : Measure _).real
                  (boxRestrict d N ⁻¹' (boxEdgeOpenEvent d N eb))) →
        phi.real (boxRestrict d N ⁻¹' (boxEdgeOpenEvent d N eb))
            = (freeInfiniteVolume d hp hp1 (by norm_num : (0:ℝ) < 2) : Measure _).real
                (boxRestrict d N ⁻¹' (boxEdgeOpenEvent d N eb))
          ∧ phi.real (boxRestrict d N ⁻¹' (boxEdgeOpenEvent d N eb))
              = (wiredInfiniteVolume d hp hp1 (by norm_num : (0:ℝ) < 2) : Measure _).real
                  (boxRestrict d N ⁻¹' (boxEdgeOpenEvent d N eb))

Uses 10

Statement 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 · Vertices of the box \((-n, n)^d\) · Free infinite-volume random-cluster measure · Convex free-energy hypothesis for a box edge at \(q = 2\) · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice

Proof usesSecant bound gives \(q = 2\) edge-event uniqueness off a countable set · Convex free energy gives wired density at \(p'\) at most free at \(p > p'\)

DefinitionFree edge densities on a box as left derivatives#✓fully proved

The free q = 2 density of every edge of Λ_N at p = logistic(t) is the left derivative of g at t.

def fdd_FreeDensityIsLeftDeriv (N : ℕ) (g : ℝ → ℝ) : Prop :=
  ∀ (e' : Sym2 (boxVerts d N)) (t : ℝ),
    freeEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t) = pressureLeftDeriv g t

Uses 5

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Free infinite-volume edge density · Logistic function \(e^t/(1+e^t)\) · Left derivative of the pressure

DefinitionWired edge densities on a box as right derivatives#✓fully proved

The wired q = 2 density of every edge of Λ_N at p = logistic(t) is the right derivative of g at t.

def fdd_WiredDensityIsRightDeriv (N : ℕ) (g : ℝ → ℝ) : Prop :=
  ∀ (e' : Sym2 (boxVerts d N)) (t : ℝ),
    wiredEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t) = pressureRightDeriv g t

Uses 5

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Logistic function \(e^t/(1+e^t)\) · Right derivative of the pressure · Wired infinite-volume edge density

DefinitionWired edge densities on a box bounded by right derivatives#✓fully proved

The wired q = 2 density of every edge of Λ_N at p = logistic(t) is at most the right derivative of g at t.

def fdd_WiredDensityUpperBound (N : ℕ) (g : ℝ → ℝ) : Prop :=
  ∀ (e' : Sym2 (boxVerts d N)) (t : ℝ),
    wiredEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t) ≤ pressureRightDeriv g t

Uses 5

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Logistic function \(e^t/(1+e^t)\) · Right derivative of the pressure · Wired infinite-volume edge density

DefinitionAverage edge density of the \(q = 2\) random-cluster measure#✓fully proved

The average edge density |E|^{-1} E_{φ_{G,p,2}}[#open edges] at p = logistic(t).

noncomputable def fpd_avgDensity (t : ℝ) : ℝ :=
  (1 / (G.edgeFinset.card : ℝ)) * fkExpect G (fsc_logistic t) 2 (fun ω => (openCount G ω : ℝ))

Uses 4 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster expectation of an observable · Logistic function \(e^t/(1+e^t)\) · Number of open edges

Used byCollapse of average edge densities to the free density · Per-box \(q = 2\) uniqueness off a countable set of tilts · Free average edge density collapse on boxes · Free growing-box collapse at \(q = 2\)

DefinitionCollapse of average edge densities to the free density#✓fully proved

The average edge densities of the graphs Gn n converge to the free infinite-volume q = 2 density of every edge of Λ_N, at every t.

def fpd_AvgDensityCollapse (d N : ℕ)
    (Gn : ℕ → SimpleGraph (boxVerts d N)) [∀ n, DecidableRel (Gn n).Adj] : Prop :=
  ∀ (e' : Sym2 (boxVerts d N)) (t : ℝ),
    Tendsto (fun n => fpd_avgDensity (Gn n) t) atTop
      (𝓝 (freeEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t)))

Uses 7

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Average edge density of the \(q = 2\) random-cluster measure · Free infinite-volume edge density · Logistic function \(e^t/(1+e^t)\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

DefinitionInfinite-volume edge densities as one-sided derivatives#✓fully proved

The wired and free q = 2 infinite-volume densities of every edge of Λ_N at p = logistic(t) are the right and left derivatives of g at t.

def fpd_IVDensityIsOneSidedDeriv (d N : ℕ) (g : ℝ → ℝ) : Prop :=
  (∀ (e' : Sym2 (boxVerts d N)) (t : ℝ),
      wiredEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t) = pressureRightDeriv g t)
    ∧ (∀ (e' : Sym2 (boxVerts d N)) (t : ℝ),
        freeEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t) = pressureLeftDeriv g t)

Uses 7

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Free infinite-volume edge density · Logistic function \(e^t/(1+e^t)\) · Left derivative of the pressure · Right derivative of the pressure · Wired infinite-volume edge density

DefinitionWeighted exponential sum#✓fully proved

The exponential sum S₀(t) = ∑_i w_i e^{a_i t}.

noncomputable def ivp2_Ssum (w a : ι → ℝ) (t : ℝ) : ℝ := ∑ i, w i * Real.exp (a i * t)

Used by 10

Used byConvexity of the ambient tilted log normalizer · Cauchy–Schwarz inequality for weighted exponential sums · Log-sum-exp cumulant generating function · Convexity of log-sum-exp with nonnegative nonzero weights · Wired tilted log normalizer as a cumulant generating function · Wired tilted log normalizer has derivative the mean open fraction · Tilted mean of open edges equals the wired FK expectation · Wired partition function at logistic \(p\) as a tilted sum · Per-box \(q = 2\) uniqueness off a countable set of tilts · Per-box uniqueness of the random-cluster measures off a countable set

DefinitionFirst moment exponential sum#✓fully proved

The first moment sum S₁(t) = ∑_i w_i a_i e^{a_i t}, the derivative of S₀.

noncomputable def ivp2_S1 (w a : ι → ℝ) (t : ℝ) : ℝ := ∑ i, w i * a i * Real.exp (a i * t)

Used by 6

Used byCauchy–Schwarz inequality for weighted exponential sums · Convexity of log-sum-exp with nonnegative nonzero weights · Wired tilted log normalizer has derivative the mean open fraction · Tilted mean of open edges equals the wired FK expectation · Per-box \(q = 2\) uniqueness off a countable set of tilts · Per-box uniqueness of the random-cluster measures off a countable set

DefinitionSecond moment exponential sum#✓fully proved

The second moment sum S₂(t) = ∑_i w_i a_i² e^{a_i t}, the derivative of S₁.

noncomputable def ivp2_S2 (w a : ι → ℝ) (t : ℝ) : ℝ := ∑ i, w i * a i ^ 2 * Real.exp (a i * t)

Used by 2

Used byCauchy–Schwarz inequality for weighted exponential sums · Convexity of log-sum-exp with nonnegative nonzero weights

LemmaCauchy–Schwarz inequality for weighted exponential sums#✓fully proved

Cauchy–Schwarz for the exponential sums: S₁² ≤ S₂ S₀.

lemma ivp2_cauchy_schwarz_cgf (w a : ι → ℝ) (hw : ∀ i, 0 ≤ w i) (t : ℝ) :
    (ivp2_S1 w a t) ^ 2 ≤ (ivp2_S2 w a t) * (ivp2_Ssum w a t)

Uses 3 · Used by 1

Statement usesFirst moment exponential sum · Second moment exponential sum · Weighted exponential sum

Used byConvexity of log-sum-exp with nonnegative nonzero weights

DefinitionLog-sum-exp cumulant generating function#✓fully proved

The log-sum-exp function K(t) = log ∑_i w_i e^{a_i t}, the cumulant generating function of a under the weights w.

noncomputable def ivp2_Kcgf (w a : ι → ℝ) (t : ℝ) : ℝ := Real.log (ivp2_Ssum w a t)

Uses 1 · Used by 7

Statement usesWeighted exponential sum

Used byConvexity of the ambient tilted log normalizer · Convexity of log-sum-exp with nonnegative nonzero weights · Convexity of the wired tilted log normalizer · Wired tilted log normalizer as a cumulant generating function · Wired tilted log normalizer has derivative the mean open fraction · Per-box \(q = 2\) uniqueness off a countable set of tilts · Per-box uniqueness of the random-cluster measures off a countable set

LemmaConvexity of log-sum-exp with nonnegative nonzero weights#✓fully proved

A cumulant generating function is convex.

lemma ivp2_Kcgf_convexOn (w a : ι → ℝ) (hw : ∀ i, 0 ≤ w i) (hpos : ∃ i, 0 < w i) :
    ConvexOn ℝ univ (ivp2_Kcgf w a)

Uses 5 · Used by 2

Statement usesLog-sum-exp cumulant generating function

Proof usesFirst moment exponential sum · Second moment exponential sum · Weighted exponential sum · Cauchy–Schwarz inequality for weighted exponential sums

Used byConvexity of the ambient tilted log normalizer · Convexity of the wired tilted log normalizer

DefinitionAmbient tilted log normalizer of a finite graph#✓fully proved

The ambient logit normalizer |E|⁻¹ log (fkZ G p q) + log (1 + eᵗ), with p = fsc_logistic t. For |E| > 0, the added term removes the Bernoulli denominator, not the unused-coordinate factor in fkZ. At zero edges this definition uses totalized real division and equals log (1 + eᵗ); no per-edge physical interpretation is intended.

noncomputable def ivp2_ambientTiltLogZ (q : ℝ) (t : ℝ) : ℝ :=
  (1 / (G.edgeFinset.card : ℝ)) * Real.log (fkZ G (fsc_logistic t) q)
    + Real.log (1 + Real.exp t)

Uses 2 · Used by 14

Statement usesAmbient FK normalizer · Logistic function \(e^t/(1+e^t)\)

Used byCentered free energy of a graph · Convexity of the ambient tilted log normalizer · Limits of ambient tilted log normalizers are convex · Ambient tilted log normalizer ignores the decidability instance · Limits of tilted log normalizers on a fixed box are attained · A limit shared with growing boxes is one fixed-box graph's value · Tilted log normalizers on a fixed box take finitely many values · Free-wired log-normalizer gap \(\le |\partial|\log q/|E|\) for \(q \ge 1\) · Assumed doubling, boundedness and oscillation data along \(K_j\) · Dyadic convergence data for the ambient tilted log normalizer · Box Fekete data from a uniform bound and an oscillation bound · Per-box \(q = 2\) uniqueness off a countable set of tilts · Convex limit of centered tilt free energies of boxes for \(d, q \ge 1\) · Per-box uniqueness of the random-cluster measures off a countable set

LemmaConvexity of the ambient tilted log normalizer#✓fully proved

The finite-volume ambient tilted log normalizer is convex in t.

lemma ivp2_ambientTiltLogZ_convexOn (q : ℝ) (hq : 0 < q) (hE : 0 < G.edgeFinset.card) :
    ConvexOn ℝ univ (ivp2_ambientTiltLogZ G q)

Uses 12 · Used by 4

Statement usesAmbient tilted log normalizer of a finite graph

Proof usesConfiguration space of a statistical-mechanics model · Number of closed edges · Bernoulli edge product · Unnormalized random-cluster weight · Ambient FK normalizer · Logistic function \(e^t/(1+e^t)\) · Log-sum-exp cumulant generating function · Convexity of log-sum-exp with nonnegative nonzero weights · Weighted exponential sum · Number of open clusters · Number of open edges

Used byLimits of ambient tilted log normalizers are convex · Per-box \(q = 2\) uniqueness off a countable set of tilts · Convex limit of centered tilt free energies of boxes for \(d, q \ge 1\) · Per-box uniqueness of the random-cluster measures off a countable set

LemmaPointwise limits of convex functions are convex#✓fully proved

A pointwise limit of convex functions on ℝ along a nontrivial filter is convex.

lemma ivp2_convexOn_of_tendsto {κ : Type*} {l : Filter κ} [l.NeBot]
    (f : κ → ℝ → ℝ) (g : ℝ → ℝ)
    (hconv : ∀ i, ConvexOn ℝ univ (f i))
    (hlim : ∀ x, Tendsto (fun i => f i x) l (𝓝 (g x))) :
    ConvexOn ℝ univ g

Used by 4

Used byPointwise limits of convex maps are convex with one-sided derivatives · Limits of ambient tilted log normalizers are convex · Per-box \(q = 2\) uniqueness off a countable set of tilts · Convex limit of centered tilt free energies of boxes for \(d, q \ge 1\)

LemmaLimits of ambient tilted log normalizers are convex#✓fully proved

Every pointwise limit of finite-volume ambient tilted log normalizers along a nontrivial filter is convex.

lemma ivp2_limitAmbientTiltLogZ_convexOn
    {κ : Type*} {l : Filter κ} [l.NeBot]
    {W : Type*} [Fintype W] [DecidableEq W]
    (Gn : κ → SimpleGraph W) [∀ i, DecidableRel (Gn i).Adj]
    (q : ℝ) (hq : 0 < q) (hE : ∀ i, 0 < (Gn i).edgeFinset.card)
    (g : ℝ → ℝ)
    (hlim : ∀ t, Tendsto (fun i => ivp2_ambientTiltLogZ (Gn i) q t) l (𝓝 (g t))) :
    ConvexOn ℝ univ g

Uses 3

Statement usesAmbient tilted log normalizer of a finite graph

Proof usesConvexity of the ambient tilted log normalizer · Pointwise limits of convex functions are convex

LemmaPointwise limits of convex maps are convex with one-sided derivatives#✓fully proved

A pointwise limit g of convex functions on ℝ is convex; its one-sided derivatives exist, are monotone, are one-sided limits of slopes, and agree off a countable set; slopes of the approximants converge to slopes of g.

lemma cdl_convexDerivLimit {κ : Type*} {l : Filter κ} [l.NeBot]
    (gn : κ → ℝ → ℝ) (g : ℝ → ℝ)
    (hconv : ∀ i, ConvexOn ℝ univ (gn i))
    (hlim : ∀ x, Tendsto (fun i => gn i x) l (𝓝 (g x))) :
    ConvexOn ℝ univ g
      ∧ (∀ t, HasDerivWithinAt g (pressureRightDeriv g t) (Ioi t) t)
      ∧ (∀ t, HasDerivWithinAt g (pressureLeftDeriv g t) (Iio t) t)
      ∧ (∀ t, Tendsto (slope g t) (𝓝[>] t) (𝓝 (pressureRightDeriv g t)))
      ∧ (∀ t, Tendsto (slope g t) (𝓝[<] t) (𝓝 (pressureLeftDeriv g t)))
      ∧ (∀ a b, Tendsto (fun i => slope (gn i) a b) l (𝓝 (slope g a b)))
      ∧ (∀ t, pressureLeftDeriv g t ≤ pressureRightDeriv g t)
      ∧ Monotone (pressureRightDeriv g)
      ∧ Monotone (pressureLeftDeriv g)
      ∧ {t : ℝ | pressureLeftDeriv g t ≠ pressureRightDeriv g t}.Countable

Uses 5

Statement usesLeft derivative of the pressure · Right derivative of the pressure

Proof usesConvex function has equal one-sided derivatives off a countable set · Pointwise limits of convex functions are convex · Left derivative of a convex function is at most the right one

LemmaContinuity of the logistic map#✓fully proved

The logistic map t ↦ e^t / (1 + e^t) is continuous. It equals Mathlib's Real.sigmoid.

lemma osc_fsc_logistic_continuous : Continuous fsc_logistic

Uses 1 · Used by 2

Statement usesLogistic function \(e^t/(1+e^t)\)

Used byContinuity in \(t\) of free \(q = 2\) edge marginals on a finite graph · Continuity in \(t\) of wired \(q = 2\) edge marginals on a finite graph

LemmaContinuity in \(p\) of the Bernoulli edge weight#✓fully proved

The Bernoulli edge weight of a fixed configuration is continuous in p.

lemma osc_edgeProduct_continuous {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (ω : ConfigSpace (Sym2 V)) :
    Continuous (fun p : ℝ => edgeProduct G p ω)

Uses 2 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli edge product

Used byContinuity in \(t\) of free \(q = 2\) edge marginals on a finite graph · Continuity in \(t\) of wired \(q = 2\) edge marginals on a finite graph

LemmaContinuity in \(t\) of free \(q = 2\) edge marginals on a finite graph#✓fully proved

The edge marginal of the free q = 2 FK measure on a finite graph is continuous in t.

lemma osc_freeBoxMarg_continuous {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (e : Sym2 V) :
    Continuous (fun s : ℝ => edgeMargProb (fkProb G (fsc_logistic s) 2) e)

Uses 10 · Used by 1

Statement usesEdge marginal of a mass function · Probability of an ambient FK configuration · Logistic function \(e^t/(1+e^t)\)

Proof usesConfiguration space of a statistical-mechanics model · Bernoulli edge product · Unnormalized random-cluster weight · Ambient FK normalizer · Number of open clusters · Continuity in \(p\) of the Bernoulli edge weight · Continuity of the logistic map

Used byLeft-continuity of the free \(q = 2\) edge density in \(t\)

LemmaContinuity in \(t\) of wired \(q = 2\) edge marginals on a finite graph#✓fully proved

The edge marginal of the wired q = 2 FK measure on a finite graph is continuous in t.

lemma osc_wiredBoxMarg_continuous {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (bdry : V → Prop) [DecidablePred bdry]
    (e : Sym2 V) :
    Continuous (fun s : ℝ => edgeMargProb (wiredFkProb G bdry (fsc_logistic s) 2) e)

Uses 10 · Used by 1

Statement usesEdge marginal of a mass function · Logistic function \(e^t/(1+e^t)\) · Wired random-cluster probability of a configuration

Proof usesConfiguration space of a statistical-mechanics model · Bernoulli edge product · Continuity in \(p\) of the Bernoulli edge weight · Continuity of the logistic map · Wired random-cluster weight · Wired random-cluster partition function · Number of open clusters with wired boundary conditions

Used byRight-continuity of the wired \(q = 2\) edge density in \(t\)

LemmaMonotonicity in \(p\) of free \(q = 2\) edge marginals on a finite graph#✓fully proved

The edge marginal of the free q = 2 FK measure on a finite graph is monotone in p.

lemma osc_fkEdgeMarg_monotone_in_p {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (e : Sym2 V) {p1 p2 : ℝ}
    (hp1 : 0 < p1) (hp1' : p1 < 1) (hp2 : 0 < p2) (hp2' : p2 < 1) (hle : p1 ≤ p2) :
    edgeMargProb (fkProb G p1 2) e ≤ edgeMargProb (fkProb G p2 2) e

Uses 10 · Used by 1

Statement usesEdge marginal of a mass function · Probability of an ambient FK configuration

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 · Number of open clusters · Increasing event · Holley inequality for increasing events

Used byFree \(q = 2\) edge density is monotone in \(p\) on \((0, 1)\)

LemmaFree \(q = 2\) edge density is monotone in \(p\) on \((0, 1)\)#✓fully proved

The free infinite-volume q = 2 edge density is monotone in p ∈ (0, 1).

lemma osc_freeEdgeDensity_q2_monotoneOn (d N : ℕ) (eb : Sym2 (boxVerts d N)) :
    MonotoneOn (freeEdgeDensity d 2 (edgeIncl d N eb)) (Ioo (0 : ℝ) 1)

Uses 21 · Used by 1

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

Proof usesConfiguration space of a statistical-mechanics model · 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\) · Edge marginal of a mass function · Event that an edge is open · Probability of an ambient FK configuration · Free \(q=2\) box masses of increasing cylinders tend to infinite volume · Free random-cluster measure on a box · Free box measure of a cylinder event as a finite sum · Free infinite-volume random-cluster measure · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Monotonicity in \(p\) of free \(q = 2\) edge marginals on a finite graph · Increasing event · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byFree \(q = 2\) edge density is monotone in \(t\)

LemmaFree \(q = 2\) edge density is monotone in \(t\)#✓fully proved

The free infinite-volume q = 2 edge density is monotone in t.

lemma osc_freeEdgeDensity_logistic_monotone (d N : ℕ) (eb : Sym2 (boxVerts d N)) :
    Monotone (fun s => freeEdgeDensity d 2 (edgeIncl d N eb) (fsc_logistic s))

Uses 5 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Free infinite-volume edge density · Logistic function \(e^t/(1+e^t)\)

Proof usesFree \(q = 2\) edge density is monotone in \(p\) on \((0, 1)\)

Used byLeft-continuity of the free \(q = 2\) edge density in \(t\)

LemmaWired \(q = 2\) edge density is monotone in \(t\)#✓fully proved

The wired infinite-volume q = 2 edge density is monotone in t.

lemma osc_wiredEdgeDensity_logistic_monotone (d N : ℕ) (eb : Sym2 (boxVerts d N)) :
    Monotone (fun s => wiredEdgeDensity d 2 (edgeIncl d N eb) (fsc_logistic s))

Uses 26 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Logistic function \(e^t/(1+e^t)\) · 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 · Wired infinite-volume measure as limit on increasing cylinder events · 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

Used byRight-continuity of the wired \(q = 2\) edge density in \(t\)

LemmaLeft-continuity of the free \(q = 2\) edge density in \(t\)#✓fully proved

The free infinite-volume q = 2 edge density is left-continuous in t.

lemma osc_freeEdgeDensity_left_continuous (d N : ℕ) (eb : Sym2 (boxVerts d N)) (t : ℝ) :
    ContinuousWithinAt
      (fun s => freeEdgeDensity d 2 (edgeIncl d N eb) (fsc_logistic s)) (Iio t) t

Uses 26 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Free infinite-volume edge density · Logistic function \(e^t/(1+e^t)\)

Proof usesConfiguration space of a statistical-mechanics model · 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\) · Edge marginal of a mass function · Event that an edge is open · Limit of free \(q = 2\) box measures of a cylinder event · Free \(q = 2\) infinite-volume mass of increasing cylinders as a box limit · Probability of an ambient FK configuration · Free \(q=2\) box masses of increasing cylinders tend to infinite volume · Free \(q = 2\) box measures are bounded by the limit value · Free random-cluster measure on a box · Free box measure of a cylinder event as a finite sum · Free infinite-volume random-cluster measure · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Continuity in \(t\) of free \(q = 2\) edge marginals on a finite graph · Free \(q = 2\) edge density is monotone in \(t\) · Increasing event · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts

LemmaRight-continuity of the wired \(q = 2\) edge density in \(t\)#✓fully proved

The wired infinite-volume q = 2 edge density is right-continuous in t.

lemma osc_wiredEdgeDensity_right_continuous (d N : ℕ) (eb : Sym2 (boxVerts d N)) (t : ℝ) :
    ContinuousWithinAt
      (fun s => wiredEdgeDensity d 2 (edgeIncl d N eb) (fsc_logistic s)) (Ioi t) t

Uses 26 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Logistic function \(e^t/(1+e^t)\) · Wired infinite-volume edge density

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\) · Edge marginal of a mass function · Event that an edge is open · Infimum of wired box probabilities of a box event · Wired infinite-volume probability equals the infimum over boxes · Wired infinite-volume measure as limit on increasing cylinder events · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Continuity in \(t\) of wired \(q = 2\) edge marginals on a finite graph · Wired \(q = 2\) edge density is monotone in \(t\) · 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 · Box \((-n, n)^d\) in the hypercubic lattice

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts

LemmaNon-bulk edge fraction bound from a boundary bound on their count#✓fully proved

If the non-bulk edges of Λ_n number at most C times the boundary of Λ_n, their fraction is at most C times the boundary-to-edge ratio.

lemma spc_boundaryFraction_le_surfaceVolume (n : ℕ) (C : ℝ) (hC : 0 ≤ C)
    (In : Finset (Sym2 (boxVerts d n)))
    (hIE : In ⊆ (boxGraph d n).edgeFinset)
    (hbd : ((boxGraph d n).edgeFinset.card - In.card : ℝ)
      ≤ C * (Finset.univ.filter (boxBoundary d n)).card)
    (hEpos : 0 < (boxGraph d n).edgeFinset.card) :
    (((boxGraph d n).edgeFinset.card - In.card : ℝ)) / (boxGraph d n).edgeFinset.card
      ≤ C * (((Finset.univ.filter (boxBoundary d n)).card : ℝ)
              / (boxGraph d n).edgeFinset.card)

Uses 5

Statement usesVertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

LemmaAmbient tilted log normalizer ignores the decidability instance#✓fully proved

The per-edge ambient tilted log normalizer does not depend on the decidability instance of the adjacency relation.

lemma spc_ambientTiltLogZ_instIrrel (N : ℕ) (H : SimpleGraph (boxVerts d N))
    (i1 i2 : DecidableRel H.Adj) (t : ℝ) :
    @ivp2_ambientTiltLogZ _ _ _ H i1 2 t = @ivp2_ambientTiltLogZ _ _ _ H i2 2 t

Uses 4 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Ambient tilted log normalizer of a finite graph · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byTilted log normalizers on a fixed box take finitely many values

LemmaTilted log normalizers on a fixed box take finitely many values#✓fully proved

The per-edge ambient tilted log normalizers of a sequence of graphs on the fixed box Λ_N take finitely many values.

lemma spc_range_finite (N : ℕ) (Gn : ℕ → SimpleGraph (boxVerts d N))
    [inst : ∀ n, DecidableRel (Gn n).Adj] (t : ℝ) :
    (Set.range (fun n => ivp2_ambientTiltLogZ (Gn n) 2 t)).Finite

Uses 5 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Ambient tilted log normalizer of a finite graph · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesAmbient tilted log normalizer ignores the decidability instance

Used byLimits of tilted log normalizers on a fixed box are attained

LemmaLimits of tilted log normalizers on a fixed box are attained#✓fully proved

A limit of per-edge ambient tilted log normalizers of graphs on the fixed box Λ_N is attained by one of the graphs.

lemma spc_feketeLimit_mem_finiteRange (N : ℕ) (Gn : ℕ → SimpleGraph (boxVerts d N))
    [∀ n, DecidableRel (Gn n).Adj] (g : ℝ → ℝ)
    (hfree : ∀ t, Tendsto (fun n => ivp2_ambientTiltLogZ (Gn n) 2 t) atTop (𝓝 (g t)))
    (t : ℝ) :
    g t ∈ Set.range (fun n => ivp2_ambientTiltLogZ (Gn n) 2 t)

Uses 5 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Ambient tilted log normalizer of a finite graph · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesTilted log normalizers on a fixed box take finitely many values

Used byA limit shared with growing boxes is one fixed-box graph's value

LemmaA limit shared with growing boxes is one fixed-box graph's value#✓fully proved

If graphs on the fixed box Λ_N and the growing boxes Λ_n have the same limiting per-edge ambient tilted log normalizer g t, then g t is the ambient tilted log normalizer of a single graph on Λ_N.

lemma spc_fixedBox_collapse_obstruction (N : ℕ) (Gn : ℕ → SimpleGraph (boxVerts d N))
    [∀ n, DecidableRel (Gn n).Adj] (g : ℝ → ℝ)
    (hfree : ∀ t, Tendsto (fun n => ivp2_ambientTiltLogZ (Gn n) 2 t) atTop (𝓝 (g t)))
    (hboxfree : ∀ t, Tendsto (fun n => ivp2_ambientTiltLogZ (boxGraph d n) 2 t) atTop (𝓝 (g t)))
    (t : ℝ) :
    (∃ H : SimpleGraph (boxVerts d N), ∃ _ : DecidableRel H.Adj,
        g t = ivp2_ambientTiltLogZ H 2 t)
      ∧ Tendsto (fun n => ivp2_ambientTiltLogZ (boxGraph d n) 2 t) atTop (𝓝 (g t))

Uses 6

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Ambient tilted log normalizer of a finite graph · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesLimits of tilted log normalizers on a fixed box are attained

LemmaVolume-growth lemma for tilted finite-volume bounds#✓fully proved

If ε ≤ q ^ (S n) λ ^ (m V n) / ε for all n, with q ≥ 1, 0 < λ < 1, V n → ∞ and S n / V n → 0, then m ≤ 0.

lemma secant_exponent_le_zero {q lam m ε : ℝ}
    (hq : 1 ≤ q) (hlampos : 0 < lam) (hlam1 : lam < 1) (hε : 0 < ε)
    {S V : ℕ → ℝ} (hVpos : ∀ n, 0 < V n)
    (hSV : Tendsto (fun n => S n / V n) atTop (𝓝 0))
    (hVinf : Tendsto V atTop atTop)
    (hineq : ∀ n, ε ≤ q ^ (S n) * lam ^ (m * V n) / ε) :
    m ≤ 0

Used by 1

Used byTilted finite-volume bounds for all \(\varepsilon > 0\) force \(b \le a\)

LemmaTilted finite-volume bounds for all \(\varepsilon > 0\) force \(b \le a\)#✓fully proved

If for every ε > 0 the bound ε ≤ q ^ (S n) λ ^ ((b - a - 2ε) V n) / ε holds for all n, with V n → ∞ and S n = o(V n), then b ≤ a.

lemma secant_b_le_a_of_finiteVolumeData {q lam a b : ℝ}
    (hq : 1 ≤ q) (hlampos : 0 < lam) (hlam1 : lam < 1)
    {S V : ℕ → ℝ} (hVpos : ∀ n, 0 < V n)
    (hSV : Tendsto (fun n => S n / V n) atTop (𝓝 0))
    (hVinf : Tendsto V atTop atTop)
    (hfv : ∀ ε > 0, ∀ n, ε ≤ q ^ (S n) * lam ^ ((b - a - 2 * ε) * V n) / ε) :
    b ≤ a

Uses 1 · Used by 1

Proof usesVolume-growth lemma for tilted finite-volume bounds

Used byTilt data give wired density at \(p'\) at most free density at \(p > p'\)

DefinitionFinite-volume tilt data for a box edge at \(q = 2\)#✓fully proved

Finite-volume tilt data for the box edge eb at q = 2: volumes V n → ∞ and surface terms S n = o(V n) such that, for all p' < p in (0, 1) and ε > 0, ε ≤ 2 ^ (S n) λ ^ ((θ^w(p') - θ^f(p) - 2ε) V n) / ε with λ = tiltFactor p p', where θ^w and θ^f are the wired and free infinite-volume densities of the edge.

def FKSecantData (d N : ℕ) (eb : Sym2 (boxVerts d N)) : Prop :=
  ∃ S V : ℕ → ℝ, (∀ n, 0 < V n)
    ∧ Tendsto (fun n => S n / V n) atTop (𝓝 0)
    ∧ Tendsto V atTop atTop
    ∧ ∀ p ∈ Ioo (0 : ℝ) 1, ∀ p' ∈ Ioo (0 : ℝ) 1, p' < p → ∀ ε > 0, ∀ n,
        ε ≤ (2 : ℝ) ^ (S n)
          * (tiltFactor p p')
              ^ ((wiredEdgeDensity d 2 (edgeIncl d N eb) p'
                    - freeEdgeDensity d 2 (edgeIncl d N eb) p - 2 * ε) * V n) / ε

Uses 5 · Used by 2

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

Used byBox-edge marginal uniqueness off a countable set under tilt data · Tilt data give wired density at \(p'\) at most free density at \(p > p'\)

LemmaTilt data give wired density at \(p'\) at most free density at \(p > p'\)#✓fully proved

Under FKSecantData, the wired edge density at p' is at most the free edge density at p whenever p' < p.

lemma hsecant_discharged (d N : ℕ) (eb : Sym2 (boxVerts d N))
    (hdata : FKSecantData d N eb) :
    ∀ 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

Uses 7 · Used by 1

Statement usesFinite-volume tilt data for a box edge at \(q = 2\) · Vertices 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 usesTilted finite-volume bounds for all \(\varepsilon > 0\) force \(b \le a\) · Tilt factor between two edge parameters

Used byBox-edge marginal uniqueness off a countable set under tilt data

LemmaBox-edge marginal uniqueness off a countable set under tilt data#✓fully proved

Under FKSecantData, at q = 2 there is a countable set S of parameters off which every measure φ whose box-edge marginal lies between the free and wired ones has the same marginal as both.

StatMech.FK.fk_uniqueness_q2_secant_from_finiteVolumeData · 17 lines

lemma fk_uniqueness_q2_secant_from_finiteVolumeData (d N : ℕ) (eb : Sym2 (boxVerts d N))
    (hdata : FKSecantData d N eb) :
    ∃ S : Set ℝ, S.Countable ∧
      ∀ p ∉ S, ∀ (hp : 0 < p) (hp1 : p < 1)
        (phi : Measure (ConfigSpace (Sym2 (Site d)))),
        ((freeInfiniteVolume d hp hp1 (by norm_num : (0:ℝ) < 2) : Measure _).real
            (boxRestrict d N ⁻¹' (boxEdgeOpenEvent d N eb)) ≤ phi.real
              (boxRestrict d N ⁻¹' (boxEdgeOpenEvent d N eb))
          ∧ phi.real (boxRestrict d N ⁻¹' (boxEdgeOpenEvent d N eb))
              ≤ (wiredInfiniteVolume d hp hp1 (by norm_num : (0:ℝ) < 2) : Measure _).real
                  (boxRestrict d N ⁻¹' (boxEdgeOpenEvent d N eb))) →
        phi.real (boxRestrict d N ⁻¹' (boxEdgeOpenEvent d N eb))
            = (freeInfiniteVolume d hp hp1 (by norm_num : (0:ℝ) < 2) : Measure _).real
                (boxRestrict d N ⁻¹' (boxEdgeOpenEvent d N eb))
          ∧ phi.real (boxRestrict d N ⁻¹' (boxEdgeOpenEvent d N eb))
              = (wiredInfiniteVolume d hp hp1 (by norm_num : (0:ℝ) < 2) : Measure _).real
                  (boxRestrict d N ⁻¹' (boxEdgeOpenEvent d N eb))

Uses 10

Statement usesConfiguration space of a statistical-mechanics model · Finite-volume tilt data for a box edge at \(q = 2\) · Event that a box edge is open · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Free infinite-volume random-cluster measure · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice

Proof usesSecant bound gives \(q = 2\) edge-event uniqueness off a countable set · Tilt data give wired density at \(p'\) at most free density at \(p > p'\)

DefinitionWired per-edge ambient tilted log normalizer#✓fully proved

The wired per-edge ambient tilted log normalizer |E|⁻¹ log Z^w(p, q) + log(1 + e^t) at p = e^t / (1 + e^t).

noncomputable def wpd_wiredAmbientTiltLogZ (q : ℝ) (t : ℝ) : ℝ :=
  (1 / (G.edgeFinset.card : ℝ)) * Real.log (wiredFkZ G bdry (fsc_logistic t) q)
    + Real.log (1 + Real.exp t)

Uses 2 · Used by 7

Statement usesLogistic function \(e^t/(1+e^t)\) · Wired random-cluster partition function

Used byWired centered free energy · Free-wired log-normalizer gap \(\le |\partial|\log q/|E|\) for \(q \ge 1\) · Convexity of the wired tilted log normalizer · Wired tilted log normalizer as a cumulant generating function · Wired tilted log normalizer has derivative the mean open fraction · Per-box \(q = 2\) uniqueness off a countable set of tilts · Per-box uniqueness of the random-cluster measures off a countable set

LemmaWired partition function at logistic \(p\) as a tilted sum#✓fully proved

The wired partition function at p = e^t / (1 + e^t) as a tilted sum over configurations divided by (1 + e^t)^{|E|}.

lemma wpd_wiredFkZ_logistic (t q : ℝ) :
    wiredFkZ G bdry (fsc_logistic t) q
      = ivp2_Ssum (fun ω => q ^ numClustersWired G bdry ω) (fun ω => (openCount G ω : ℝ)) t
          / (1 + Real.exp t) ^ G.edgeFinset.card

Uses 9 · Used by 2

Statement usesLogistic function \(e^t/(1+e^t)\) · Weighted exponential sum · Number of open edges · Wired random-cluster partition function · Number of open clusters with wired boundary conditions

Proof usesConfiguration space of a statistical-mechanics model · Number of closed edges · Bernoulli edge product · Wired random-cluster weight

Used byWired tilted log normalizer as a cumulant generating function · Tilted mean of open edges equals the wired FK expectation

LemmaWired tilted log normalizer as a cumulant generating function#✓fully proved

The wired ambient tilted log normalizer is |E|⁻¹ times the cumulant generating function of the number of open edges under the weight q^{k^w}.

lemma wpd_wiredAmbientTiltLogZ_eq_Kcgf (q : ℝ) (hq : 0 < q) (hE : 0 < G.edgeFinset.card)
    (t : ℝ) :
    wpd_wiredAmbientTiltLogZ G bdry q t
      = (1 / (G.edgeFinset.card : ℝ))
          * ivp2_Kcgf (fun ω => q ^ numClustersWired G bdry ω)
              (fun ω => (openCount G ω : ℝ)) t

Uses 9 · Used by 2

Statement usesLog-sum-exp cumulant generating function · Number of open edges · Wired per-edge ambient tilted log normalizer · Number of open clusters with wired boundary conditions

Proof usesConfiguration space of a statistical-mechanics model · Logistic function \(e^t/(1+e^t)\) · Weighted exponential sum · Wired random-cluster partition function · Wired partition function at logistic \(p\) as a tilted sum

Used byConvexity of the wired tilted log normalizer · Wired tilted log normalizer has derivative the mean open fraction

LemmaConvexity of the wired tilted log normalizer#✓fully proved

The wired ambient tilted log normalizer is convex in t.

lemma wpd_wiredAmbientTiltLogZ_convexOn (q : ℝ) (hq : 0 < q) (hE : 0 < G.edgeFinset.card) :
    ConvexOn ℝ univ (wpd_wiredAmbientTiltLogZ G bdry q)

Uses 7 · Used by 2

Statement usesWired per-edge ambient tilted log normalizer

Proof usesConfiguration space of a statistical-mechanics model · Log-sum-exp cumulant generating function · Convexity of log-sum-exp with nonnegative nonzero weights · Number of open edges · Wired tilted log normalizer as a cumulant generating function · Number of open clusters with wired boundary conditions

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts · Per-box uniqueness of the random-cluster measures off a countable set

DefinitionExpectation under the wired FK measure#✓fully proved

The expectation of an observable under the wired FK measure.

noncomputable def wpd_wiredFkExpect (p q : ℝ) (X : ConfigSpace (Sym2 V) → ℝ) : ℝ :=
  ∑ ω : ConfigSpace (Sym2 V), wiredFkProb G bdry p q ω * X ω

Uses 2 · Used by 7

Statement usesConfiguration space of a statistical-mechanics model · Wired random-cluster probability of a configuration

Used byAverage wired edge density · Average wired edge density as the mean of edge marginals · Wired tilted log normalizer has derivative the mean open fraction · Tilted mean of open edges equals the wired FK expectation · Expected wired open-edge count is the sum of edge marginals · Per-box \(q = 2\) uniqueness off a countable set of tilts · Per-box uniqueness of the random-cluster measures off a countable set

LemmaTilted mean of open edges equals the wired FK expectation#✓fully proved

The tilted mean of the number of open edges is its wired FK expectation.

lemma wpd_wiredCgfMean_eq_openCount_expect (q : ℝ) (hq : 0 < q) (t : ℝ) :
    wpd_wiredFkExpect G bdry (fsc_logistic t) q (fun ω => (openCount G ω : ℝ))
      = ivp2_S1 (fun ω => q ^ numClustersWired G bdry ω) (fun ω => (openCount G ω : ℝ)) t
          / ivp2_Ssum (fun ω => q ^ numClustersWired G bdry ω)
              (fun ω => (openCount G ω : ℝ)) t

Uses 13 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Logistic function \(e^t/(1+e^t)\) · First moment exponential sum · Weighted exponential sum · Number of open edges · Expectation under the wired FK measure · Number of open clusters with wired boundary conditions

Proof usesNumber of closed edges · Bernoulli edge product · Wired random-cluster probability of a configuration · Wired random-cluster weight · Wired random-cluster partition function · Wired partition function at logistic \(p\) as a tilted sum

Used byWired tilted log normalizer has derivative the mean open fraction

LemmaWired tilted log normalizer has derivative the mean open fraction#✓fully proved

The derivative in t of the wired ambient tilted log normalizer is |E|⁻¹ times the expected number of open edges under the wired FK measure.

lemma wpd_wiredAmbientTiltLogZ_hasDerivAt (q : ℝ) (hq : 0 < q) (hE : 0 < G.edgeFinset.card)
    (t : ℝ) :
    HasDerivAt (wpd_wiredAmbientTiltLogZ G bdry q)
      ((1 / (G.edgeFinset.card : ℝ))
        * wpd_wiredFkExpect G bdry (fsc_logistic t) q (fun ω => (openCount G ω : ℝ))) t

Uses 11 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Logistic function \(e^t/(1+e^t)\) · Number of open edges · Wired per-edge ambient tilted log normalizer · Expectation under the wired FK measure

Proof usesLog-sum-exp cumulant generating function · First moment exponential sum · Weighted exponential sum · Wired tilted log normalizer as a cumulant generating function · Tilted mean of open edges equals the wired FK expectation · Number of open clusters with wired boundary conditions

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts · Per-box uniqueness of the random-cluster measures off a countable set

DefinitionAverage wired edge density#✓fully proved

The average wired edge density |E|⁻¹ E^w[|ω|] at p = e^t / (1 + e^t).

noncomputable def wpd_avgWiredDensity (q : ℝ) (t : ℝ) : ℝ :=
  (1 / (G.edgeFinset.card : ℝ))
    * wpd_wiredFkExpect G bdry (fsc_logistic t) q (fun ω => (openCount G ω : ℝ))

Uses 4 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model · Logistic function \(e^t/(1+e^t)\) · Number of open edges · Expectation under the wired FK measure

Used byAverage wired density collapse at \(q = 2\) · Average wired edge density as the mean of edge marginals · Per-box \(q = 2\) uniqueness off a countable set of tilts · Per-box uniqueness of the random-cluster measures off a countable set · Wired average edge density collapse on boxes · Average wired \(q = 2\) edge density of a box as a mean of marginals

LemmaExpected wired open-edge count is the sum of edge marginals#✓fully proved

The expected number of open edges is the sum of the edge marginals.

lemma wpd_wiredFkExpect_openCount_eq_sum (p q : ℝ) :
    wpd_wiredFkExpect G bdry p q (fun ω => (openCount G ω : ℝ))
      = ∑ e ∈ G.edgeFinset, edgeMargProb (wiredFkProb G bdry p q) e

Uses 6 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Edge marginal of a mass function · Number of open edges · Wired random-cluster probability of a configuration · Expectation under the wired FK measure

Proof usesNumber of open edges in a finite edge set

Used byAverage wired edge density as the mean of edge marginals

LemmaAverage wired edge density as the mean of edge marginals#✓fully proved

The average wired edge density is the mean of the wired edge marginals.

lemma wpd_avgWiredDensity_eq_sum_edgeMarg (q : ℝ) (t : ℝ) :
    wpd_avgWiredDensity G bdry q t
      = (1 / (G.edgeFinset.card : ℝ))
          * ∑ e ∈ G.edgeFinset, edgeMargProb (wiredFkProb G bdry (fsc_logistic t) q) e

Uses 8 · Used by 2

Statement usesEdge marginal of a mass function · Logistic function \(e^t/(1+e^t)\) · Wired random-cluster probability of a configuration · Average wired edge density

Proof usesConfiguration space of a statistical-mechanics model · Number of open edges · Expectation under the wired FK measure · Expected wired open-edge count is the sum of edge marginals

Used byPer-box uniqueness of the random-cluster measures off a countable set · Average wired \(q = 2\) edge density of a box as a mean of marginals

LemmaWired and free FK weights within a factor \(q^{|\partial|}\), \(q \ge 1\)#✓fully proved

For q ≥ 1, the wired FK weight is at most the free one, and the free one is at most q^{|∂|} times the wired one.

lemma wpd_wiredFkWeight_le {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    (ω : ConfigSpace (Sym2 V)) :
    wiredFkWeight G bdry p q ω ≤ fkWeight G p q ω
      ∧ fkWeight G p q ω
          ≤ q ^ (Finset.univ.filter bdry).card * wiredFkWeight G bdry p q ω

Uses 14 · Used by 1

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

Proof usesAdding edges within a vertex set drops components by at most its size · Bernoulli edge product · Number of open clusters · Open 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 · Number of open clusters with wired boundary conditions · Open subgraph of a bond configuration · Boundary wiring relation · Wired open graph

Used bySandwich \(Z^w \le Z \le q^{|\partial|} Z^w\) for \(q \ge 1\)

LemmaSandwich \(Z^w \le Z \le q^{|\partial|} Z^w\) for \(q \ge 1\)#✓fully proved

For q ≥ 1, Z^w ≤ Z ≤ q^{|∂|} Z^w.

lemma wpd_wiredFkZ_le {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q) :
    wiredFkZ G bdry p q ≤ fkZ G p q
      ∧ fkZ G p q ≤ q ^ (Finset.univ.filter bdry).card * wiredFkZ G bdry p q

Uses 6 · Used by 1

Statement usesAmbient FK normalizer · Wired random-cluster partition function

Proof usesConfiguration space of a statistical-mechanics model · Unnormalized random-cluster weight · Wired random-cluster weight · Wired and free FK weights within a factor \(q^{|\partial|}\), \(q \ge 1\)

Used byFree-wired log-normalizer gap \(\le |\partial|\log q/|E|\) for \(q \ge 1\)

LemmaFree-wired log-normalizer gap \(\le |\partial|\log q/|E|\) for \(q \ge 1\)#✓fully proved

For q ≥ 1, the free and wired per-edge ambient tilted log normalizers differ by at most |∂| log q / |E|.

lemma wpd_ambientTiltLogZ_sub_le {q : ℝ} (hq : 1 ≤ q) (hE : 0 < G.edgeFinset.card) (t : ℝ) :
    |ivp2_ambientTiltLogZ G q t - wpd_wiredAmbientTiltLogZ G bdry q t|
      ≤ ((Finset.univ.filter bdry).card : ℝ) / (G.edgeFinset.card : ℝ) * Real.log q

Uses 12 · Used by 2

Statement usesAmbient tilted log normalizer of a finite graph · Wired per-edge ambient tilted log normalizer

Proof usesConfiguration space of a statistical-mechanics model · Bernoulli edge product · Unnormalized random-cluster weight · Ambient FK normalizer · Logistic function \(e^t/(1+e^t)\) · Number of open clusters · Wired random-cluster weight · Wired random-cluster partition function · Sandwich \(Z^w \le Z \le q^{|\partial|} Z^w\) for \(q \ge 1\) · Number of open clusters with wired boundary conditions

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts · Per-box uniqueness of the random-cluster measures off a countable set

DefinitionAverage wired density collapse at \(q = 2\)#✓fully proved

Average wired density collapse: for every edge e' of Λ_N and every t, the average wired edge density of Λ_n converges to the wired infinite-volume density of e'.

def wpd_AvgWiredDensityCollapse (N : ℕ) : Prop :=
  ∀ (e' : Sym2 (boxVerts d N)) (t : ℝ),
    Tendsto (fun n => wpd_avgWiredDensity (boxGraph d n) (boxBoundary d n) 2 t) atTop
      (𝓝 (wiredEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t)))

Uses 9

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\) · Logistic function \(e^t/(1+e^t)\) · Wired infinite-volume edge density · Average wired edge density · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

DefinitionCentered free energy of a graph#✓fully proved

The centered free energy F_G(t) - F_G(0), with F_G = ivp2_ambientTiltLogZ G q. In the FK range q > 0, the ambient non-edge offset cancels in this difference.

noncomputable def cfe_centered (q : ℝ) (t : ℝ) : ℝ :=
  ivp2_ambientTiltLogZ G q t - ivp2_ambientTiltLogZ G q 0

Uses 1 · Used by 4

Statement usesAmbient tilted log normalizer of a finite graph

Used byPointwise convergence of box centered free energies · Per-box \(q = 2\) uniqueness off a countable set of tilts · Convex limit of centered tilt free energies of boxes for \(d, q \ge 1\) · Per-box uniqueness of the random-cluster measures off a countable set

DefinitionWired centered free energy#✓fully proved

The wired centered free energy, obtained by subtracting wpd_wiredAmbientTiltLogZ G bdry q 0 from its value at t. In the FK range q > 0, the ambient non-edge offset cancels.

noncomputable def cfe_wiredCentered (q : ℝ) (t : ℝ) : ℝ :=
  wpd_wiredAmbientTiltLogZ G bdry q t - wpd_wiredAmbientTiltLogZ G bdry q 0

Uses 1 · Used by 2

Statement usesWired per-edge ambient tilted log normalizer

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts · Per-box uniqueness of the random-cluster measures off a countable set

DefinitionPointwise convergence of box centered free energies#✓fully proved

The centered free energies of the boxes Λ_n converge pointwise to G, and G(0) = 0.

def cfe_CenteredConvergence (d : ℕ) (G : ℝ → ℝ) : Prop :=
  (∀ t, Tendsto (fun n => cfe_centered (boxGraph d n) 2 t) atTop (𝓝 (G t))) ∧ G 0 = 0

Uses 5

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Centered free energy of a graph · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

72 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.