Griffiths inequalities

DefinitionSpin value of a Boolean#✓fully proved

The spin value ±1 of a Boolean: 1 for true, -1 for false. See also CondensedMatter.IsingModel.spin and StatMech.Ising.spinB_eq_isingModelSpin.

def spinB (b : Bool) : ℝ := if b then 1 else -1

Used by 14

Used byConfiguration sum of a spin monomial is nonnegative · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · 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 · 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\) · Simon–Lieb inequality in the infinite-volume plus state · Simon–Lieb inequality on a finite graph · Boolean spin agrees with Physlib's Ising spin

DefinitionSpin monomial with given exponents#✓fully proved

The spin monomial ∏_x σ_x^{m_x} with exponents m : V → ℕ.

def monomial (m : V → ℕ) (s : ConfigSpace V) : ℝ := ∏ x : V, (spin s x) ^ (m x)

Uses 2 · Used by 11

Statement usesConfiguration space of a statistical-mechanics model · Spin 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 · 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 · Being a spin monomial · Configuration sum of a spin monomial is nonnegative · Unnormalized second Griffiths inequality

LemmaConfiguration sum of a spin monomial is nonnegative#✓fully proved

The sum of a spin monomial over all configurations is nonnegative.

lemma sum_monomial_nonneg (m : V → ℕ) : 0 ≤ ∑ s : ConfigSpace V, monomial m s

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Spin monomial with given exponents

Proof usesSpin of a configuration at a site · Spin value of a Boolean

Used byNonnegativity of the GKS positivity kernel

DefinitionBeing a spin monomial#✓fully proved

f is a spin monomial ∏_x σ_x^{m_x} for some exponents m.

def IsSpinMonomial (f : ConfigSpace V → ℝ) : Prop :=
  ∃ m : V → ℕ, ∀ s, f s = monomial m s

Uses 2 · Used by 9

Statement usesConfiguration space of a statistical-mechanics model · Spin monomial with given exponents

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 · 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 · Unnormalized second Griffiths inequality

LemmaNonnegativity of the GKS positivity kernel#✓fully proved

The positivity kernel of the GKS inequalities: for nonnegative c_i, d_i and spin monomials fac i, obs, the configuration sum of obs · ∏_i (c_i + d_i · fac_i) is nonnegative.

lemma gks_kernel {ι : Type*} (I : Finset ι) (c d : ι → ℝ)
    (hc : ∀ i ∈ I, 0 ≤ c i) (hd : ∀ i ∈ I, 0 ≤ d i)
    (fac : ι → ConfigSpace V → ℝ) (hfac : ∀ i ∈ I, IsSpinMonomial (fac i))
    (obs : ConfigSpace V → ℝ) (hobs : IsSpinMonomial obs) :
    0 ≤ ∑ s : ConfigSpace V, obs s * ∏ i ∈ I, (c i + d i * fac i s)

Uses 5 · Used by 8

Statement usesConfiguration space of a statistical-mechanics model · Being a spin monomial

Proof usesSpin monomial with given exponents · Spin of a configuration at a site · Configuration sum of a spin monomial is nonnegative

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 · First Griffiths inequality (GKS I) · Griffiths' second inequality for inhomogeneous couplings · Griffiths monotonicity of correlations in the edge set · Unnormalized second Griffiths inequality

DefinitionSpin product over a vertex set#✓fully proved

The spin product σ_A = ∏_{x ∈ A} σ_x.

def spinProd (A : Finset V) (s : ConfigSpace V) : ℝ := ∏ x ∈ A, spin s x

Uses 2 · Used by 29

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

Used byGriffiths' second inequality for two distinct spins · 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 · Griffiths–Hurst–Sherman inequality · Zero-field correlation in an induced subgraph · Correlation with field in an induced subgraph · Monotonicity of correlations · First Griffiths inequality (GKS I) · Second Griffiths inequality (GKS II) · Griffiths' second inequality for inhomogeneous couplings · Griffiths monotonicity of correlations in the edge set · Unnormalized second Griffiths inequality · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · 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 · Random-current representation · Correlation function with couplings · 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\) · Free-boundary zero-field two-point function in a finite set · Simon–Lieb inequality in the infinite-volume plus state · Simon–Lieb inequality on a finite graph · Two-point function with a site field

