The finite-volume Ising Gibbs measure

10 fully proved

A. Spins and bonds

DefinitionSpin of a configuration at a site#✓fully proved

The spin σ_x ∈ {1, -1} of the configuration s at x: 1 for true, -1 for false.

def spin (s : ConfigSpace V) (x : V) : ℝ := if s x then 1 else -1

Uses 1 · Used by 108

Statement usesConfiguration space of a statistical-mechanics model

Used byPositive planar percolation at some \(p < 1\) via the Ising model · Griffiths' second inequality for two distinct spins · Field derivative of the magnetization as a sum of covariances · Three-replica variable \(d_w\) · Third Ursell function of the finite Ising model · Lebowitz four-point combination · Field derivative of the two-point covariance · GHS gap on an edge equals the third Ursell function · Griffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Field weight of the disagreement set · Agreement-set Boltzmann weight with doubled couplings and field · GHS concavity of the magnetization in the field · Three-site duplicated-variable factor · Griffiths–Hurst–Sherman inequality · Susceptibility bound \(\chi(h) \le m(h)/h \le 1/h\) from concavity · GHS susceptibility bound \(\chi \le 1/h\) · Spin covariance in the inhomogeneous model · Directional spin sum · GHS concavity · Inhomogeneous field weight of the disagreement set · Inhomogeneous agreement-set Boltzmann weight · Griffiths–Hurst–Sherman inequality · Third Ursell function of the inhomogeneous Ising model · Magnetization vanishes at zero field · Susceptibility bound \(\chi(h) \le m(h)/h\) from concavity · Total spin of a configuration · Rotated two-replica sum variable \(t_w\) · Rotated two-replica difference variable \(u_w\) · Monotonicity of correlations · Energy observable of the Ising model · First Griffiths inequality (GKS I) · Nonnegativity of the GKS positivity kernel · Griffiths' second inequality for inhomogeneous couplings · Griffiths monotonicity of correlations in the edge set · Boltzmann weight as a product of cosh-plus-sinh factors · Spin monomial with given exponents · Spin product over a vertex set · Configuration sum of a spin monomial is nonnegative · Unnormalized second Griffiths inequality · Boltzmann weight with inhomogeneous couplings and site fields · FKG inequality · Edge crossing from region-bounding dual walks and a walk decomposition · Edge crossing from closed-walk parities and walk decompositions · Edge crossing from cycle-parity compatibility of even subgraphs · Edge crossing from side colourings of dual walks · High-temperature expansion · Kramers–Wannier duality · Kramers–Wannier duality · Self-dual edge crossing of K₄ by complementary edges · Onsager's formula from the spin Kac-Ward identities · Onsager's formula · Box energy with a boundary condition · Uniqueness of the Gibbs state · Ising specification in a box · Ising specification as a Markov kernel · The plus state is a Gibbs (DLR) state · Specification applied to a bounded continuous function · Bond variable of a crossing bond · Finite-volume magnetization at the origin · Origin-only minus configuration satisfies the filled-cluster data · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Integrability of the spin at a site under finite measures · 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 · Spontaneous magnetization of the Ising model · Measurability of the spin at a site · Peierls' theorem · Spin at a site as a bounded continuous function · Energy on a set with a boundary condition · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · Finite-volume plus-boundary magnetization at the origin · Cluster lower bound for double-current sums · Random-current form of the \(\beta\)-derivative of the magnetization · Four-source lower bound for the pattern sum · Origin–site covariance in a box · Free-boundary site magnetization in a box · Finite-volume mean-field inequality for the Ising model · Origin magnetization with the outer-layer field switched off · Mean-field lower bound for the spontaneous magnetization · \(\beta\)-derivative of the origin magnetization in a box · Energy with general couplings and a uniform field · Random-current representation · Random-current representation with a field for even source sets · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Conditional finite-volume Aizenman–Barsky–Fernández inequality · Two-point spin covariance · Covariance of a spin with a bond variable · Negative Hamiltonian of the Ising model · Ising one-point function · Plus-state two-point function at zero field · Simon–Lieb inequality in the infinite-volume plus state · Simon–Lieb boundary sum against a measure · Simon–Lieb inequality on a finite graph · Boltzmann weight with a site field · Hamiltonian agrees with Physlib's Ising energy · Edge bond sum is half the sum over ordered adjacent pairs · Bond variable of an unordered pair · Bond variable takes values \(\pm 1\) · Ising Hamiltonian on a finite graph · Lee–Yang circle theorem · Ferromagnetic Lee–Yang polynomial has no zero in the open unit disk