DefinitionFinite-volume Ising expectation#✓fully proved

The finite-volume Ising expectation ⟨f⟩ = ∑_s P(s) f(s) of an observable f.

noncomputable def isingExpectation (β h : ℝ) (f : ConfigSpace V → ℝ) : ℝ :=
  ∑ s : ConfigSpace V, isingProb G β h s * f s

Uses 2 · Used by 32

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

Used byGriffiths' second inequality for two distinct spins · Field derivative of the magnetization as a sum of covariances · 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 · 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 susceptibility bound \(\chi \le 1/h\) · 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) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Random-current form of the \(\beta\)-derivative of the magnetization · Origin–site covariance in a box · Free-boundary site magnetization in a box · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · \(\beta\)-derivative of the origin magnetization in a box · 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 · Ising one-point function · Free-boundary zero-field two-point function in a finite set · Simon–Lieb inequality in the infinite-volume plus state

LemmaBoltzmann weight as a product of cosh-plus-sinh factors#✓fully proved

The Boltzmann weight factorizes as a product over edges and vertices of cosh + sinh · σ terms.

lemma isingWeight_factor (β h : ℝ) (s : ConfigSpace V) :
    isingWeight G β h s
      = (∏ e ∈ G.edgeFinset, (Real.cosh β + bond s e * Real.sinh β))
        * (∏ x : V, (Real.cosh (β * h) + spin s x * Real.sinh (β * h)))

Uses 6 · Used by 1

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

Proof usesBond variable takes values \(\pm 1\) · Ising Hamiltonian on a finite graph

Used byFirst Griffiths inequality (GKS I)

TheoremFirst Griffiths inequality (GKS I)#✓fully proved

For the ferromagnetic Ising model on a finite graph with β ≥ 0 and h ≥ 0, every spin correlation is nonnegative: 0 ≤ ⟨σ_A⟩.

R. B. Griffiths, Correlations in Ising ferromagnets. I, J. Math. Phys. 8 (1967); D. G. Kelly and S. Sherman, General Griffiths' inequalities on correlations in Ising ferromagnets, J. Math. Phys. 9 (1968).

theorem gks_first (β h : ℝ) (hβ : 0 ≤ β) (hh : 0 ≤ h) (A : Finset V) :
    0 ≤ isingExpectation G β h (spinProd A)

Uses 13 · Used by 7

Statement usesFinite-volume Ising expectation · Spin product over a vertex set

Proof usesConfiguration space of a statistical-mechanics model · Being a spin monomial · Bond variable of an unordered pair · Nonnegativity of the GKS positivity kernel · Gibbs probability of an Ising configuration · Boltzmann weight of an Ising configuration · Boltzmann weight as a product of cosh-plus-sinh factors · Ising partition function · Positivity of the Ising partition function · Spin monomial with given exponents · Spin of a configuration at a site

Used byGriffiths–Hurst–Sherman inequality · GHS concavity of the magnetization in the field · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · 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\)

DefinitionPointwise product of two configurations#✓fully proved

The pointwise product of two configurations: spin σ_y σ'_y at y (true when the spins agree).

def xnor (σ q : ConfigSpace V) : ConfigSpace V := fun y => σ y == q y

Uses 1 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model

Used byDuplicated-variable involution on configuration pairs · Griffiths' second inequality for inhomogeneous couplings · Griffiths monotonicity of correlations in the edge set · Unnormalized second Griffiths inequality

DefinitionDuplicated-variable involution on configuration pairs#✓fully proved

The involution (σ, q) ↦ (σ, σ q) of pairs of configurations.

def dblFun (p : ConfigSpace V × ConfigSpace V) : ConfigSpace V × ConfigSpace V :=
  (p.1, xnor p.1 p.2)

Uses 2 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Pointwise product of two configurations

Used byGinibre's duplicated-variable change of variables

DefinitionGinibre's duplicated-variable change of variables#✓fully proved

Ginibre's duplicated-variable change of variables (σ, q) ↦ (σ, σ q) as an equivalence.

def dblEquiv : (ConfigSpace V × ConfigSpace V) ≃ (ConfigSpace V × ConfigSpace V) where
  toFun := dblFun
  invFun := dblFun
  left_inv := dblFun_invol
  right_inv := dblFun_invol

Uses 2 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Duplicated-variable involution on configuration pairs

Used byGriffiths' second inequality for inhomogeneous couplings · Griffiths monotonicity of correlations in the edge set · Unnormalized second Griffiths inequality

LemmaUnnormalized second Griffiths inequality#✓fully proved

The unnormalized second Griffiths inequality: Z² (⟨σ_{A ∆ B}⟩ - ⟨σ_A⟩⟨σ_B⟩) ≥ 0.

lemma unnorm_gks2 (β h : ℝ) (hβ : 0 ≤ β) (hh : 0 ≤ h) (A B : Finset V) :
    (∑ s, spinProd A s * isingWeight G β h s) * (∑ s, spinProd B s * isingWeight G β h s)
      ≤ (∑ s, spinProd (A ∆ B) s * isingWeight G β h s) * (∑ s, isingWeight G β h s)

Uses 12 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Boltzmann weight of an Ising configuration · Spin product over a vertex set

Proof usesBeing a spin monomial · Bond variable of an unordered pair · Bond variable takes values \(\pm 1\) · Ginibre's duplicated-variable change of variables · Nonnegativity of the GKS positivity kernel · Ising Hamiltonian on a finite graph · Spin monomial with given exponents · Spin of a configuration at a site · Pointwise product of two configurations

Used byMonotonicity of correlations · Second Griffiths inequality (GKS II)

TheoremSecond Griffiths inequality (GKS II)#✓fully proved

For the ferromagnetic Ising model on a finite graph with β ≥ 0 and h ≥ 0, spin correlations are positively correlated: ⟨σ_A⟩ ⟨σ_B⟩ ≤ ⟨σ_A σ_B⟩ = ⟨σ_{A ∆ B}⟩.

R. B. Griffiths, Correlations in Ising ferromagnets. I, J. Math. Phys. 8 (1967); D. G. Kelly and S. Sherman, General Griffiths' inequalities on correlations in Ising ferromagnets, J. Math. Phys. 9 (1968).

theorem gks_second (β h : ℝ) (hβ : 0 ≤ β) (hh : 0 ≤ h) (A B : Finset V) :
    isingExpectation G β h (spinProd A) * isingExpectation G β h (spinProd B)
      ≤ isingExpectation G β h (spinProd (A ∆ B))

Uses 8 · Used by 1

Statement usesFinite-volume Ising expectation · Spin product over a vertex set

Proof usesConfiguration space of a statistical-mechanics model · Gibbs probability of an Ising configuration · Boltzmann weight of an Ising configuration · Ising partition function · Positivity of the Ising partition function · Unnormalized second Griffiths inequality

Used byGriffiths' second inequality for two distinct spins

DefinitionEnergy observable of the Ising model#✓fully proved

The energy observable ∑_{e ∈ E(G)} σ_x σ_y + h ∑_x σ_x, the β-derivative of the log-weight.

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

Uses 3 · Used by 1

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

Used byMonotonicity of correlations

TheoremMonotonicity of correlations#✓fully proved

Monotonicity of correlations (a consequence of the second Griffiths inequality): for h ≥ 0, every spin correlation ⟨σ_A⟩_{β,h} is nondecreasing in β ≥ 0 (Griffiths, J. Math. Phys. 8 (1967)).

theorem corr_monotone (h : ℝ) (hh : 0 ≤ h) (A : Finset V) :
    MonotoneOn (fun β => isingExpectation G β h (spinProd A)) (Set.Ici (0 : ℝ))

Uses 12 · Used by 1

Statement usesFinite-volume Ising expectation · Spin product over a vertex set

Proof usesConfiguration space of a statistical-mechanics model · Bond variable of an unordered pair · Ising Hamiltonian on a finite graph · Gibbs probability of an Ising configuration · Boltzmann weight of an Ising configuration · Ising partition function · Positivity of the Ising partition function · Spin of a configuration at a site · Unnormalized second Griffiths inequality · Energy observable of the Ising model