DefinitionBond variable of an unordered pair#✓fully proved

The bond variable σ_x σ_y of an unordered pair e = {x, y}.

def bond (s : ConfigSpace V) (e : Sym2 V) : ℝ :=
  Sym2.lift ⟨fun x y => spin s x * spin s y, fun _ _ => mul_comm _ _⟩ e

Uses 2 · Used by 79

Statement usesConfiguration space of a statistical-mechanics model · Spin of a configuration at a site

Used byPositive planar percolation at some \(p < 1\) via the Ising model · Field derivative of the magnetization as a sum of covariances · Griffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Agreement-set Boltzmann weight with doubled couplings and field · Zero-field disagreement-set Boltzmann weight · GHS concavity of the magnetization in the field · Griffiths–Hurst–Sherman inequality · Susceptibility bound \(\chi(h) \le m(h)/h \le 1/h\) from concavity · GHS concavity · Inhomogeneous agreement-set Boltzmann weight · Griffiths–Hurst–Sherman inequality · Inhomogeneous zero-field disagreement-set weight · Magnetization vanishes at zero field · Susceptibility bound \(\chi(h) \le m(h)/h\) from concavity · Monotonicity of correlations · Energy observable of the Ising model · First Griffiths inequality (GKS I) · Griffiths' second inequality for inhomogeneous couplings · Griffiths monotonicity of correlations in the edge set · Boltzmann weight as a product of cosh-plus-sinh factors · Unnormalized second Griffiths inequality · Boltzmann weight with inhomogeneous couplings and site fields · FKG inequality · Edges cut by a spin configuration · Edge crossing from region-bounding dual walks and a walk decomposition · Edge crossing from closed-walk parities and walk decompositions · Edge crossing from cycle-parity compatibility of even subgraphs · Edge crossing from side colourings of dual walks · High-temperature expansion · Kramers–Wannier duality · Kramers–Wannier duality · Self-dual edge crossing of K₄ by complementary edges · Onsager's formula from the spin Kac-Ward identities · Onsager's formula · Box energy with a boundary condition · Uniqueness of the Gibbs state · Ising specification in a box · Ising specification as a Markov kernel · The plus state is a Gibbs (DLR) state · Specification applied to a bounded continuous function · Contour event of a set: opposite spins across every crossing bond · Bond variable of a crossing bond · Origin-only minus configuration satisfies the filled-cluster data · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · FK 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 · Peierls' theorem · Energy on a set with a boundary condition · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · Cluster lower bound for double-current sums · Random-current form of the \(\beta\)-derivative of the magnetization · Four-source lower bound for the pattern sum · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Bond energy of a configuration · Energy with general couplings and a uniform field · Boltzmann weight with couplings · Random-current representation · Random-current representation with a field for even source sets · Term of the exponential expansion of an edge weight · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Negative Hamiltonian of the Ising model · Simon–Lieb inequality in the infinite-volume plus state · Simon–Lieb inequality on a finite graph · Boltzmann weight with a site field · Hamiltonian agrees with Physlib's Ising energy · Edge bond sum is half the sum over ordered adjacent pairs · Bond variable takes values \(\pm 1\) · Ising Hamiltonian on a finite graph · Lee–Yang circle theorem · Ferromagnetic Lee–Yang polynomial has no zero in the open unit disk · Zero-field Boltzmann weight of a configuration

LemmaBond variable takes values \(\pm 1\)#✓fully proved

A bond variable is 1 or -1.

lemma bond_eq_pm (s : ConfigSpace V) (e : Sym2 V) : bond s e = 1 ∨ bond s e = -1

Uses 3 · Used by 15

Statement usesConfiguration space of a statistical-mechanics model · Bond variable of an unordered pair

Proof usesSpin of a configuration at a site

Used byGriffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Griffiths–Hurst–Sherman inequality · Griffiths–Hurst–Sherman inequality · Griffiths' second inequality for inhomogeneous couplings · Griffiths monotonicity of correlations in the edge set · Boltzmann weight as a product of cosh-plus-sinh factors · Unnormalized second Griffiths inequality · High-temperature expansion · Kramers–Wannier duality · Kramers–Wannier duality · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality on a finite graph

B. The Hamiltonian and the partition function

DefinitionIsing Hamiltonian on a finite graph#✓fully proved

The Ising Hamiltonian H(s) = -∑_{xy ∈ E(G)} σ_x σ_y - h ∑_x σ_x on a finite graph G with unit coupling and external field h. See also CondensedMatter.IsingModel.energy and StatMech.Ising.hamiltonian_eq_energy.

def hamiltonian (h : ℝ) (s : ConfigSpace V) : ℝ :=
  - (∑ e ∈ G.edgeFinset, bond s e) - h * ∑ x, spin s x

Uses 3 · Used by 28

Statement usesConfiguration space of a statistical-mechanics model · Bond variable of an unordered pair · Spin of a configuration at a site

Used byField derivative of the magnetization as a sum of covariances · Griffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · GHS concavity of the magnetization in the field · Griffiths–Hurst–Sherman inequality · Susceptibility bound \(\chi(h) \le m(h)/h \le 1/h\) from concavity · Magnetization vanishes at zero field · Susceptibility bound \(\chi(h) \le m(h)/h\) from concavity · Monotonicity of correlations · Boltzmann weight as a product of cosh-plus-sinh factors · Unnormalized second Griffiths inequality · FKG inequality · High-temperature expansion · Kramers–Wannier duality · Kramers–Wannier duality · Onsager's formula from the spin Kac-Ward identities · Onsager's formula · Random-current form of the \(\beta\)-derivative of the magnetization · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Random-current representation with a field for even source sets · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state · Ising model as a Physlib canonical ensemble · Hamiltonian agrees with Physlib's Ising energy · Finite-volume Ising Gibbs probability mass function · Boltzmann weight of an Ising configuration · Positivity of the Ising partition function

DefinitionBoltzmann weight of an Ising configuration#✓fully proved

The Boltzmann weight exp (-β H(s)) of a configuration at inverse temperature β.

noncomputable def isingWeight (β h : ℝ) (s : ConfigSpace V) : ℝ :=
  Real.exp (-β * hamiltonian G h s)

Uses 2 · Used by 29

Statement usesConfiguration space of a statistical-mechanics model · Ising Hamiltonian on a finite graph

Used byField derivative of the magnetization as a sum of covariances · Griffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Two-replica weight in an agreement fibre · GHS concavity of the magnetization in the field · Griffiths–Hurst–Sherman inequality · Susceptibility bound \(\chi(h) \le m(h)/h \le 1/h\) from concavity · Magnetization vanishes at zero field · Susceptibility bound \(\chi(h) \le m(h)/h\) from concavity · Monotonicity of correlations · First Griffiths inequality (GKS I) · Second Griffiths inequality (GKS II) · Boltzmann weight as a product of cosh-plus-sinh factors · Unnormalized second Griffiths inequality · FKG inequality · High-temperature expansion · Kramers–Wannier duality · Kramers–Wannier duality · Random-current form of the \(\beta\)-derivative of the magnetization · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Random-current representation with a field for even source sets · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state · Finite-volume Ising Gibbs probability mass function · Gibbs probability of an Ising configuration · Ising Gibbs probabilities sum to one · Ising partition function · Positivity of the Ising partition function

DefinitionIsing partition function#✓fully proved

The partition function Z = ∑_s exp (-β H(s)). See also CanonicalEnsemble.mathematicalPartitionFunction and StatMech.Ising.isingZ_eq_mathematicalPartitionFunction.

noncomputable def isingZ (β h : ℝ) : ℝ := ∑ s : ConfigSpace V, isingWeight G β h s

Uses 2 · Used by 32

Statement usesConfiguration space of a statistical-mechanics model · Boltzmann weight of an Ising configuration

Used byField derivative of the magnetization as a sum of covariances · Griffiths–Hurst–Sherman inequality · Law of the agreement configuration of two replicas · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · GHS concavity of the magnetization in the field · Griffiths–Hurst–Sherman inequality · Susceptibility bound \(\chi(h) \le m(h)/h \le 1/h\) from concavity · Magnetization vanishes at zero field · Susceptibility bound \(\chi(h) \le m(h)/h\) from concavity · Monotonicity of correlations · First Griffiths inequality (GKS I) · Second Griffiths inequality (GKS II) · FKG inequality · Dual high-temperature expansion proportional to the partition function · High-temperature expansion · Kramers–Wannier duality · Kramers–Wannier duality · Kramers–Wannier duality · High-temperature expansion · Zero-field Ising partition function with unit couplings · Random-current form of the \(\beta\)-derivative of the magnetization · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Random-current representation with a field for even source sets · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state · Ising Gibbs probability agrees with Physlib's canonical probability · Ising partition function agrees with Physlib's partition function · Finite-volume Ising Gibbs probability mass function · Gibbs probability of an Ising configuration · Ising Gibbs probabilities sum to one · Positivity of the Ising partition function