Used bySharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\)

DefinitionBoltzmann weight with inhomogeneous couplings and site fields#✓fully proved

The Boltzmann weight exp(∑_{e ∈ E} J_e σ_e + ∑_x h_x σ_x).

noncomputable def wJ (E : Finset (Sym2 V)) (J : Sym2 V → ℝ) (hf : V → ℝ)
    (s : ConfigSpace V) : ℝ :=
  Real.exp ((∑ e ∈ E, J e * bond s e) + ∑ x, hf x * spin s x)

Uses 3 · Used by 17

Statement usesConfiguration space of a statistical-mechanics model · Bond variable of an unordered pair · Spin 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 · Two-replica expectation with inhomogeneous couplings · Inhomogeneous two-replica weight in an agreement fibre · GHS concavity · Griffiths–Hurst–Sherman inequality · Induced-subgraph partition function over the active sites only · Gibbs expectation with inhomogeneous couplings and site fields · Griffiths' second inequality for inhomogeneous couplings · Griffiths monotonicity of correlations in the edge set · Partition function with inhomogeneous couplings and site fields · Cluster lower bound for double-current sums · 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 · Simon–Lieb inequality in the infinite-volume plus state

DefinitionPartition function with inhomogeneous couplings and site fields#✓fully proved

The partition function ∑_σ wJ E J h σ.

noncomputable def ZJ (E : Finset (Sym2 V)) (J : Sym2 V → ℝ) (hf : V → ℝ) : ℝ :=
  ∑ s : ConfigSpace V, wJ E J hf s

Uses 2 · Used by 21

Statement usesConfiguration space of a statistical-mechanics model · Boltzmann weight with inhomogeneous couplings and site fields

Used byGriffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Griffiths–Hurst–Sherman inequality · Inhomogeneous law of the agreement configuration · Two-replica expectation with inhomogeneous couplings · GHS concavity · Inhomogeneous induced-subgraph partition function with field · Griffiths–Hurst–Sherman inequality · Inhomogeneous zero-field induced-subgraph partition function · Induced-subgraph partition function with doubled coupling and field · Zero-field induced-subgraph partition function with doubled coupling · Zero-field partition function of an induced subgraph · Gibbs expectation with inhomogeneous couplings and site fields · Edge-removal ratio of partition functions · Griffiths' second inequality for inhomogeneous couplings · Griffiths monotonicity of correlations in the edge set · Cluster lower bound for double-current sums · 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 · Simon–Lieb inequality in the infinite-volume plus state

DefinitionGibbs expectation with inhomogeneous couplings and site fields#✓fully proved

The Gibbs expectation ⟨f⟩_{E,J,h} = ∑_σ f(σ) w(σ) / Z.

noncomputable def expJ (E : Finset (Sym2 V)) (J : Sym2 V → ℝ) (hf : V → ℝ)
    (f : ConfigSpace V → ℝ) : ℝ :=
  (∑ s : ConfigSpace V, f s * wJ E J hf s) / ZJ E J hf

Uses 3 · Used by 18

Statement usesConfiguration space of a statistical-mechanics model · Partition function with inhomogeneous couplings and site fields · Boltzmann weight with inhomogeneous couplings and site fields

Used byGriffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Griffiths–Hurst–Sherman inequality · Spin covariance in the inhomogeneous model · Covariance with the directional spin · GHS concavity · Griffiths–Hurst–Sherman inequality · Third Ursell function of the inhomogeneous Ising model · Zero-field correlation in an induced subgraph · Correlation with field in an induced subgraph · Griffiths' second inequality for inhomogeneous couplings · Griffiths monotonicity of correlations in the edge set · Cluster lower bound for double-current sums · Four-source lower bound for the pattern sum · 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 · Simon–Lieb inequality in the infinite-volume plus state

TheoremGriffiths' second inequality for inhomogeneous couplings#✓fully proved

Griffiths' second inequality for nonnegative couplings and fields: ⟨σ_A⟩⟨σ_B⟩ ≤ ⟨σ_{A ∆ B}⟩. Reference: R. B. Griffiths, "Correlations in Ising ferromagnets I", J. Math. Phys. 8 (1967) 478–483; J. Ginibre, "General formulation of Griffiths' inequalities", Comm. Math. Phys. 16 (1970) 310–328. See also gks_second (GKS2) for uniform couplings.

theorem gks_second_J (E : Finset (Sym2 V)) (J : Sym2 V → ℝ) (hf : V → ℝ)
    (hJ : ∀ e ∈ E, 0 ≤ J e) (hhf : ∀ x, 0 ≤ hf x) (A B : Finset V) :
    expJ E J hf (spinProd A) * expJ E J hf (spinProd B)
      ≤ expJ E J hf (spinProd (A ∆ B))

Uses 13

Statement usesSpin product over a vertex set · Gibbs expectation with inhomogeneous couplings and site fields

Proof usesConfiguration space of a statistical-mechanics model · Being a spin monomial · Bond variable of an unordered pair · Bond variable takes values \(\pm 1\) · Ginibre's duplicated-variable change of variables · Nonnegativity of the GKS positivity kernel · Spin monomial with given exponents · Spin of a configuration at a site · Pointwise product of two configurations · Partition function with inhomogeneous couplings and site fields · Boltzmann weight with inhomogeneous couplings and site fields

TheoremGriffiths monotonicity of correlations in the edge set#✓fully proved

Griffiths monotonicity: adding edges with nonnegative couplings increases every correlation ⟨σ_A⟩. Reference: R. B. Griffiths, "Correlations in Ising ferromagnets I", J. Math. Phys. 8 (1967) 478–483.

theorem griffiths_mono (E₁ E₂ : Finset (Sym2 V)) (J : Sym2 V → ℝ) (hf : V → ℝ)
    (hsub : E₁ ⊆ E₂) (hJ : ∀ e ∈ E₂, 0 ≤ J e) (hhf : ∀ x, 0 ≤ hf x)
    (hdiag : ∀ e ∈ E₂, e ∉ E₁ → ¬ e.IsDiag) (A : Finset V) :
    expJ E₁ J hf (spinProd A) ≤ expJ E₂ J hf (spinProd A)

Uses 13 · Used by 8

Statement usesSpin product over a vertex set · Gibbs expectation with inhomogeneous couplings and site fields

Proof usesConfiguration space of a statistical-mechanics model · Being a spin monomial · Bond variable of an unordered pair · Bond variable takes values \(\pm 1\) · Ginibre's duplicated-variable change of variables · Nonnegativity of the GKS positivity kernel · Spin monomial with given exponents · Spin of a configuration at a site · Pointwise product of two configurations · Partition function with inhomogeneous couplings and site fields · Boltzmann weight with inhomogeneous couplings and site fields

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 · Cluster lower bound for double-current sums · 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

DefinitionEdge-removal ratio of partition functions#✓fully proved

The edge-removal ratio ζ(S) = (Z_{E∖S} / Z_E) ∏_{e ∈ S} cosh J_e.

noncomputable def ghy_zeta (E : Finset (Sym2 V)) (J : Sym2 V → ℝ) (hf : V → ℝ)
    (S : Finset (Sym2 V)) : ℝ :=
  ZJ (E \ S) J hf / ZJ E J hf * ∏ e ∈ S, Real.cosh (J e)

Uses 1 · Used by 1

Statement usesPartition function with inhomogeneous couplings and site fields

Used byEdge-removal weight with hyperbolic sine factors

DefinitionEdge-removal weight with hyperbolic sine factors#✓fully proved

The weight ρ(S) = ζ(S) ∏_{e ∈ S} tanh J_e = (Z_{E∖S} / Z_E) ∏_{e ∈ S} sinh J_e.

noncomputable def ghy_rho (E : Finset (Sym2 V)) (J : Sym2 V → ℝ) (hf : V → ℝ)
    (S : Finset (Sym2 V)) : ℝ :=
  ghy_zeta E J hf S * ∏ e ∈ S, Real.tanh (J e)

Uses 1

Statement usesEdge-removal ratio of partition functions

23 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.