LemmaPositivity of the Ising partition function#✓fully proved

The partition function is positive.

lemma isingZ_pos (β h : ℝ) : 0 < isingZ G β h

Uses 4 · Used by 18

Statement usesIsing partition function

Proof usesConfiguration space of a statistical-mechanics model · Ising Hamiltonian on a finite graph · Boltzmann weight of an Ising configuration

Used byField derivative of the magnetization as a sum of covariances · Griffiths–Hurst–Sherman inequality · GHS concavity of the magnetization in the field · Griffiths–Hurst–Sherman inequality · Susceptibility bound \(\chi(h) \le m(h)/h \le 1/h\) from concavity · Susceptibility bound \(\chi(h) \le m(h)/h\) from concavity · Monotonicity of correlations · First Griffiths inequality (GKS I) · Second Griffiths inequality (GKS II) · FKG inequality · Random-current form of the \(\beta\)-derivative of the magnetization · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Random-current representation with a field for even source sets · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state · Finite-volume Ising Gibbs probability mass function · Ising Gibbs probabilities sum to one

C. The Gibbs distribution

DefinitionGibbs probability of an Ising configuration#✓fully proved

The Gibbs probability exp (-β H(s)) / Z of a configuration. See also CanonicalEnsemble.probability and StatMech.Ising.isingProb_eq_probability.

noncomputable def isingProb (β h : ℝ) (s : ConfigSpace V) : ℝ :=
  isingWeight G β h s / isingZ G β h

Uses 3 · Used by 23

Statement usesConfiguration space of a statistical-mechanics model · Boltzmann weight of an Ising configuration · Ising partition function

Used byField derivative of the magnetization as a sum of covariances · Griffiths–Hurst–Sherman inequality · GHS concavity of the magnetization in the field · Griffiths–Hurst–Sherman inequality · Susceptibility bound \(\chi(h) \le m(h)/h \le 1/h\) from concavity · Two-replica Ising expectation · Three-replica Ising expectation · Magnetization vanishes at zero field · Susceptibility bound \(\chi(h) \le m(h)/h\) from concavity · Monotonicity of correlations · First Griffiths inequality (GKS I) · Second Griffiths inequality (GKS II) · Finite-volume Ising expectation · FKG inequality · Random-current form of the \(\beta\)-derivative of the magnetization · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Random-current representation with a field for even source sets · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state · Ising Gibbs probability agrees with Physlib's canonical probability · Finite-volume Ising Gibbs probability mass function · Ising Gibbs probabilities sum to one

LemmaIsing Gibbs probabilities sum to one#✓fully proved

The Gibbs probabilities sum to one.

lemma isingProb_sum_eq_one (β h : ℝ) : ∑ s : ConfigSpace V, isingProb G β h s = 1

Uses 5 · Used by 10

Statement usesConfiguration space of a statistical-mechanics model · Gibbs probability of an Ising configuration

Proof usesBoltzmann weight of an Ising configuration · Ising partition function · Positivity of the Ising partition function

Used byGriffiths–Hurst–Sherman inequality · GHS concavity of the magnetization in the field · Griffiths–Hurst–Sherman inequality · Susceptibility bound \(\chi(h) \le m(h)/h \le 1/h\) from concavity · FKG inequality · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state · Finite-volume Ising Gibbs probability mass function

DefinitionFinite-volume Ising Gibbs probability mass function#✓fully proved

The finite-volume Ising Gibbs distribution as a probability mass function on configurations.

noncomputable def isingPMF (β h : ℝ) : PMF (ConfigSpace V) :=
  PMF.ofFintype (fun s => ENNReal.ofReal (isingProb G β h s)) (by
    rw [← ENNReal.ofReal_sum_of_nonneg (fun s _ => isingProb_nonneg G β h s),
      isingProb_sum_eq_one G β h]
    simp)

Uses 7

Statement usesConfiguration space of a statistical-mechanics model · Ising Hamiltonian on a finite graph · Gibbs probability of an Ising configuration · Ising Gibbs probabilities sum to one · Boltzmann weight of an Ising configuration · Ising partition function · Positivity of the Ising partition function

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.